From 1df6371e460a7f46fa2fbda42cc34afa100d5b79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Wed, 23 Aug 2023 17:21:02 +0200 Subject: [PATCH 1/2] Fixing incorrect passing proof reporting (#2024) * Fixing incorrect passing proof reporting * Set Version: 1.0.264 * simplifications * one import fewer * Set Version: 1.0.265 * Set Version: 1.0.266 * Set Version: 1.0.267 * Set Version: 1.0.268 * Set Version: 1.0.269 * Set Version: 1.0.270 * Set Version: 1.0.271 * Set Version: 1.0.272 * Set Version: 1.0.273 * Set Version: 1.0.274 * correcting the resume_proof test * formatting --------- Co-authored-by: devops Co-authored-by: rv-jenkins Co-authored-by: Everett Hildenbrandt --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/utils.py | 17 ++++------------- .../src/tests/integration/test_foundry_prove.py | 7 ++++++- package/debian/changelog | 2 +- package/version | 2 +- 5 files changed, 13 insertions(+), 17 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 9828d4b9c9..61920dfa0a 100644 --- 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.273" +version = "1.0.274" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index c16af8d466..31a34392b2 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -21,7 +21,6 @@ from pyk.kore.rpc import KoreClient, KoreExecLogFormat, kore_server from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver from pyk.proof.equality import EqualityProof, EqualityProver -from pyk.proof.proof import ProofStatus from pyk.utils import single if TYPE_CHECKING: @@ -125,8 +124,7 @@ def kevm_prove( cut_point_rules=cut_point_rules, ) assert isinstance(proof, APRProof) - failure_nodes = proof.failing - if len(failure_nodes) == 0: + if proof.passed: _LOGGER.info(f'Proof passed: {proof.id}') return True else: @@ -134,15 +132,15 @@ def kevm_prove( return False elif type(prover) is EqualityProver: prover.advance_proof() - if prover.proof.status == ProofStatus.PASSED: + if prover.proof.passed: _LOGGER.info(f'Proof passed: {prover.proof.id}') return True - if prover.proof.status == ProofStatus.FAILED: + elif prover.proof.failed: _LOGGER.error(f'Proof failed: {prover.proof.id}') if type(proof) is EqualityProof: _LOGGER.info(proof.pretty(kprove)) return False - if prover.proof.status == ProofStatus.PENDING: + else: _LOGGER.info(f'Proof pending: {prover.proof.id}') return False return False @@ -150,13 +148,6 @@ def kevm_prove( except Exception as e: _LOGGER.error(f'Proof crashed: {proof.id}\n{e}', exc_info=True) return False - failure_nodes = proof.pending + proof.failing - if len(failure_nodes) == 0: - _LOGGER.info(f'Proof passed: {proof.id}') - return True - else: - _LOGGER.error(f'Proof failed: {proof.id}') - return False def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> list[str]: diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index d4789c0d04..bdca38a6f4 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py @@ -328,7 +328,9 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update: def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) -> None: + foundry = Foundry(foundry_root) test_id = 'AssumeTest.test_assume_false(uint256,uint256)' + prove_res = foundry_prove( foundry_root, tests=[test_id], @@ -338,7 +340,10 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) max_iterations=4, reinit=True, ) - assert_pass(test_id, prove_res) + + proof = foundry.get_apr_proof(test_id) + assert proof.pending + prove_res = foundry_prove( foundry_root, tests=[test_id], diff --git a/package/debian/changelog b/package/debian/changelog index 8e43842b35..7d449a6795 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.273) unstable; urgency=medium +kevm (1.0.274) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 3b931e1bcc..2a443d2a01 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.273 +1.0.274 From f3aa859ae90c08b7d37ffe9e051e37d174d1c695 Mon Sep 17 00:00:00 2001 From: Freeman <105403280+F-WRunTime@users.noreply.github.com> Date: Wed, 23 Aug 2023 15:21:54 -0600 Subject: [PATCH 2/2] Setting fetch-depth (#2031) * Setting fetch-depth * Set Version: 1.0.273 * Set Version: 1.0.275 * Resolve possible future issues on recursive checkouts of submodules --------- Co-authored-by: devops --- .github/workflows/master-push.yml | 3 +++ .github/workflows/test-pr.yml | 4 ++++ .github/workflows/update-foundry-prove.yml | 1 + .github/workflows/update-version.yml | 1 + kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 3 ++- package/version | 2 +- 7 files changed, 13 insertions(+), 3 deletions(-) diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml index 65665d2fcf..0a8d9f0d9f 100644 --- a/.github/workflows/master-push.yml +++ b/.github/workflows/master-push.yml @@ -23,6 +23,7 @@ jobs: uses: actions/checkout@v3 with: ref: ${{ github.event.push.head.sha }} + fetch-depth: 0 - name: 'Upgrade bash' if: ${{ contains(matrix.os, 'macos') }} run: brew install bash @@ -61,6 +62,7 @@ jobs: with: submodules: recursive ref: ${{ github.event.push.head.sha }} + fetch-depth: 0 - name: 'Set up Docker' uses: ./.github/actions/with-docker with: @@ -119,6 +121,7 @@ jobs: uses: actions/checkout@v3 with: ref: ${{ github.event.push.head.sha }} + fetch-depth: 0 - name: 'Make Release' env: GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }} diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index ead1de3413..745e112265 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -56,6 +56,7 @@ jobs: uses: actions/checkout@v3 with: submodules: true + fetch-depth: 0 - name: 'Install Poetry' uses: Gr1N/setup-poetry@v8 - name: 'Build kevm' @@ -136,6 +137,7 @@ jobs: uses: actions/checkout@v3 with: submodules: recursive + fetch-depth: 0 - name: 'Set up Docker' uses: ./.github/actions/with-docker with: @@ -157,6 +159,7 @@ jobs: uses: actions/checkout@v3 with: submodules: recursive + fetch-depth: 0 - name: 'Set up Docker' uses: ./.github/actions/with-docker with: @@ -182,6 +185,7 @@ jobs: uses: actions/checkout@v3 with: submodules: recursive + fetch-depth: 0 - name: 'Set up Docker' uses: ./.github/actions/with-docker with: diff --git a/.github/workflows/update-foundry-prove.yml b/.github/workflows/update-foundry-prove.yml index 83beb6f23d..192c935ee1 100644 --- a/.github/workflows/update-foundry-prove.yml +++ b/.github/workflows/update-foundry-prove.yml @@ -16,6 +16,7 @@ jobs: submodules: recursive token: ${{ secrets.JENKINS_GITHUB_PAT }} ref: ${{ github.events.inputs.branch }} + fetch-depth: 0 - name: 'Configure GitHub user' run: | git config user.name devops diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml index b96cb9f354..3464faf97b 100644 --- a/.github/workflows/update-version.yml +++ b/.github/workflows/update-version.yml @@ -21,6 +21,7 @@ jobs: with: submodules: recursive token: ${{ secrets.JENKINS_GITHUB_PAT }} + fetch-depth: 0 - name: 'Configure GitHub user' run: | git config user.name devops diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 61920dfa0a..d84b9f2755 100644 --- 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.274" +version = "1.0.275" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 7d449a6795..0fda15eb33 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,5 +1,6 @@ -kevm (1.0.274) unstable; urgency=medium +kevm (1.0.275) unstable; urgency=medium * Initial Release. -- Everett Hildenbrandt Tue, 16 Jul 2019 00:14:12 -0700 + \ No newline at end of file diff --git a/package/version b/package/version index 2a443d2a01..16e372fe1d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.274 +1.0.275