Run integration tests using nix runner matrix

.github/workflows/test.yml

@@ -74,7 +74,7 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - runner: ubuntu-22.04
+          - runner: [self-hosted, linux, normal]
             os: ubuntu-22.04
             nix: x86_64-linux
           - runner: macos-12
@@ -114,6 +114,30 @@ jobs:
           name: k-framework
           authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
 
+      - uses: dorny/paths-filter@v3
+        id: changes
+        with:
+          filters: |
+            kore:
+              - 'kore/**'
+            kore_rpc_types:
+              - 'kore-rpc-types/**'
+            booster:
+              - 'booster/**'
+              - scripts/booster-integration-tests.sh
+            dev_tools:
+              - 'dev-tools/**'
+            project:
+              - 'stack.yaml*'
+              - 'cabal.project*'
+              - 'Makefile'
+              - '*.mk'
+              - 'flake.nix'
+              - 'deps/*'
+              - '.github/*'
+            kore_tests:
+              - 'test/**'
+
       - name: Build
         run: GC_DONT_GC=1 nix build .#kore-exec .#kore-rpc-booster
 
@@ -132,8 +156,25 @@ jobs:
             cabal-nix-${{ runner.os }}-ghc-${{ env.ghc_version }}
 
       - name: Test
+        if: ${{ steps.changes.outputs.booster == 'true' || steps.changes.outputs.kore == 'true' || steps.changes.outputs.project == 'true' }}
         run: GC_DONT_GC=1 nix develop .#cabal --command bash -c "hpack ./booster && hpack dev-tools && cabal update && cabal build all && cabal test --enable-tests --test-show-details=direct kore-test unit-tests"
 
+      - name: Run booster integration tests
+        # do not run this unless anything has changed in a relevant directory
+        if: ${{ matrix.runner != 'macos-12' && (steps.changes.outputs.booster == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.project == 'true') }}
+        env:
+          CONNECTION_ATTEMPTS: 30
+        run: |
+          GC_DONT_GC=1 nix develop .#cabal --command bash -c "scripts/booster-integration-tests.sh"
+
+      - name: Run kore integration tests
+        # do not run this unless anything has changed in a relevant directory
+        if: ${{ matrix.runner != 'macos-12' && (steps.changes.outputs.kore == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.kore_tests == 'true' || steps.changes.outputs.project == 'true') }}
+        run: |
+          GC_DONT_GC=1 nix develop github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
+                --override-input haskell-backend . --update-input haskell-backend \
+                --command bash -c "cd test && make -j2 --output-sync test"
+
   nix-integration:
     name: 'Nix / Integration'
     needs: formatting

test/include.mk

@@ -34,6 +34,11 @@ OUTS += $(foreach TEST, $(TESTS), $(TEST).out)
 GOLDEN += $(foreach OUT, $(OUTS), $(OUT).golden)
 
 KOMPILE_OPTS += --output-definition $(KOMPILED) -Wno unused-var -Wno missing-syntax-module
+
+ifeq "$(shell uname)" "Darwin"
+	KOMPILE_OPTS += --no-haskell-binary
+endif
+
 KRUN_OPTS += --definition $(KOMPILED)
 KORE_EXEC_OPTS += \
 	$(if $(STORE_PROOFS),\

test/serialized-definition/Makefile

@@ -2,26 +2,33 @@ include $(CURDIR)/../include.mk
 
 KORE_FILES=$(wildcard [a-z]*definition.kore)
 
+ifeq "$(shell uname)" "Darwin"
+.PHONY: test
+test:
+	@echo "Skipping serialization test on Mac OS"
+else
 test: $(addprefix test-,$(basename $(KORE_FILES)))
+endif
 
 MODULE=UNDEFINED-MODULE
 
 # lame solution: specify the --module $MODULE individually instead of grep|tail|sed
 test-a-to-f-definition: MODULE=TEST
-test-test-smoke-definition: MODULE=C
 test-test-totalSupply-definition: MODULE=VERIFICATION
 
 test-%: %.kore
 	@echo "Serializing definition $<"
-	time -f "%esec" $(KORE_EXEC) $< --output serialized.bin --module $(MODULE) --serialize
+	$(KORE_EXEC) $< --output serialized.bin --module $(MODULE) --serialize
 	@echo "Loading serialized definition (to hit an error afterwards)"
-	time -f "%esec" sh -c "$(KORE_EXEC) serialized.bin \
+	sh -c "$(KORE_EXEC) serialized.bin \
 		--module $(MODULE) \
 		--pattern serialized.bin \
 		--debug-rewrite FAIL-ME-PLEASE 2>&1 | \
 		grep FAIL-ME-PLEASE"
 	@rm serialized.bin
 
+.PHONY: clean
 clean:
+	rm -f serialized.bin
 
 golden: