Update dependency: deps/k_release

* deps/k_release: v5.0.0-4e7c3d0

* deps/k_release: v5.0.0-89fed2e

* include.mk: Don't delete kore-expand-macros

* test: Remove obsolete references to domains.k

* deps/k_release: v5.0.0-62ed02e

* Dockerfile: Use K release

* Dockerfile: Remove Z3, HLint, and stylish-haskell

Z3 should now be provided by the K Framework Docker image. HLint and
stylish-haskell checks are not run on Jenkins anymore, but on GitHub Actions.

* Check with stylish-haskell for Test workflow

* Check that stack.yaml.lock is up-to-date in Test workflow

* include.mk: Do not install our own K

* deps/k_release: v5.0.0-95b467b

* deps/k_release: v5.0.0-c305b58

* Jenkinsfile: Check phase runs on GitHub now

* test: make golden

* include.mk: Run kore-exec with --no-bug-report

* Add Docker scripts

Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: rv-jenkins

.github/workflows/test.yml

@@ -116,6 +116,14 @@ jobs:
           path: ${{ steps.locate-stack-root.outputs.stack-root }}
           key: ${{ runner.os }}-ghc-8.10.1-${{ hashFiles('stack.yaml.lock') }}
 
+      - name: Build dependencies
+        run: |
+          stack build --only-dependencies
+          if [ ! $(git status --porcelain | wc -l) -eq 0 ]; then
+            git diff
+            exit 1
+          fi
+
       - name: Build project
         run: stack build --pedantic
 
@@ -134,3 +142,29 @@ jobs:
 
       - name: Run hlint
         run: curl -sSL https://raw.github.com/ndmitchell/hlint/master/misc/run.sh | sh -s kore -j
+
+  stylish-haskell:
+    name: 'stylish-haskell'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Install stylish-haskell
+        run: |
+          cd $(mktemp -d)
+          wget https://github.com/jaspervdj/stylish-haskell/releases/download/v0.11.0.0/stylish-haskell-v0.11.0.0-linux-x86_64.tar.gz
+          tar xaf stylish-haskell-v0.11.0.0-linux-x86_64.tar.gz
+          sudo mv stylish-haskell-v0.11.0.0-linux-x86_64/stylish-haskell /usr/local/bin/
+          stylish-haskell --version
+
+      - uses: actions/checkout@v2.3.4
+        with:
+          submodules: recursive
+
+      - name: Format with stylish-haskell
+        run: stylish-haskell -i -r kore
+
+      - name: Check for changes
+        run: |
+          if [ ! $(git status --porcelain | wc -l) -eq 0 ]; then
+            git diff
+            exit 1
+          fi

Dockerfile

@@ -1,4 +1,5 @@
-FROM ubuntu:bionic
+ARG K_COMMIT
+FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT}
 
 ENV TZ=America/Chicago
 RUN    ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \
@@ -7,47 +8,22 @@ RUN    ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/local
 RUN    apt update                                                                \
     && apt upgrade --yes                                                         \
     && apt install --yes                                                         \
-           bison curl flex gcc git jq                                            \
-           make openjdk-8-jdk pandoc                                             \
            libtinfo-dev                                                          \
-           python3 python-pygments python-recommonmark python-sphinx             \
-           time unzip wget
+           curl git make unzip
 
-RUN update-alternatives --set java /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java
+ENV LC_ALL=C.UTF-8
 
 ARG USER_ID=1000
 ARG GROUP_ID=1000
 RUN    groupadd --gid $GROUP_ID user                                        \
     && useradd --create-home --uid $USER_ID --shell /bin/sh --gid user user
 
-ADD scripts/install-stack.sh /home/user/.install-stack/
-RUN /home/user/.install-stack/install-stack.sh
+ARG STACK=2.5.1
+RUN curl -sSL https://raw.githubusercontent.com/commercialhaskell/stack/v$STACK/etc/scripts/get-stack.sh | sh
 
 USER $USER_ID:$GROUP_ID
+WORKDIR /home/user
 
-ENV LC_ALL=C.UTF-8
-
-ARG Z3=4.8.8
-RUN    cd /home/user \
-    && wget https://github.com/Z3Prover/z3/releases/download/z3-$Z3/z3-$Z3-x64-ubuntu-16.04.zip \
-    && unzip z3-$Z3-x64-ubuntu-16.04.zip \
-    && rm z3-$Z3-x64-ubuntu-16.04.zip \
-    && mv z3-$Z3-x64-ubuntu-16.04 z3
-ENV PATH=/home/user/z3/bin:$PATH
-
-ARG HLINT=3.2
-RUN    cd /home/user \
-    && curl https://github.com/ndmitchell/hlint/releases/download/v$HLINT/hlint-$HLINT-x86_64-linux.tar.gz -sSfL | tar xzf - \
-    && mv hlint-$HLINT hlint
-ENV PATH=/home/user/hlint:$PATH
-
-ARG STYLISH_HASKELL=0.11.0.0
-RUN    cd /home/user \
-    && curl https://github.com/jaspervdj/stylish-haskell/releases/download/v$STYLISH_HASKELL/stylish-haskell-v$STYLISH_HASKELL-linux-x86_64.tar.gz -sSfL | tar xzf - \
-    && mv stylish-haskell-v$STYLISH_HASKELL-linux-x86_64 stylish-haskell
-ENV PATH=/home/user/stylish-haskell:$PATH
-
-ADD --chown=user:user stack.yaml /home/user/.tmp-haskell/
-ADD --chown=user:user kore/package.yaml /home/user/.tmp-haskell/kore/
-RUN    cd /home/user/.tmp-haskell \
-    && stack build --only-snapshot --test --bench --haddock
+ADD --chown=user:user stack.yaml .tmp-haskell/
+ADD --chown=user:user kore/package.yaml .tmp-haskell/kore/
+RUN cd .tmp-haskell && stack build --only-snapshot --test --bench --haddock

Jenkinsfile

@@ -1,7 +1,8 @@
 pipeline {
   agent {
     dockerfile {
-      additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+      label 'docker'
+      additionalBuildArgs '--build-arg K_COMMIT=$(cat deps/k_release | cut --delimiter="-" --field="2") --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
     }
   }
   options {
@@ -19,13 +20,6 @@ pipeline {
         }
       }
     }
-    stage('Check') {
-      steps {
-        sh '''
-          ./scripts/check.sh
-        '''
-      }
-    }
     stage('Dependencies') {
       steps {
         sh '''

README.md

@@ -52,8 +52,16 @@ in addition to the requirements and recommendations below.
 For integration testing, we require:
 
 - GNU [make]
-- The [K Framework] frontend, or [curl] to fetch an appropriate version.
-  The frontend has other dependencies, most notably a Java runtime.
+- The [K Framework] frontend.
+
+Instead of installing the frontend, you can use our `Dockerfile`
+to run the integration tests inside a container.
+Use `docker.sh` to run commands inside the container:
+
+``` sh
+./docker/build.sh  # run once when dependencies change
+./docker/run.sh make ...
+```
 
 ### Recommended dependencies
 

deps/k_release

@@ -1 +1 @@
-v5.0.0-2440f2e
+v5.0.0-c305b58

docker/build.sh

@@ -0,0 +1,2 @@
+#!/usr/bin/env bash
+docker build --build-arg K_COMMIT=$(cat deps/k_release | cut --delimiter="-" --field="2") --build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g) -t kore .

docker/run.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+# Run command in Docker
+docker run --rm --mount src=$(pwd),target=/home/user/kore,type=bind --workdir=/home/user/kore kore "$@"

include.mk

@@ -11,20 +11,13 @@ export TOP  # so that sub-makes do not invoke git again
 UPSTREAM_BRANCH = origin/master
 
 BUILD_DIR = $(TOP)/.build
-K_RELEASE_TAR = $(BUILD_DIR)/k-nightly.tar.gz
-K_RELEASE_TAR_URL = https://github.com/kframework/k/releases/download/$(shell cat $(TOP)/deps/k_release)/k-nightly.tar.gz
-K_RELEASE_DEFAULT = $(BUILD_DIR)/k
-K_RELEASE ?= $(K_RELEASE_DEFAULT)
-K_RELEASE_BIN = $(K_RELEASE)/bin
-K_RELEASE_LIB = $(K_RELEASE)/lib
 
 # The kernel JAR is used as a build timestamp.
-K = $(K_RELEASE_LIB)/kframework/java/kernel-1.0-SNAPSHOT.jar
-KOMPILE = $(K_RELEASE_BIN)/kompile
-KRUN = $(K_RELEASE_BIN)/krun
+KOMPILE = kompile
+KRUN = krun
 export KRUN
-KPROVE = $(K_RELEASE_BIN)/kprove
-KBMC = $(K_RELEASE_BIN)/kbmc
+KPROVE = kprove
+KBMC = kbmc
 
 KOMPILE_OPTS = --backend haskell
 KRUN_OPTS = --haskell-backend-command $(KORE_EXEC)
@@ -34,8 +27,6 @@ export KPROVE_OPTS
 KPROVE_REPL_OPTS = --haskell-backend-command $(KORE_REPL)
 export KPROVE_REPL_OPTS
 
-HS_TOP = $(TOP)/kore
-HS_SOURCE_DIRS = $(HS_TOP)/src $(HS_TOP)/app $(HS_TOP)/test $(HS_TOP)/bench
 STACK_BUILD = build --pedantic $(STACK_BUILD_OPTS)
 
 STACK = stack --allow-different-user
@@ -48,7 +39,7 @@ export KORE_PARSER
 export KORE_PARSER_OPTS
 
 KORE_EXEC = $(BUILD_DIR)/kore/bin/kore-exec
-KORE_EXEC_OPTS =
+KORE_EXEC_OPTS = --no-bug-report
 export KORE_EXEC
 export KORE_EXEC_OPTS
 
@@ -65,14 +56,3 @@ $(KORE_REPL):
 
 $(KORE_PARSER):
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-parser
-
-$(K_RELEASE_DEFAULT)/lib/kframework/java/kernel-1.0-SNAPSHOT.jar:
-	mkdir -p $(BUILD_DIR)
-	rm -rf $(K_RELEASE_DEFAULT) $(K_RELEASE_TAR)
-	curl --location --output $(K_RELEASE_TAR) $(K_RELEASE_TAR_URL)
-	mkdir -p $(K_RELEASE_DEFAULT)
-	tar --extract --file $(K_RELEASE_TAR) --strip-components 1 --directory $(K_RELEASE_DEFAULT)
-	cp $(TOP)/src/main/kore/prelude.kore $(K_RELEASE_DEFAULT)/include/kore
-	rm $(K_RELEASE_DEFAULT)/bin/kore*
-	$(KRUN) --version
-	test -f $@