From af8e6e32db8eac3b1843618bb59393b5469f53a3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 17 Apr 2024 11:29:22 +1000 Subject: [PATCH 1/4] add --no-haskell-binary option to integration test compilations on MacOS --- test/include.mk | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/test/include.mk b/test/include.mk index 851a9eb3b0..a45e9d94c6 100644 --- a/test/include.mk +++ b/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),\ From f31d9849e9957aefab2033b12d56a1465ca24daa Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 17 Apr 2024 13:16:00 +1000 Subject: [PATCH 2/4] Adjust serialisation test (skip it on Mac, avoid using time -f) --- test/serialized-definition/Makefile | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/test/serialized-definition/Makefile b/test/serialized-definition/Makefile index 7e9bc91b63..0161618b0a 100644 --- a/test/serialized-definition/Makefile +++ b/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: From da54dbc6912dc99991cfb66075b87854b436933d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 17 Apr 2024 11:29:46 +1000 Subject: [PATCH 3/4] TESTING: run integration tests using nix in matrix * use self-hosted linux runner * bump connection attempts for booster test * use path filters * run all integration tests when github setup changes * omit integration tests on macos-12 runner --- .github/workflows/test.yml | 43 +++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 449bfcc75d..c5542a1e83 100644 --- a/.github/workflows/test.yml +++ b/.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 From 4758f12c3bfe251ad542a1e74e1316534444ce71 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 17 Apr 2024 17:58:43 +1000 Subject: [PATCH 4/4] fix github path filter --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index c5542a1e83..4db9e28f72 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -134,7 +134,7 @@ jobs: - '*.mk' - 'flake.nix' - 'deps/*' - - '.github/' + - '.github/*' kore_tests: - 'test/**'