From 9d457e4053d34b7fd9af48e88389569d3f1b879e Mon Sep 17 00:00:00 2001 From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com> Date: Mon, 25 Aug 2025 15:07:56 -0700 Subject: [PATCH 1/5] chore: bump dafny version --- StandardLibrary/runtimes/python/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StandardLibrary/runtimes/python/pyproject.toml b/StandardLibrary/runtimes/python/pyproject.toml index 72d531713..e758c983f 100644 --- a/StandardLibrary/runtimes/python/pyproject.toml +++ b/StandardLibrary/runtimes/python/pyproject.toml @@ -18,7 +18,7 @@ include = [ python = "^3.11.0" pytz = ">=2023.3.post1, <2026.0.0" # TODO: Longer-term, write something to pull this in from the project's project.properties file -DafnyRuntimePython = "4.9.0" +DafnyRuntimePython = "4.11.0" # Package testing From 56e9925719826ec3d9f28d2f04547bf9f9f71c96 Mon Sep 17 00:00:00 2001 From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com> Date: Tue, 23 Sep 2025 14:31:11 -0700 Subject: [PATCH 2/5] dafny runtime python --- .github/workflows/check_dafny_runtime_versions.yml | 4 ++-- project.properties | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/check_dafny_runtime_versions.yml b/.github/workflows/check_dafny_runtime_versions.yml index 1ab75e7f4..f5f015965 100644 --- a/.github/workflows/check_dafny_runtime_versions.yml +++ b/.github/workflows/check_dafny_runtime_versions.yml @@ -24,8 +24,8 @@ jobs: # Normalize by removing `.postN` if present normalized_dafny_runtime_python_version=$(echo "$dafny_runtime_python_version" | sed 's/\.post[0-9]*$//') - # Extract the version from project.properties - dafny_version=$(grep -oP 'dafnyVersion=\K[^\s]+' project.properties) + # Extract the Dafny Runtime Python Version from project.properties + dafny_version=$(grep -oP 'dafnyRuntimePythonVersion=\K[^\s]+' project.properties) # Check if the versions match if [ "$normalized_dafny_runtime_python_version" != "$dafny_version" ]; then diff --git a/project.properties b/project.properties index 5d11f69e2..bc46e929a 100644 --- a/project.properties +++ b/project.properties @@ -7,5 +7,6 @@ # And the Dotnet projects include and parse this file. dafnyVersion=4.9.0 dafnyVerifyVersion=4.9.1 +dafnyRuntimePythonVersion=4.11.0 dafnyRustVersion=nightly-2025-01-30-7db1e5f mplVersion=1.11.1-SNAPSHOT From 486e65de188745982f709eb00c56cde87217148c Mon Sep 17 00:00:00 2001 From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com> Date: Wed, 24 Sep 2025 11:45:56 -0700 Subject: [PATCH 3/5] enforcement step --- .../check_dafny_runtime_versions.yml | 30 +++++++++++++++++-- project.properties | 3 ++ 2 files changed, 31 insertions(+), 2 deletions(-) diff --git a/.github/workflows/check_dafny_runtime_versions.yml b/.github/workflows/check_dafny_runtime_versions.yml index f5f015965..9db298e13 100644 --- a/.github/workflows/check_dafny_runtime_versions.yml +++ b/.github/workflows/check_dafny_runtime_versions.yml @@ -1,7 +1,6 @@ # Checks that DafnyRuntimePython version in StandardLibrary's pyproject.toml # matches the Dafny version in project.properties. -# .toml is static and cannot load this automatically. -# This must be bumped manually. +# Also enforces review of dafnyRuntimePythonVersion when dafnyVersion is changed. name: Check DafnyRuntimePython Version Consistency on: @@ -16,6 +15,33 @@ jobs: steps: - uses: actions/checkout@v4 + with: + fetch-depth: 0 + + # TODO: Remove this entire step when dafnyRuntimePythonVersion is deleted from project.properties + - name: Enforce dafnyVersion review (PR only) + if: github.event_name == 'pull_request' + run: | + BASE_SHA="${{ github.event.pull_request.base.sha }}" + HEAD_SHA="${{ github.event.pull_request.head.sha }}" + + # Check if dafnyVersion was changed + if git diff "$BASE_SHA" "$HEAD_SHA" -- project.properties | grep -q "^[+-]dafnyVersion="; then + # Check if dafnyRuntimePythonVersion was also changed + if ! git diff "$BASE_SHA" "$HEAD_SHA" -- project.properties | grep -q "^[+-]dafnyRuntimePythonVersion="; then + echo "ERROR: dafnyVersion was changed but dafnyRuntimePythonVersion was not reviewed." + echo "" + echo "Required action (choose one):" + echo "1. PREFERRED: Delete the dafnyRuntimePythonVersion line entirely if the new Dafny version is compatible" + echo "2. Update dafnyRuntimePythonVersion to a compatible version" + echo "3. Keep the same value but add a comment explaining why (e.g., '# Keeping 4.11.0 due to compatibility issues')" + echo "" + echo "This ensures conscious review of the temporary Python runtime workaround." + echo "NOTE: When dafnyRuntimePythonVersion is removed, also remove this enforcement step." + exit 1 + fi + fi + - name: Validate DafnyRuntimePython Version Consistency run: | # Extract the version from pyproject.toml diff --git a/project.properties b/project.properties index bc46e929a..c1543c47f 100644 --- a/project.properties +++ b/project.properties @@ -7,6 +7,9 @@ # And the Dotnet projects include and parse this file. dafnyVersion=4.9.0 dafnyVerifyVersion=4.9.1 +# TEMPORARY WORKAROUND: When updating dafnyVersion, try to REMOVE this property first. +# Only keep if the new Dafny version has Python runtime compatibility issues. +# GitHub workflow will enforce this review. Goal: remove this entirely. dafnyRuntimePythonVersion=4.11.0 dafnyRustVersion=nightly-2025-01-30-7db1e5f mplVersion=1.11.1-SNAPSHOT From 37e1c8673fa8eebb6e0178cd7730b0fc3016ad48 Mon Sep 17 00:00:00 2001 From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com> Date: Wed, 24 Sep 2025 11:50:29 -0700 Subject: [PATCH 4/5] format --- .github/workflows/check_dafny_runtime_versions.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/check_dafny_runtime_versions.yml b/.github/workflows/check_dafny_runtime_versions.yml index 9db298e13..d7c46f3f7 100644 --- a/.github/workflows/check_dafny_runtime_versions.yml +++ b/.github/workflows/check_dafny_runtime_versions.yml @@ -24,7 +24,7 @@ jobs: run: | BASE_SHA="${{ github.event.pull_request.base.sha }}" HEAD_SHA="${{ github.event.pull_request.head.sha }}" - + # Check if dafnyVersion was changed if git diff "$BASE_SHA" "$HEAD_SHA" -- project.properties | grep -q "^[+-]dafnyVersion="; then # Check if dafnyRuntimePythonVersion was also changed From bda80129e201e779c5331d6353dddb467c37a408 Mon Sep 17 00:00:00 2001 From: Darwin Chowdary <39110935+imabhichow@users.noreply.github.com> Date: Wed, 24 Sep 2025 11:54:55 -0700 Subject: [PATCH 5/5] format --- .github/workflows/check_dafny_runtime_versions.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/check_dafny_runtime_versions.yml b/.github/workflows/check_dafny_runtime_versions.yml index d7c46f3f7..3578ecedb 100644 --- a/.github/workflows/check_dafny_runtime_versions.yml +++ b/.github/workflows/check_dafny_runtime_versions.yml @@ -1,6 +1,7 @@ # Checks that DafnyRuntimePython version in StandardLibrary's pyproject.toml # matches the Dafny version in project.properties. -# Also enforces review of dafnyRuntimePythonVersion when dafnyVersion is changed. +# .toml is static and cannot load this automatically. +# This must be bumped manually. name: Check DafnyRuntimePython Version Consistency on: