Run integration tests with Nix (#2492)

* Makefile: Do not automatically rebuild backend

Automatically rebuilding the backend makes it impossible to test an out-of-tree
build with the Makefile.

* test.nix: Run integration tests in Nix

* test.yml: Run integration tests on Linux separately

* test.nix: Override backend in kframework/k

Co-authored-by: rv-jenkins <[email protected]>

Author: ttuegel

.github/workflows/test.yml

@@ -52,6 +52,35 @@ jobs:
       - name: Check shell
         run: nix-shell --run "echo OK"
 
+  nix-integration:
+    name: 'Nix / Integration'
+    runs-on: ubuntu-latest
+    needs: nix
+    steps:
+      - name: Check out code
+        uses: actions/[email protected]
+        with:
+          # Check out pull request HEAD instead of merge commit.
+          ref: ${{ github.event.pull_request.head.sha }}
+          submodules: recursive
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          extra_nix_config: |
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: Install Cachix
+        uses: cachix/cachix-action@v8
+        with:
+          name: kore
+          skipPush: true
+          extraPullNames: runtimeverification
+
+      - name: Run integration tests
+        run: nix-build test.nix
+
   cabal:
     name: 'Cabal'
     runs-on: ubuntu-latest

README.md

@@ -60,6 +60,7 @@ Use `docker.sh` to run commands inside the container:
 
 ``` sh
 ./docker/build.sh  # run once when dependencies change
+./docker/run.sh make  # build the backend
 ./docker/run.sh make test  # run all tests
 ./docker/run.sh make -C test/imp test  # run all tests in test/imp
 ```
@@ -116,6 +117,13 @@ When the `.cabal` package description file changes, run:
 
 This script is also run by an automatic workflow.
 
+We provide a `test.nix` for running integration tests:
+
+``` sh
+nix-build test.nix  # run all integration tests
+nix-build test.nix --argstr test imp  # run the integration tests in test/imp
+nix-shell test.nix  # enter a shell where we can run tests manually
+```
 
 [git]: https://git-scm.com/
 [stack]: https://www.haskellstack.org/

include.mk

@@ -48,11 +48,11 @@ KORE_REPL_OPTS = --no-bug-report
 export KORE_REPL
 export KORE_REPL_OPTS
 
-$(KORE_EXEC):
+$(BUILD_DIR)/kore/bin/kore-exec:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-exec
 
-$(KORE_REPL):
+$(BUILD_DIR)/kore/bin/kore-repl:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-repl
 
-$(KORE_PARSER):
+$(BUILD_DIR)/kore/bin/kore-parser:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-parser

test.nix

@@ -0,0 +1,74 @@
+let
+  sources = import ./nix/sources.nix;
+  pinned = import sources."nixpkgs" { config = {}; overlays = []; };
+in
+
+{ pkgs ? pinned
+, test ? null
+}:
+
+let
+  inherit (pkgs) stdenv lib;
+  inherit (pkgs) bison diffutils ncurses z3;
+
+  ttuegel =
+    let
+      src = builtins.fetchGit {
+        url = "https://github.com/ttuegel/nix-lib";
+        rev = "66bb0ab890ff4d828a2dcfc7d5968465d0c7084f";
+        ref = "main";
+      };
+    in import src { inherit pkgs; };
+
+  default = import ./. {};
+  inherit (default) kore;
+
+  kframework =
+    let
+      tag = lib.fileContents ./deps/k_release;
+      url = "https://github.com/kframework/k/releases/download/${tag}/release.nix";
+      args = import (builtins.fetchurl { inherit url; });
+      src = pkgs.fetchgit args;
+    in import src {};
+
+  k = kframework.k.override {
+    haskell-backend = kore;
+  };
+
+in
+
+stdenv.mkDerivation {
+  name = "kore-test";
+  src = ttuegel.cleanGitSubtree { name = "kore"; src = ./.; };
+  preferLocalBuild = true;
+  buildInputs = [
+    k kore  # some tests use kore-exec directly, others run through the frontend
+    ncurses  # TODO: .../lib/kframework/setenv: line 31: tput: command not found
+    z3
+  ];
+  configurePhase = ''
+    export TOP=$(pwd)
+  '';
+  buildFlags =
+    [
+      "KORE_PARSER=kore-parser"
+      "KORE_EXEC=kore-exec"
+      "KORE_REPL=kore-repl"
+      "--output-sync"
+      "test"
+    ]
+    ++ lib.optional (test != null) "-C ${test}"
+    ;
+  enableParallelBuilding = true;
+  preBuild = ''
+    cd test
+  '';
+  installPhase = ''
+    runHook preInstall
+
+    touch "$out"
+
+    runHook postInstall
+  '';
+}
+

test/include.mk

@@ -19,7 +19,7 @@ KOMPILED := $(TEST_DIR)/$(DEF)-kompiled
 export KOMPILED
 DEF_KORE_DEFAULT = $(KOMPILED)/definition.kore
 DEF_KORE ?= $(DEF_KORE_DEFAULT)
-TEST_DEPS = $(K) $(KORE_PARSER) $(DEF_KORE) $(KORE_EXEC)
+TEST_DEPS = $(K) $(DEF_KORE)
 
 TESTS = \
 	$(wildcard $(DEF_DIR)/*.verify) \
@@ -44,7 +44,7 @@ KORE_EXEC_OPTS += \
 KPROVE_REPL_OPTS += -d $(DEF_DIR) -m $(KPROVE_MODULE)
 KPROVE_SPEC = $<
 
-$(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K) $(KORE_PARSER)
+$(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K)
 	@echo ">>>" $(CURDIR) "kompile" $<
 	rm -fr $(KOMPILED)
 	$(KOMPILE) $(KOMPILE_OPTS) $<
@@ -112,10 +112,10 @@ PATTERN_OPTS = --pattern "$$(cat $*.k)"
 %.save-proofs.kore: %.out
 	[ -f $@ ]
 
-%-spec.k.repl: $(TEST_DIR)/%-spec.k $(KORE_REPL) $(TEST_DEPS)
+%-spec.k.repl: $(TEST_DIR)/%-spec.k $(TEST_DEPS)
 	$(KPROVE) $(KPROVE_REPL_OPTS) $<
 
-%-spec.k.run-repl-script: $(TEST_DIR)/%-spec.k $(KORE_REPL) $(TEST_DEPS)
+%-spec.k.run-repl-script: $(TEST_DIR)/%-spec.k $(TEST_DEPS)
 	$(KPROVE) $(KPROVE_REPL_OPTS) $<
 %-spec.k.run-repl-script: KORE_REPL_OPTS= -r --repl-script $@
 
@@ -133,15 +133,15 @@ PATTERN_OPTS = --pattern "$$(cat $*.k)"
 
 ### MERGE
 
-%.merge.out: $(TEST_DIR)/%.merge $(DEF_KORE) $(KORE_EXEC)
+%.merge.out: $(TEST_DIR)/%.merge $(DEF_KORE)
 	@echo ">>>" $(CURDIR) "kore-exec --merge-rules" $<
 	rm -f $@
 	$(KORE_EXEC) $(DEF_KORE) --module $(KORE_MODULE) --merge-rules $< --output $@
 	$(DIFF) $@.golden $@ || $(FAILED)
 
 ### SCRIPTS
 
-test-%.sh.out: $(KORE_EXEC) $(TEST_DIR)/test-%.sh
+test-%.sh.out: $(TEST_DIR)/test-%.sh
 	@echo ">>>" $(CURDIR) $(@:.out=)
 	rm -f $@
 	$(TEST_DIR)/$(@:.out=) > $@ || true

test/no-injection-into-hooked/Makefile

@@ -17,7 +17,7 @@ clean:
 
 .PHONY: test-k test golden clean
 
-test-kompiled/definition.kore: test.k $(K) $(KORE_PARSER)
+test-kompiled/definition.kore: test.k $(K)
 	@echo ">>>" $(CURDIR) "kompile" $<
 	rm -fr $(KOMPILED)
 	$(KOMPILE) $(KOMPILE_OPTS) $<; if [ $$? -eq 0 ]; then exit 1; fi

test/parser/Makefile

@@ -13,7 +13,7 @@ TESTS = $(wildcard *.kore)
 OUTS += $(foreach TEST, $(TESTS), $(TEST).out)
 GOLDEN += $(foreach TEST, $(TESTS), $(TEST).golden)
 
-%.kore.out : %.kore $(KORE_PARSER)
+%.kore.out : %.kore
 	$(KORE_PARSER) --no-print-definition $< 2>$@ || true
 	$(DIFF) $*.kore.golden $@ || $(FAILED)