Simplify testing, make failing lists explicit (#2082)

* tests/failing-symbolic.haskell-dry-run: remove old list * tests/failing.haskell: remove unused list * tests/slow.haskell: remove unused list * kevm-pyk/Makefile: standard variable names for controlling test harnesses * kevm-pyk/pyproject.toml: add pytest-timeout * tests/failing-symbolic.pyk: add failing-symbolic tests to pyk list too, sort * kevm-pyk/test_prove, tests/{failing,slow}: propogate failing test lists forward, remove slow test list * kevm-pyk/tests/test_prove: test lists are complete independently now * Makefile: separate out pyk/legacy proof steps * .github/test-pr: adjust PR job * Makefile: correct pytest invocations * kevm-pyk/pyproject.toml: update with pytest-timeout plugin * Makefile: remove direct use of PYTEST_PARALLEL * Makefile: remove explicit setting of PYTEST args in toplevel makefile * Set Version: 1.0.298 * Makefile, kevm-pyk/tests/test_prove: legacy => kprove * .github/test-pr: correct docker image name * .github/test-pr: simplify CI job a bit * .github/test-pr: factor out foundry tests into matrix too * .github/test-pr: typo * .github/test-pr: build kevm-pyk before building haskell backend * .github/: consistent ${GITHUB_SHA} => ${{ github.sha }} everywhere * .github/test-pr: unique name for each foundry testing backend container * .github/test-pr: more compact matrix specs * .github/test-pr: keep running tests in matrices if any fail * .github/test-pr: update stage timings, 1.5x runtime + 15min * Set Version: 1.0.299 * .github/test-pr: adjust timeouts * Set Version: 1.0.300 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Sep 21, 2023 · 8f4a32a · 8f4a32a
1 parent 4085431
commit 8f4a32a
Show file tree

Hide file tree

Showing 16 changed files with 240 additions and 493 deletions.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -69,7 +69,7 @@ jobs:
         run: |
           set -x
           kevm_version=v$(cat package/version)
-          gh release create "${kevm_version}" --target "${GITHUB_SHA}"
+          gh release create "${kevm_version}" --target "${{ github.sha }}"
 
   gh-pages:
     name: 'Publish GH Pages'

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -81,16 +81,16 @@ jobs:
         with:
           container-name: kevm-ci-profile-${{ github.sha }}
       - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make poetry'
+        run: docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
+        run: docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
       - name: 'Run profiling'
         run: |
-          docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make profile'
+          docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'make profile'
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kevm-ci-profile-${GITHUB_SHA}
+          docker stop --time=0 kevm-ci-profile-${{ github.sha }}
 
   test-concrete-execution:
     name: 'Build and Test KEVM concrete execution'
@@ -108,51 +108,38 @@ jobs:
         with:
           container-name: kevm-ci-concrete-${{ github.sha }}
       - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make poetry'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin llvm haskell'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin llvm haskell'
       - name: 'Test integration'
-        run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-integration'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
-        run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-conformance'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-conformance'
       - name: 'Test llvm krun'
-        run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-interactive'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-interactive'
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kevm-ci-concrete-${GITHUB_SHA}
+          docker stop --time=0 kevm-ci-concrete-${{ github.sha }}
 
-  test-prove-haskell:
-    name: 'Build and Test KEVM haskell proofs'
+  test-prove:
+    name: 'Build and Test KEVM proofs'
     needs: kevm-pyk-code-quality-checks
     runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 120
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-          fetch-depth: 0
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
-        with:
-          container-name: kevm-ci-haskell-${{ github.sha }}
-      - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make poetry'
-      - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell'
-      - name: 'Prove Haskell'
-        run: docker exec -u github-user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove PYTEST_ARGS=-vv'
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-haskell-${GITHUB_SHA}
-
-  test-prove-haskell-booster:
-    name: 'Build and Test KEVM haskell proofs (booster)'
-    needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 150
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - test-suite: 'test-prove-kprove'
+            test-args:
+            timeout: 90
+          - test-suite: 'test-prove-pyk'
+            test-args:
+            timeout: 90
+          - test-suite: 'test-prove-pyk'
+            test-args: '--use-booster'
+            timeout: 60
+    timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -161,49 +148,33 @@ jobs:
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kevm-ci-haskell-booster-${{ github.sha }}
+          container-name: kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
       - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-haskell-booster-${GITHUB_SHA} /bin/bash -c 'make poetry'
-      - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-haskell-booster-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
+      - name: 'Build distribution'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell'
       - name: 'Prove Haskell'
-        run: docker exec -u github-user kevm-ci-haskell-booster-${GITHUB_SHA} /bin/bash -c 'make test-prove PYTEST_ARGS="-vv --use-booster"'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}'"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kevm-ci-haskell-booster-${GITHUB_SHA}
+          docker stop --time=0 kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
 
   test-prove-foundry:
     name: 'Build and Test KEVM Foundry proofs'
     needs: kevm-pyk-code-quality-checks
     runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 150
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-          fetch-depth: 0
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
-        with:
-          container-name: kevm-ci-foundry-${{ github.sha }}
-      - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make poetry'
-      - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
-      - name: 'Foundry Prove'
-        run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS=-vv'
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-foundry-${GITHUB_SHA}
-
-  test-prove-foundry-booster:
-    name: 'Build and Test KEVM Foundry proofs (booster)'
-    needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 150
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - test-suite: 'legacy'
+            test-args:
+            timeout: 240
+          - test-suite: 'booster'
+            test-args: '--use-booster'
+            timeout: 90
+    timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -213,17 +184,17 @@ jobs:
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kevm-ci-booster-${{ github.sha }}
+          container-name: kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }}
       - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make poetry'
+        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
+        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
       - name: 'Foundry Prove'
-        run: docker exec -u github-user kevm-ci-booster-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS="-vv --use-booster"'
+        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make test-foundry-prove PYTEST_ARGS='-vv ${{ matrix.test-args }}'"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kevm-ci-booster-${GITHUB_SHA}
+          docker stop --time=0 kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }}
 
   nix:
     name: 'Nix'

diff --git a/.github/workflows/update-foundry-prove.yml b/.github/workflows/update-foundry-prove.yml
@@ -36,21 +36,21 @@ jobs:
           CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
         run: cachix watch-exec k-framework -- nix build --extra-experimental-features 'nix-command flakes' .#devShell.x86_64-linux.inputDerivation --no-link
       - name: 'Build k-deps'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make k-deps'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make k-deps'
       - name: 'Build blockchain-k-plugin-deps'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make plugin-deps'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make plugin-deps'
       - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make poetry'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build evm-semantics'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make build'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make build'
       - name: 'Build Foundry'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make build-foundry -j2'
       - name: 'Foundry Prove Update'
-        run: docker exec -u github-user kevm-update-output-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove FOUNDRY_PAR=8 PYTEST_ARGS+="--use-booster --update-expected-output"'
+        run: docker exec -u github-user kevm-update-output-${{ github.sha }} /bin/bash -c 'make test-foundry-prove FOUNDRY_PAR=8 PYTEST_ARGS+="--use-booster --update-expected-output"'
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kevm-update-output-${GITHUB_SHA}
+          docker stop --time=0 kevm-update-output-${{ github.sha }}
       - name: 'Commit changes'
         run: |
           git add kevm-pyk/src/tests/integration/test-data/show/ && git commit --allow-empty -m "test-data/show/: update expected show output" || true

diff --git a/Makefile b/Makefile
@@ -27,40 +27,41 @@ kevm-pyk: poetry-env
 # Tests
 # -----
 
-test: test-integration test-conformance test-prove test-interactive
+test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-interactive
 
 
 # Foundry Tests
 
-PYTEST_PARALLEL := 8
-PYTEST_ARGS     :=
-
 test-foundry-prove: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_foundry_prove.py -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
-
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_foundry_prove.py"
 
 # Conformance Tests
 
 test-conformance: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_conformance.py -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_conformance.py"
 
 test-vm: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_vm -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_vm"
 
 test-rest-vm: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_rest_vm -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_rest_vm"
 
 test-bchain: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_bchain -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_bchain"
 
 test-rest-bchain: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_rest_bchain -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_rest_bchain"
 
 
 # Proof Tests
 
-test-prove: tests/specs/opcodes/evm-optimizations-spec.md poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_prove -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
+test-prove: test-prove-pyk test-prove-kprove
+
+test-prove-pyk: tests/specs/opcodes/evm-optimizations-spec.md poetry
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_pyk_prove"
+
+test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_kprove_prove"
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
 tests/specs/opcodes/evm-optimizations-spec.md:
@@ -70,10 +71,10 @@ tests/specs/opcodes/evm-optimizations-spec.md:
 # Integration Tests
 
 test-integration: poetry
-	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+='-k "(test_kast.py or test_run.py or test_solc_to_k.py)" -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)'
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+='-k "(test_kast.py or test_run.py or test_solc_to_k.py)"'
 
 profile: poetry
-	$(MAKE) -C kevm-pyk/ profile PROF_ARGS+='-n$(PYTEST_PARALLEL) $(PYTEST_ARGS)'
+	$(MAKE) -C kevm-pyk/ profile
 	find /tmp/pytest-of-$$(whoami)/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
 
 

diff --git a/kevm-pyk/Makefile b/kevm-pyk/Makefile
@@ -22,18 +22,21 @@ poetry-install:
 
 # Tests
 
-TEST_ARGS :=
+PYTEST_BASE_ARGS := --verbose --durations=0 --dist=worksteal
+PYTEST_ARGS      :=
+PYTEST_PARALLEL  := 8
+PYTEST_MAXFAIL   := 1
 
 test: test-all
 
 test-all: poetry-install
-	$(POETRY_RUN) pytest src/tests --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+	$(POETRY_RUN) pytest src/tests $(PYTEST_BASE_ARGS) --maxfail=$(PYTEST_MAXFAIL) --numprocesses=$(PYTEST_PARALLEL) $(PYTEST_ARGS)
 
 test-unit: poetry-install
-	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
+	$(POETRY_RUN) pytest src/tests/unit $(PYTEST_BASE_ARGS) --maxfail=$(PYTEST_MAXFAIL) --numprocesses=$(PYTEST_PARALLEL) $(PYTEST_ARGS)
 
 test-integration: poetry-install
-	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+	$(POETRY_RUN) pytest src/tests/integration $(PYTEST_BASE_ARGS) --maxfail=$(PYTEST_MAXFAIL) --numprocesses=$(PYTEST_PARALLEL) $(PYTEST_ARGS)
 
 
 # Coverage

diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.299"
+version = "1.0.300"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -33,6 +33,7 @@ isort = "*"
 mypy = "*"
 pep8-naming = "*"
 pytest = "*"
+pytest-timeout = "*"
 pytest-cov = "*"
 pytest-mock = "*"
 pytest-xdist = "*"

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.299'
+VERSION: Final = '1.0.300'
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.299'
		VERSION: Final = '1.0.300'