K dockerhub images

Dockerfile

@@ -1,60 +1,29 @@
-FROM runtimeverificationinc/kframework:ubuntu-bionic
+ARG K_COMMIT
+FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT}
 
 #####################
 # Install packages. #
 #####################
 
-RUN     apt-get update -q \
-    &&  apt install --yes \
-          libstdc++6      \
-          llvm-6.0        \
-          clang++-6.0     \
-          clang-6.0
-
-RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \
-    && cd z3                                                        \
-    && python scripts/mk_make.py                                    \
-    && cd build                                                     \
-    && make -j8                                                     \
-    && make install                                                 \
-    && cd ../..                                                     \
-    && rm -rf z3
+RUN    apt-get update        \
+    && apt-get upgrade --yes \
+    && apt-get install --yes \
+          clang-6.0          \
+          clang++-6.0        \
+          libstdc++6         \
+          llvm-6.0           \
+          pkg-config
 
 # This user is set up in the runtimeverificationinc/kframework:* images.
-USER user:user
-
-##################
-# Perl packages. #
-##################
-
-COPY --from=runtimeverificationinc/perl:ubuntu-bionic \
-     --chown=user:user \
-     /home/user/perl5 \
-     /home/user/perl5
-
-###################
-# Configure opam. #
-###################
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
 
-COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \
-     --chown=user:user \
-     /home/user/.opam \
-     /home/user/.opam
-
-
-# This is where the rest of the dependencies go.
-ENV DEPS_DIR="/home/user/c-semantics-deps"
-
-############
-# Build K. #
-############
-
-COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k
+USER user:user
+WORKDIR /home/user
 
-RUN cd ${DEPS_DIR}/k \
-  && mvn package -q -U \
-      -DskipTests -DskipKTest \
-      -Dhaskell.backend.skip -Dllvm.backend.skip \
-      -Dcheckstyle.skip
+COPY --chown=user:user .build/k/k-distribution/src/main/scripts/lib/opam /home/user/lib/opam
+COPY --chown=user:user .build/k/k-distribution/src/main/scripts/bin      /home/user/bin
 
-ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
+ENV OPAMROOT=/home/user/.opam
+RUN ./bin/k-configure-opam-dev

Jenkinsfile

@@ -1,99 +1,68 @@
-// Object holding the docker image.
-def img
-
 pipeline {
-  agent none 
-  options {
-    ansiColor('xterm')
+  agent {
+    dockerfile {
+      label 'docker'
+      additionalBuildArgs '--build-arg K_COMMIT=$(cd .build/k && git rev-parse --short=7 HEAD) --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+    }
   }
+  options { ansiColor('xterm') }
   stages {
-    stage ( 'Pull Request' ) {
-      agent any
+    stage('Pull Request') {
       when { 
         changeRequest()
         beforeAgent true
       }
       stages {
-        stage ( 'Set title' ) { steps {
-          script {
-            currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
-          }
-        } }
-        stage ( 'Build docker image' ) { steps {
-          script {
-            img = docker.build "c-semantics:${env.CHANGE_ID}"
-          }
-        } }
-        stage ( 'Compile' ) {
-          options {
-            timeout(time: 70, unit: 'MINUTES')
-          }
+        stage('Set title') { steps { script { currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}" } } }
+        stage('Compile') {
+          options { timeout(time: 70, unit: 'MINUTES') }
           steps {
-            script { img.inside {
+            script {
               sh '''
                 eval $(opam config env)
                 eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
                 export KOMPILE_FLAGS=-O2
                 make -j4 profile-rule-parsing --output-sync=line
               '''
-            } }
+            }
           }
-          post { success {
-            archiveArtifacts 'dist/timelogs.d/timelogs.csv'
-          } }
+          post { success { archiveArtifacts 'dist/timelogs.d/timelogs.csv' } }
         }
-        stage ( 'Re-compile w/ timeout' ) { steps {
-          timeout(time: 8, unit: 'SECONDS' ) {
-            script { img.inside {
+        stage('Re-compile w/ timeout') {
+          options { timeout(time: 8, unit: 'MINUTES') }
+          steps {
+            script {
               sh '''
                 eval $(opam config env)
                 eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
                 make
               '''
-            } }
-          }
-        } }
-        stage ( 'Test' ) {
-          options {
-            timeout(time: 300, unit: 'MINUTES')
+            }
           }
+        }
+        stage('Test') {
+          options { timeout(time: 300, unit: 'MINUTES') }
           steps {
-            script { img.inside {
+            script {
               sh '''
                 eval $(opam config env)
                 eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
                 ${K_BIN}/spawn-kserver
                 make -C tests/unit-pass -j$(nproc) os-comparison
               '''
-            } }
+            }
           }
-          post { always {
-            archiveArtifacts artifacts: 'tests/unit-pass/*config', allowEmptyArchive: true
-          } }
+          post { always { archiveArtifacts artifacts: 'tests/unit-pass/*config', allowEmptyArchive: true } }
         }
-        stage ( 'Test clean target' ) { steps {
-          script { img.inside {
-            sh 'make clean'
-            sh '[ $(git clean -xfd 2>&1 | wc -l) -eq 0 ]'
-          } }
-       } }
-      } // stages of 'Pull Request'
-    }   // Pull Request
-
-    stage ( 'Merged to master' ) {
-      when {
-        branch 'master'
-        beforeAgent true
-      }
-      agent any
-      stages {
-        stage ( 'Build docker image' ) { steps {
-          script {
-            img = docker.build 'runtimeverificationinc/c-semantics:latest'
+        stage('Test clean target') {
+          steps {
+            script {
+              sh 'make clean'
+              sh '[ $(git clean -xfd 2>&1 | wc -l) -eq 0 ]'
+            }
           }
-        } }
-      } // stages of 'Merged to master'
-    }   // 'Merged to master'
-
-  }     // pipeline stages
-}       // pipeline
+        }
+      }
+    }
+  }
+}

Makefile

@@ -1,9 +1,9 @@
 ROOT := $(realpath $(dir $(lastword $(MAKEFILE_LIST))))
 
-export K_BIN ?= $(ROOT)/.build/k/k-distribution/target/release/k/bin
+export K_BIN ?= $(dir $(shell which kompile))
 
-export KOMPILE := $(K_BIN)/kompile
-export KDEP := $(K_BIN)/kdep
+export KOMPILE := kompile
+export KDEP    := kdep
 
 # Appending to whatever the environment provided.
 K_OPTS += -Xmx8g