From d0065d25191efe5bf9955597fd298793b026f22d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 09:56:26 +0000 Subject: [PATCH 01/12] Jenkinsfile: formatting --- Jenkinsfile | 55 +++++++++++++++++------------------------------------ 1 file changed, 17 insertions(+), 38 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index 952564b08..83a8f89d0 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -3,31 +3,19 @@ def img pipeline { agent none - options { - ansiColor('xterm') - } + options { ansiColor('xterm') } stages { - stage ( 'Pull Request' ) { + stage('Pull Request') { agent any 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('Build docker image') { steps { script { img = docker.build "c-semantics:${env.CHANGE_ID}" } } } + stage('Compile') { + options { timeout(time: 70, unit: 'MINUTES') } steps { script { img.inside { sh ''' @@ -38,12 +26,11 @@ pipeline { ''' } } } - 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' ) { + stage('Re-compile w/ timeout') { + options { timeout(time: 8, unit: 'MINUTES') } + steps { script { img.inside { sh ''' eval $(opam config env) @@ -52,11 +39,9 @@ pipeline { ''' } } } - } } - stage ( 'Test' ) { - options { - timeout(time: 300, unit: 'MINUTES') - } + } + stage('Test') { + options { timeout(time: 300, unit: 'MINUTES') } steps { script { img.inside { sh ''' @@ -67,11 +52,9 @@ pipeline { ''' } } } - 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 { + stage('Test clean target') { steps { script { img.inside { sh 'make clean' sh '[ $(git clean -xfd 2>&1 | wc -l) -eq 0 ]' @@ -80,18 +63,14 @@ pipeline { } // stages of 'Pull Request' } // Pull Request - stage ( 'Merged to master' ) { + 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('Build docker image') { steps { script { img = docker.build 'runtimeverificationinc/c-semantics:latest' } } } } // stages of 'Merged to master' } // 'Merged to master' From 165b7db67d935217f8a2dd34caa2c4a63533d077 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 10:02:34 +0000 Subject: [PATCH 02/12] Dockerfile, Jenkinsfile: use prebuilt K images --- Dockerfile | 53 +++++++---------------------------------------------- Jenkinsfile | 2 +- 2 files changed, 8 insertions(+), 47 deletions(-) diff --git a/Dockerfile b/Dockerfile index 7d9cb9584..899478686 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,4 +1,5 @@ -FROM runtimeverificationinc/kframework:ubuntu-bionic +ARG K_COMMIT +FROM runtimeverificationincink/kframework-k:ubuntu-bionic-${K_COMMIT} ##################### # Install packages. # @@ -11,50 +12,10 @@ RUN apt-get update -q \ 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 - # 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. # -################### - -COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \ - --chown=user:user \ - /home/user/.opam \ - /home/user/.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 - -# 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 - -RUN cd ${DEPS_DIR}/k \ - && mvn package -q -U \ - -DskipTests -DskipKTest \ - -Dhaskell.backend.skip -Dllvm.backend.skip \ - -Dcheckstyle.skip - -ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin" +USER user:user +WORKDIR /home/user diff --git a/Jenkinsfile b/Jenkinsfile index 83a8f89d0..014173de2 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -13,7 +13,7 @@ pipeline { } 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('Build docker image') { steps { script { img = docker.build "c-semantics:${env.CHANGE_ID}" "--build-arg K_COMMIT=$(cd .build/k && git rev-pares --short=7 HEAD) --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)" } } } stage('Compile') { options { timeout(time: 70, unit: 'MINUTES') } steps { From d5f8c4f47678acf7531c2c7a993109633775a96b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 10:05:26 +0000 Subject: [PATCH 03/12] Jenkinsfile: use image directly instead of img.inside --- Jenkinsfile | 52 +++++++++++++++++++++------------------------------- 1 file changed, 21 insertions(+), 31 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index 014173de2..e374cba4f 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -1,78 +1,68 @@ -// Object holding the docker image. -def img - pipeline { - agent none + agent { + dockerfile { + label 'docker' + additionalBuildArgs '--build-arg K_COMMIT=$(cd ext/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 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}" "--build-arg K_COMMIT=$(cd .build/k && git rev-pares --short=7 HEAD) --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)" } } } + 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' } } } stage('Re-compile w/ timeout') { options { timeout(time: 8, unit: 'MINUTES') } steps { - script { img.inside { + script { sh ''' eval $(opam config env) eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib) make ''' - } } + } } } 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 } } } - stage('Test clean target') { steps { - script { img.inside { - sh 'make clean' - sh '[ $(git clean -xfd 2>&1 | wc -l) -eq 0 ]' - } } - } } + stage('Test clean target') { + steps { + script { + 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' } } } - } // stages of 'Merged to master' - } // 'Merged to master' - } // pipeline stages } // pipeline From 119f201ce81da7c9bb96a02af6cdac8d7d88ea05 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 10:06:51 +0000 Subject: [PATCH 04/12] Jenkinsfile: cleanup --- Jenkinsfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index e374cba4f..602196fc5 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -62,7 +62,7 @@ pipeline { } } } - } // stages of 'Pull Request' - } // Pull Request - } // pipeline stages -} // pipeline + } + } + } +} From b67d40b9afc1e4fd1739363e387e5f9179056a5c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 10:08:05 +0000 Subject: [PATCH 05/12] Jenkinsfile: correct directory for getting K submodule --- Jenkinsfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index 602196fc5..e2a298101 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -2,7 +2,7 @@ pipeline { agent { dockerfile { label 'docker' - additionalBuildArgs '--build-arg K_COMMIT=$(cd ext/k && git rev-parse --short=7 HEAD) --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)' + 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') } From 71f2939b21fd9cb08c5d9c3b581e6aeb98384927 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 10:28:54 +0000 Subject: [PATCH 06/12] Dockerfile: typo --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 899478686..f10f6d738 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,5 +1,5 @@ ARG K_COMMIT -FROM runtimeverificationincink/kframework-k:ubuntu-bionic-${K_COMMIT} +FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT} ##################### # Install packages. # From 9d14bbc5d1548bfbd79b2056f39af11db6d3943a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 11:39:52 +0000 Subject: [PATCH 07/12] Makefile: get K_BIN from where kompile PATH is --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 9b28f6b69..5b6bbf7b3 100644 --- a/Makefile +++ b/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 From 9c28709a720dc55c3f9144e0f5fb146b246ccc62 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 13:00:12 +0000 Subject: [PATCH 08/12] Dockerfile: setup opam ahead of time --- Dockerfile | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Dockerfile b/Dockerfile index f10f6d738..15589bb36 100644 --- a/Dockerfile +++ b/Dockerfile @@ -19,3 +19,9 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user USER user:user WORKDIR /home/user + +COPY --chown=user:user .build/k/k-distribution/main/scripts/lib/opam ~/lib/opam +COPY --chown=user:user .build/k/k-distribution/main/scripts/bin ~/bin + +ENV OPAMROOT=/home/user/.opam +RUN ./bin/k-configure-opam-dev From cd89e6582c7aa2771001d568279bf3cd5d9a161b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 13:00:35 +0000 Subject: [PATCH 09/12] Dockerfile: use absolute paths --- Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index 15589bb36..4aeefc091 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,8 +20,8 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user USER user:user WORKDIR /home/user -COPY --chown=user:user .build/k/k-distribution/main/scripts/lib/opam ~/lib/opam -COPY --chown=user:user .build/k/k-distribution/main/scripts/bin ~/bin +COPY --chown=user:user .build/k/k-distribution/main/scripts/lib/opam /home/user/lib/opam +COPY --chown=user:user .build/k/k-distribution/main/scripts/bin /home/user/bin ENV OPAMROOT=/home/user/.opam RUN ./bin/k-configure-opam-dev From 838d8e4a65c8ca8b5cf98ee1ca931c45c45d7653 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 13:01:42 +0000 Subject: [PATCH 10/12] Dockerfile: formatting --- Dockerfile | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/Dockerfile b/Dockerfile index 4aeefc091..23bf2fd48 100644 --- a/Dockerfile +++ b/Dockerfile @@ -5,12 +5,13 @@ 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 apt-get update \ + && apt-get upgrade --yes \ + && apt-get install --yes \ + clang-6.0 \ + clang++-6.0 \ + libstdc++6 \ + llvm-6.0 # This user is set up in the runtimeverificationinc/kframework:* images. ARG USER_ID=1000 From 44ce55d5e476bf105f2ea2452491ed00119a57c9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 13:08:08 +0000 Subject: [PATCH 11/12] Dockerfile: correct paths --- Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index 23bf2fd48..2fa3ebbc2 100644 --- a/Dockerfile +++ b/Dockerfile @@ -21,8 +21,8 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user USER user:user WORKDIR /home/user -COPY --chown=user:user .build/k/k-distribution/main/scripts/lib/opam /home/user/lib/opam -COPY --chown=user:user .build/k/k-distribution/main/scripts/bin /home/user/bin +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 OPAMROOT=/home/user/.opam RUN ./bin/k-configure-opam-dev From 4180d3a4a4f4d7d9958666e1118b23b446c7bf64 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 13 May 2020 13:18:54 +0000 Subject: [PATCH 12/12] Dockerfile: add pkg-config --- Dockerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 2fa3ebbc2..1bd47b49a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -11,7 +11,8 @@ RUN apt-get update \ clang-6.0 \ clang++-6.0 \ libstdc++6 \ - llvm-6.0 + llvm-6.0 \ + pkg-config # This user is set up in the runtimeverificationinc/kframework:* images. ARG USER_ID=1000