diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 924d325d815..1354126dbf5 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -1,13 +1,10 @@
-Fixes #
+
+### What was changed?
-
-
-
-
-
-
-
+### How has this been tested?
+
By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
diff --git a/.github/workflows/check-deep-tests-reusable.yml b/.github/workflows/check-deep-tests-reusable.yml
index c2c6e23dcd2..eb38ecebc98 100644
--- a/.github/workflows/check-deep-tests-reusable.yml
+++ b/.github/workflows/check-deep-tests-reusable.yml
@@ -1,28 +1,26 @@
name: Check Deep Tests (Reusable Workflow)
on:
+ workflow_dispatch:
workflow_call:
- inputs:
- sha:
- type: string
- branch:
- type: string
jobs:
check-deep-tests:
runs-on: ubuntu-20.04
steps:
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- - uses: actions/github-script@v6
+ - uses: actions/github-script@v7
if: github.repository_owner == 'dafny-lang'
with:
+ # Since nightly-build.yml always targets fixed branches now, rather than being parameterized by
+ # branch, we can't effectively check "for a specific branch".
+ # That means we have to be less precise for now and block all branches if any branch fails the deep nightly tests.
script: |
const script = require('${{ github.workspace }}/dafny/.github/workflows/check-for-workflow-run.js')
console.log(script({github, context, core,
- workflow_id: 'deep-tests.yml',
- ...('${{ inputs.sha }}' ? {sha: '${{ inputs.sha }}'} : {}),
- ...('${{ inputs.branch }}' ? {branch: '${{ inputs.branch }}'} : {})}))
+ workflow_id: 'nightly-build.yml',
+ branch: 'master'}))
diff --git a/.github/workflows/check-for-workflow-run.js b/.github/workflows/check-for-workflow-run.js
index e0a2ee1c766..f4b86dd90fb 100644
--- a/.github/workflows/check-for-workflow-run.js
+++ b/.github/workflows/check-for-workflow-run.js
@@ -14,16 +14,33 @@ module.exports = async ({github, context, core, workflow_id, sha, ...config}) =>
// These are ordered by creation time, so decide based on the first
// run for this SHA we see.
const runFilterDesc = sha ? `${workflow_id} on ${sha}` : workflow_id
- for (const run of result.data.workflow_runs) {
- if ((!sha || run.head_sha === sha) && run.status !== "in_progress") {
- if (run.conclusion !== "success") {
- core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}`)
- } else {
- // The SHA is fully tested, exit with success
- console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
- }
+ const workflow_runs = result.data.workflow_runs.filter(run => !sha || run.head_sha === sha)
+ const workflow_runs_completed = workflow_runs.filter(run => run.status === "completed")
+ // The status property can be one of: “queued”, “in_progress”, or “completed”.
+ const workflow_runs_in_progress = workflow_runs.filter(run => run.status !== "completed")
+ for (const run of workflow_runs_completed) {
+ // The conclusion property can be one of:
+ // “success”, “failure”, “neutral”, “cancelled”, “skipped”, “timed_out”, or “action_required”.
+ if (run.conclusion === "success") {
+ // The SHA is fully tested, exit with success
+ console.log(`Last run of ${runFilterDesc} succeeded: ${run.html_url}`)
+ return
+ } else if (run.conclusion === "failure" || run.conclusion === "timed_out") {
+ const extraMessage = workflow_runs_in_progress.length > 0 ?
+ `\nA run of ${runFilterDesc} is currently ${workflow_runs_in_progress[0].status}:`+
+ ` ${workflow_runs_in_progress[0].html_url}, just re-run this test once it is finished.` :
+ `\nAt the time of checking, no fix was underway.\n`+
+ `- Please first check https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml . `+
+ `If you see any queued or in progress run on ${runFilterDesc}, just re-run this test once it is finished.`+
+ `- If not, and you are a Dafny developer, please fix the issue by creating a PR with the label [run-deep-tests], have it reviewed and merged, ` +
+ `and then trigger the workflow on ${runFilterDesc} with the URL https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml .\n`+
+ `With such a label, you can merge a PR even if tests are not successful, but make sure the deeps one are!\n`+
+ `If you do not have any clue on how to fix it, `+
+ `at worst you can revert all PRs from the last successful run and indicate the authors they need to re-file`+
+ ` their PRs and add the label [run-deep-tests] to their PRs`;
+ core.setFailed(`Last run of ${runFilterDesc} did not succeed: ${run.html_url}${extraMessage}`)
return
}
}
- core.setFailed(`No runs of ${runFilterDesc} found!`)
+ core.setFailed(`No completed runs of ${runFilterDesc} found!`)
}
diff --git a/.github/workflows/compfuzzci_close_pr.yaml b/.github/workflows/compfuzzci_close_pr.yaml
new file mode 100644
index 00000000000..fec95d7b6b2
--- /dev/null
+++ b/.github/workflows/compfuzzci_close_pr.yaml
@@ -0,0 +1,29 @@
+# This workflow is triggered on PR being closed.
+# It dispatches workflow on CompFuzzCI repository, where the bugs found in the PR head is discarded from the database.
+
+name: Updating CompFuzzCI on PR Closed
+on:
+ pull_request:
+ branches:
+ - master
+ types: [closed]
+
+jobs:
+ UpdatePRClosed:
+ if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang'
+ runs-on: ubuntu-latest
+ steps:
+ - name: Trigger CompFuzzCI
+ uses: actions/github-script@v7
+ with:
+ github-token: ${{ secrets.COMPFUZZCI_PAT }}
+ script: |
+ await github.rest.actions.createWorkflowDispatch({
+ owner: 'CompFuzzCI',
+ repo: 'DafnyCompilerFuzzer',
+ workflow_id: 'update_pr_close.yaml',
+ ref: 'main',
+ inputs: {
+ pr_head_ref: '${{github.event.pull_request.head.ref}}'
+ }
+ })
\ No newline at end of file
diff --git a/.github/workflows/compfuzzci_fuzz.yaml b/.github/workflows/compfuzzci_fuzz.yaml
new file mode 100644
index 00000000000..720f6a02a76
--- /dev/null
+++ b/.github/workflows/compfuzzci_fuzz.yaml
@@ -0,0 +1,37 @@
+# This workflow is triggered on PR being opened, synced, reopened, closed.
+# It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled.
+# For problems or suggestions, contact karnbongkot.boonriong23@imperial.ac.uk
+
+name: Fuzzing on PR
+on:
+ pull_request_target:
+ branches:
+ - master
+
+jobs:
+ FuzzOnPR:
+ if: github.event.pull_request.base.ref == 'master' &&
+ (github.event.pull_request.author_association == 'COLLABORATOR' ||
+ github.event.pull_request.author_association == 'MEMBER' ||
+ github.event.pull_request.author_association == 'OWNER')
+ runs-on: ubuntu-latest
+ steps:
+ - name: Trigger CompFuzzCI
+ uses: actions/github-script@v7
+ with:
+ github-token: ${{ secrets.COMPFUZZCI_PAT }}
+ script: |
+ await github.rest.actions.createWorkflowDispatch({
+ owner: 'CompFuzzCI',
+ repo: 'DafnyCompilerFuzzer',
+ workflow_id: 'fuzz.yaml',
+ ref: 'main',
+ inputs: {
+ pr: '${{github.event.pull_request.number}}',
+ author: '${{github.event.pull_request.user.login}}',
+ branch: '${{github.event.pull_request.head.ref}}',
+ head_sha: '${{github.event.pull_request.head.sha}}',
+ duration: '3600',
+ instance: '2'
+ }
+ })
\ No newline at end of file
diff --git a/.github/workflows/compfuzzci_process_issues.yaml b/.github/workflows/compfuzzci_process_issues.yaml
new file mode 100644
index 00000000000..2228ef0a2d9
--- /dev/null
+++ b/.github/workflows/compfuzzci_process_issues.yaml
@@ -0,0 +1,51 @@
+# This workflow is triggered on issue being opened, closed, reopened.
+# The CompFuzzCI fuzzer needs to keep track of active issues in the repository to ensure that the fuzzer does not report the same issue multiple times.
+# For open and reopen events: It dispatches workflow on CompFuzzCI repository, where the issue is added to the database.
+# For close event: It dispatches workflow on CompFuzzCI repository, where the issue is removed from the database.
+
+name: Issue Update for Fuzzer
+on:
+ issues:
+ branches:
+ - master
+ types: [opened, closed, reopened]
+
+jobs:
+ UpdateIssueOpened:
+ if: github.event.action == 'opened' || github.event.action == 'reopened'
+ runs-on: ubuntu-latest
+ steps:
+ - name: Trigger CompFuzzCI
+ uses: actions/github-script@v7
+ with:
+ github-token: ${{ secrets.COMPFUZZCI_PAT }}
+ script: |
+ await github.rest.actions.createWorkflowDispatch({
+ owner: 'CompFuzzCI',
+ repo: 'DafnyCompilerFuzzer',
+ workflow_id: 'update_issue_open.yaml',
+ ref: 'main',
+ inputs: {
+ issue_number: '${{github.event.issue.number}}',
+ issuer: '${{github.event.issue.user.login}}',
+ commit: '${{ github.sha }}'
+ }
+ })
+ UpdateIssueClosed:
+ if: github.event.action == 'closed'
+ runs-on: ubuntu-latest
+ steps:
+ - name: Trigger CompFuzzCI
+ uses: actions/github-script@v7
+ with:
+ github-token: ${{ secrets.COMPFUZZCI_PAT }}
+ script: |
+ await github.rest.actions.createWorkflowDispatch({
+ owner: 'CompFuzzCI',
+ repo: 'DafnyCompilerFuzzer',
+ workflow_id: 'update_issue_close.yaml',
+ ref: 'main',
+ inputs: {
+ issue_number: '${{github.event.issue.number}}'
+ }
+ })
\ No newline at end of file
diff --git a/.github/workflows/daily-soak-test-build.yml b/.github/workflows/daily-soak-test-build.yml
new file mode 100644
index 00000000000..98f9025f244
--- /dev/null
+++ b/.github/workflows/daily-soak-test-build.yml
@@ -0,0 +1,23 @@
+
+# Scheduled daily build
+#
+# The purpose of this build is to run tests that may have non-deterministic failures
+# many times over, in the hopes of more aggressively revealing
+# flaky tests that occasionally slow down unrelated development.
+
+name: Daily soak test workflow
+
+on:
+ schedule:
+ # Chosen to be hopefully outside of business hours for most contributors'
+ # time zones, and not on the hour to avoid heavy scheduled-job times:
+ # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule
+ - cron: "30 3 * * *"
+ workflow_dispatch:
+
+jobs:
+ daily-soak-build-for-master:
+ if: github.repository_owner == 'dafny-lang' || github.event_name == 'workflow_dispatch'
+ uses: ./.github/workflows/xunit-tests-reusable.yml
+ with:
+ soak_test: true
diff --git a/.github/workflows/deep-tests.yml b/.github/workflows/deep-tests.yml
deleted file mode 100644
index 16228a31723..00000000000
--- a/.github/workflows/deep-tests.yml
+++ /dev/null
@@ -1,58 +0,0 @@
-
-# This workflow includes more expensive tests than what is run on every PR, that are unlikely to break on most changes.
-# It also publishes a nightly release.
-#
-# The if at the beginning of each job terminates the workflow immediately on any repo (like a fork) that is not the main
-# dafny-lang/dafny repo. This stops such forks from running this workflow and failing (for lack of a secret) the attempt to
-# publish a nightly build themselves.
-
-name: Nightly test and release workflow
-
-on:
- schedule:
- # Chosen to be hopefully outside of business hours for most contributors'
- # time zones, and not on the hour to avoid heavy scheduled-job times:
- # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule
- - cron: "30 14 * * *"
- workflow_dispatch:
-
-jobs:
- deep-integration-tests:
- if: github.repository_owner == 'dafny-lang'
- uses: ./.github/workflows/integration-tests-reusable.yml
- with:
- all_platforms: true
- num_shards: 5
-
- determine-vars:
- if: github.repository_owner == 'dafny-lang' && github.ref == 'refs/heads/master'
- runs-on: ubuntu-22.04
- steps:
- - name: Checkout Dafny
- uses: actions/checkout@v3
- with:
- ref: ${{ inputs.sha }}
- submodules: recursive
-
- - name: Get short sha
- run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV
-
- - name: Get current date
- run: echo "date=`date +'%Y-%m-%d'`" >> $GITHUB_ENV
-
- outputs:
- name: nightly-${{ env.date }}-${{ env.sha_short }}
-
- publish-release:
- uses: ./.github/workflows/publish-release-reusable.yml
- needs: [deep-integration-tests, determine-vars]
- with:
- name: ${{ needs.determine-vars.outputs.name }}
- sha: ${{ github.sha }}
- tag_name: nightly
- release_nuget: true
- draft: false
- release_notes: "This is an automatically published nightly release. This release may not be as stable as versioned releases and does not contain release notes."
- prerelease: true
- secrets:
- nuget_api_key: ${{ secrets.NUGET_API_KEY }}
diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml
index 7680173f8ef..99dc121ca7f 100644
--- a/.github/workflows/doc-tests.yml
+++ b/.github/workflows/doc-tests.yml
@@ -10,6 +10,7 @@ on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
+ merge_group:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
@@ -18,27 +19,27 @@ concurrency:
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
doctests:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
runs-on: ubuntu-latest
- steps:
+ steps:
+ # The Windows image was recently updated with a .NET 9 CLI which made CI fail,
+ # We added a global.json to force it to use any .NET CLI with 8 as a major version
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
- dotnet-version: 6.0.x
+ dotnet-version: 8.0.x
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
submodules: recursive
path: dafny
- name: Load Z3
run: |
- sudo apt-get install -qq libarchive-tools
+ sudo apt-get update && sudo apt-get install -qq libarchive-tools
mkdir -p dafny/Binaries/z3/bin
wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
mv z3-* dafny/Binaries/z3/bin/
diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml
index 905c86531e2..79d72f30dcf 100644
--- a/.github/workflows/integration-tests-reusable.yml
+++ b/.github/workflows/integration-tests-reusable.yml
@@ -9,10 +9,17 @@ on:
num_shards:
required: true
type: number
+ ref:
+ required: true
+ type: string
+ compilers:
+ description: 'Compilers to use'
+ type: string
+ required: false
+ default: ""
env:
- dotnet-version: 6.0.x # SDK Version for building Dafny
-
+ dotnet-version: 8.0.x # SDK Version for building Dafny
jobs:
# This job is used to dynamically calculate the matrix dimensions.
@@ -24,7 +31,7 @@ jobs:
- name: Populate OS list (all platforms)
id: populate-os-list-all
if: inputs.all_platforms
- run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT
+ run: echo "os-list=[\"ubuntu-20.04\", \"macos-13\", \"windows-2019\"]" >> $GITHUB_OUTPUT
- name: Populate OS list (one platform)
id: populate-os-list-one
if: "!inputs.all_platforms"
@@ -32,7 +39,7 @@ jobs:
- name: Populate OS mapping for package.py
id: populate-os-mapping
run: |
- echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-latest\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT
+ echo "os-mapping={\"ubuntu-20.04\": \"ubuntu\", \"macos-13\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT
- name: Populate target runtime version list (all platforms)
id: populate-target-runtime-version-all
if: inputs.all_platforms
@@ -50,6 +57,7 @@ jobs:
shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
test:
needs: populate-matrix-dimensions
+ timeout-minutes: 120
runs-on: ${{ matrix.os }}
strategy:
matrix:
@@ -61,9 +69,14 @@ jobs:
if: runner.os == 'Linux'
run: cert-sync /etc/ssl/certs/ca-certificates.crt
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{ env.dotnet-version }}
+ # Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+ - name: Setup dotnet
+ uses: actions/setup-dotnet@v4
+ with:
+ dotnet-version: 6.0.x
- name: C++ for ubuntu 20.04
if: matrix.os == 'ubuntu-20.04'
run: |
@@ -73,31 +86,41 @@ jobs:
run: |
sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
- name: Set up oldest supported JDK
- if: matrix.target-language-version == 'oldest'
- uses: actions/setup-java@v3
+ if: matrix.target-language-version != 'newest'
+ uses: actions/setup-java@v4
with:
java-version: 8
distribution: corretto
- name: Set up newest supported JDK
if: matrix.target-language-version == 'newest'
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
+ - name: Set up oldest supported Go
+ uses: actions/setup-go@v5
+ with:
+ go-version: '1.21'
+ cache: false
+ - name: Set up goimports
+ env:
+ GO111MODULE: on
+ run: go install golang.org/x/tools/cmd/goimports@latest
- name: Set up Python
- uses: actions/setup-python@v4
+ uses: actions/setup-python@v5
with:
python-version: '3.11'
- name: Upgrade outdated pip
run: python -m pip install --upgrade pip
- name: Install lit
run: pip install lit OutputCheck pyyaml
- - uses: actions/setup-node@v3
+ - uses: actions/setup-node@v4
- run: npm install bignumber.js
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
path: dafny
+ ref: ${{ inputs.ref }}
submodules: true # Until the libraries work again
- name: Install Java runtime locally (non-Windows)
if: runner.os != 'Windows'
@@ -110,6 +133,22 @@ jobs:
# - name: Clean up libraries for testing
# run: |
# rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
+ - name: Use the default Rust linker (Non-Windows)
+ if: runner.os != 'Windows'
+ run: rustup default stable
+ - name: Use specific Toolchain (Windows)
+ if: runner.os == 'Windows'
+ run: rustup default stable-x86_64-pc-windows-gnu
+ - name: Rust-related System information
+ run: |
+ echo "What is the Rust version?"
+ rustc -vV
+ echo "What is the cargo version?"
+ cargo --version
+ echo "What is the architecture?"
+ uname -m
+ echo "What are Rust toolchains installed?"
+ rustup toolchain list
- name: Create release
if: inputs.all_platforms
run: |
@@ -124,7 +163,7 @@ jobs:
- name: Load Z3
if: "!inputs.all_platforms"
run: |
- sudo apt-get install -qq libarchive-tools
+ sudo apt-get update && sudo apt-get install -qq libarchive-tools
mkdir -p dafny/Binaries/z3/bin
wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
mv z3-4.12.1 dafny/Binaries/z3/bin/
@@ -137,9 +176,10 @@ jobs:
XUNIT_SHARD: ${{ matrix.shard }}
XUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
DAFNY_RELEASE: ${{ github.workspace }}\unzippedRelease\dafny
+ DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
run: |
cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe
- dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" dafny/Source/IntegrationTests/IntegrationTests.csproj
+ dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests/IntegrationTests.csproj
- name: Generate tests (non-Windows)
## This step creates lit tests from examples in documentation
## These are then picked up by the integration tests below
@@ -153,13 +193,14 @@ jobs:
env:
XUNIT_SHARD: ${{ matrix.shard }}
XUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
+ DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }}
run: |
${{ inputs.all_platforms }} && export DAFNY_RELEASE="${{ github.workspace }}/unzippedRelease/dafny"
- dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" dafny/Source/IntegrationTests
- - uses: actions/upload-artifact@v3
+ dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests
+ - uses: actions/upload-artifact@v4
if: always()
with:
- name: integration-test-results-${{ matrix.os }}
+ name: integration-test-results-${{ matrix.os }}-${{ matrix.shard }}
path: |
dafny/Source/*/TestResults/*.trx
dafny/Source/*/TestResults/*/coverage.cobertura.xml
diff --git a/.github/workflows/jekyll.yml b/.github/workflows/jekyll.yml
new file mode 100644
index 00000000000..0727bfc0c73
--- /dev/null
+++ b/.github/workflows/jekyll.yml
@@ -0,0 +1,60 @@
+# Sample workflow for building and deploying a Jekyll site to GitHub Pages
+name: Deploy Jekyll site to Pages
+
+on:
+ # Runs on pushes targeting the default branch
+ push:
+ branches: ["master"]
+
+ # Allows you to run this workflow manually from the Actions tab
+ workflow_dispatch:
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+ contents: read
+ pages: write
+ id-token: write
+
+# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
+# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
+concurrency:
+ group: "pages"
+ cancel-in-progress: false
+
+jobs:
+ # Build job
+ build:
+ runs-on: ubuntu-latest
+ steps:
+ - name: Checkout
+ uses: actions/checkout@v4
+ - name: Setup Ruby
+ uses: ruby/setup-ruby@v1
+ with:
+ ruby-version: '3.1' # Not needed with a .ruby-version file
+ bundler-cache: true # runs 'bundle install' and caches installed gems automatically
+ cache-version: 0 # Increment this number if you need to re-download cached gems
+ working-directory: 'docs'
+ - name: Setup Pages
+ id: pages
+ uses: actions/configure-pages@v5
+ - name: Build with Jekyll
+ # Outputs to the './_site' directory by default
+ run: (cd docs; bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}" --destination ../_site)
+ env:
+ JEKYLL_ENV: production
+ - name: Upload artifact
+ # Automatically uploads an artifact from the './_site' directory by default
+ uses: actions/upload-pages-artifact@v3
+
+ # Deployment job
+ deploy:
+ environment:
+ name: github-pages
+ url: ${{ steps.deployment.outputs.page_url }}
+ runs-on: ubuntu-latest
+ needs: build
+ steps:
+ - name: Deploy to GitHub Pages
+ id: deployment
+ uses: actions/deploy-pages@v4
diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml
index 61805e91a58..5e779c576a8 100644
--- a/.github/workflows/msbuild.yml
+++ b/.github/workflows/msbuild.yml
@@ -4,6 +4,7 @@ on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
+ merge_group:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
@@ -11,13 +12,11 @@ concurrency:
env:
- dotnet-version: 6.0.x # SDK Version for building Dafny
+ dotnet-version: 8.0.x # SDK Version for building Dafny
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
singletons:
needs: check-deep-tests
@@ -25,17 +24,23 @@ jobs:
runs-on: ubuntu-20.04
steps:
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- name: Restore tools
working-directory: dafny
run: dotnet tool restore
+ - name: Check whitespace and style
+ working-directory: dafny
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+ - name: Check that it's possible to bump the version
+ working-directory: dafny
+ run: make bumpversion-test
- name: Get Boogie Version
run: |
sudo apt-get update
@@ -45,7 +50,7 @@ jobs:
working-directory: dafny
run: git apply customBoogie.patch
- name: Checkout Boogie
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
repository: boogie-org/boogie
path: dafny/boogie
@@ -53,11 +58,8 @@ jobs:
- name: Build Dafny with local Boogie
working-directory: dafny
run: dotnet build Source/Dafny.sln
- - name: Check whitespace and style
- working-directory: dafny
- run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
- name: Create NuGet package (just to make sure it works)
- run: dotnet pack --no-build dafny/Source/Dafny.sln
+ run: dotnet pack dafny/Source/Dafny.sln
- name: Check uniformity of integration tests that exercise backends
run: DAFNY_INTEGRATION_TESTS_MODE=uniformity-check dotnet test dafny/Source/IntegrationTests
@@ -68,14 +70,17 @@ jobs:
integration-tests:
needs: check-deep-tests
- if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
+ if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.pull_request.labels.*.name, 'run-integration-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
uses: ./.github/workflows/integration-tests-reusable.yml
with:
+ ref: ${{ github.ref }}
# By default run only on one platform, but run on all platforms if the PR has the "run-deep-tests"
# label, and skip checking the nightly build above.
# This is the best way to fix an issue in master that was only caught by the nightly build.
all_platforms: ${{ contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')}}
num_shards: 5
+ # Omit Rust in the nightly build (or rather simulating it here) because Rust is known to have random issues
+ compilers: ${{ (contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')) && 'cs,java,go,js,cpp,dfy,py' || '' }}
test-coverage-analysis:
runs-on: ubuntu-20.04
@@ -86,13 +91,13 @@ jobs:
steps:
# Check out Dafny so that highlighted source is possible
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
@@ -109,12 +114,13 @@ jobs:
dotnet tool run coco "Source/DafnyCore/Dafny.atg" -namespace Microsoft.Dafny -frames "Source/DafnyCore/Coco"
- name: Download integration test artifacts
- uses: actions/download-artifact@v3
+ uses: actions/download-artifact@v4
with:
- name: integration-test-results-ubuntu-20.04
+ pattern: integration-test-results-ubuntu-20.04-*
+ merge-multiple: true
- name: Download unit test artifacts
- uses: actions/download-artifact@v3
+ uses: actions/download-artifact@v4
with:
name: unit-test-results-ubuntu-20.04
@@ -127,7 +133,7 @@ jobs:
reportgenerator \
-reports:"./**/coverage.cobertura.xml" \
-reporttypes:Cobertura -targetdir:coverage-cobertura \
- -classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector;-DAST.*;-DCOMP.*"
+ -classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector;-Microsoft.Dafny.Compilers.DafnyCompiler;-DAST.*;-DCOMP.*"
# Generate HTML from combined report, leaving out XUnitExtensions
reportgenerator \
-reports:"coverage-cobertura/Cobertura.xml" \
@@ -158,7 +164,7 @@ jobs:
output: both
# Fail if less than 86% total coverage, measured across all packages combined.
# Report "yellow" status if less than 90% total coverage.
- thresholds: '86 90'
+ thresholds: '85 90'
- name: Code coverage report (LSP)
uses: irongut/CodeCoverageSummary@v1.3.0
@@ -175,7 +181,7 @@ jobs:
# Report "yellow" status if less than 90% total coverage.
thresholds: '86 90'
- - uses: actions/upload-artifact@v3
+ - uses: actions/upload-artifact@v4
if: always() # Upload results even if the job fails
with:
name: test-coverage-results
diff --git a/.github/workflows/nightly-build-manual.yml b/.github/workflows/nightly-build-manual.yml
new file mode 100644
index 00000000000..51b85eafed4
--- /dev/null
+++ b/.github/workflows/nightly-build-manual.yml
@@ -0,0 +1,26 @@
+
+# Manual trigger for the nightly build on a given branch.
+
+name: Nightly test and release workflow (Manual trigger)
+
+on:
+ workflow_dispatch:
+ inputs:
+ ref:
+ description: 'The git ref to run on'
+ required: true
+ type: string
+ publish-prerelease:
+ description: 'Whether to publish a prerelease'
+ required: false
+ type: boolean
+ default: false
+
+jobs:
+ nightly-build:
+ uses: ./.github/workflows/nightly-build-reusable.yml
+ with:
+ ref: ${{ inputs.ref }}
+ publish-prerelease: ${{ inputs.publish-prerelease }}
+ secrets:
+ nuget_api_key: ${{ secrets.NUGET_API_KEY }}
diff --git a/.github/workflows/nightly-build-reusable.yml b/.github/workflows/nightly-build-reusable.yml
new file mode 100644
index 00000000000..4b659ebba7b
--- /dev/null
+++ b/.github/workflows/nightly-build-reusable.yml
@@ -0,0 +1,63 @@
+# This workflow includes more expensive tests than what is run on every PR, that are unlikely to break on most changes.
+# It also optionally publishes a nightly prerelease.
+
+name: Nightly test and release workflow (Reusable Workflow)
+
+on:
+ workflow_call:
+ inputs:
+ ref:
+ required: true
+ type: string
+ publish-prerelease:
+ required: false
+ type: boolean
+ default: false
+ secrets:
+ # Required if publish-prerelease is true
+ nuget_api_key:
+ required: false
+
+jobs:
+ deep-integration-tests:
+ if: github.repository_owner == 'dafny-lang'
+ uses: ./.github/workflows/integration-tests-reusable.yml
+ with:
+ ref: ${{ inputs.ref }}
+ all_platforms: true
+ num_shards: 10
+ # Omit Rust because Rust is known to have random issues
+ compilers: cs,java,go,js,cpp,dfy,py
+
+ determine-vars:
+ if: github.repository_owner == 'dafny-lang' && inputs.publish-prerelease
+ runs-on: ubuntu-22.04
+ steps:
+ - name: Checkout Dafny
+ uses: actions/checkout@v4
+ with:
+ ref: ${{ inputs.ref }}
+ submodules: recursive
+
+ - name: Get short sha
+ run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV
+
+ - name: Get current date
+ run: echo "date=`date +'%Y-%m-%d'`" >> $GITHUB_ENV
+
+ outputs:
+ name: nightly-${{ env.date }}-${{ env.sha_short }}
+
+ publish-release:
+ uses: ./.github/workflows/publish-release-reusable.yml
+ needs: [deep-integration-tests, determine-vars]
+ with:
+ name: ${{ needs.determine-vars.outputs.name }}
+ ref: ${{ inputs.ref }}
+ tag_name: nightly
+ release_nuget: true
+ draft: false
+ release_notes: "This is an automatically published nightly release. This release may not be as stable as versioned releases and does not contain release notes."
+ prerelease: true
+ secrets:
+ nuget_api_key: ${{ secrets.nuget_api_key }}
diff --git a/.github/workflows/nightly-build.yml b/.github/workflows/nightly-build.yml
new file mode 100644
index 00000000000..311a0656713
--- /dev/null
+++ b/.github/workflows/nightly-build.yml
@@ -0,0 +1,33 @@
+
+# Scheduled nightly build
+#
+# Scheduled workflows only ever trigger for the default branch,
+# but we need to run nightly jobs on multiple branches.
+# This workflow therefore triggers a reusable workflow
+# on every branch that needs to be protected with the nightly deep-test mechanism,
+# and ensures which ever branch contains the next planned release
+# publishes the nightly prerelease.
+#
+# The if at the beginning of each job terminates the workflow immediately on any repo (like a fork) that is not the main
+# dafny-lang/dafny repo. This stops such forks from running this workflow and failing (for lack of a secret) the attempt to
+# publish a nightly build themselves.
+
+name: Nightly test and release workflow
+
+on:
+ schedule:
+ # Chosen to be hopefully outside of business hours for most contributors'
+ # time zones, and not on the hour to avoid heavy scheduled-job times:
+ # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule
+ - cron: "30 14 * * *"
+ workflow_dispatch:
+
+jobs:
+ nightly-build-for-master:
+ if: github.repository_owner == 'dafny-lang'
+ uses: ./.github/workflows/nightly-build-reusable.yml
+ with:
+ ref: master
+ publish-prerelease: true
+ secrets:
+ nuget_api_key: ${{ secrets.NUGET_API_KEY }}
diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml
index 8e6333175bb..adee22747dc 100644
--- a/.github/workflows/publish-release-reusable.yml
+++ b/.github/workflows/publish-release-reusable.yml
@@ -9,7 +9,7 @@ on:
prerelease:
required: false
type: boolean
- sha:
+ ref:
required: true
type: string
draft:
@@ -30,20 +30,20 @@ on:
required: false
env:
- dotnet-version: 6.0.x # SDK Version for building Dafny
+ dotnet-version: 8.0.x # SDK Version for building Dafny
jobs:
publish-release:
- runs-on: macos-latest
+ runs-on: macos-13 # Put back 'ubuntu-20.04' if macos-latest fails in any way
steps:
- name: Print version
run: echo ${{ inputs.name }}
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
path: dafny
- ref: ${{ inputs.sha }}
+ ref: ${{ inputs.ref }}
- name: Ensure tag exists
if: ${{ inputs.prerelease }}
run: |
@@ -51,7 +51,7 @@ jobs:
git push origin ${{ inputs.tag_name }} -f
working-directory: dafny
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
- name: C++ for ubuntu 20.04
@@ -63,14 +63,14 @@ jobs:
run: |
sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
- name: Set up JDK 18
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
- - uses: actions/setup-node@v3
+ - uses: actions/setup-node@v4
- run: npm install bignumber.js
- name: Set up Python
- uses: actions/setup-python@v4
+ uses: actions/setup-python@v5
with:
python-version: '3.11'
- name: Build Dafny
@@ -79,14 +79,14 @@ jobs:
rm dafny/Binaries/*.nupkg
- name: Create release NuGet package (for uploading)
if: ${{ !inputs.prerelease }}
- run: dotnet pack --no-build dafny/Source/Dafny.sln
+ run: dotnet pack dafny/Source/Dafny.sln
- name: Create prerelease NuGet package (for uploading)
if: ${{ inputs.prerelease }}
# NuGet will consider any package with a version-suffix as a prerelease
- run: dotnet pack --version-suffix ${{ inputs.name }} --no-build dafny/Source/Dafny.sln
+ run: dotnet pack --version-suffix ${{ inputs.name }} dafny/Source/Dafny.sln
- name: Make NuGet package available as an artifact
- uses: actions/upload-artifact@v3
+ uses: actions/upload-artifact@v4
with:
name: nuget-packages
path: dafny/Binaries/*.nupkg
@@ -96,22 +96,31 @@ jobs:
# Need --skip-duplicate for cases where we release a new Dafny
# version but the runtime hasn't changed and is still the old
# version.
- run: dotnet nuget push --skip-duplicate "dafny/Binaries/Dafny*.nupkg" -k ${{ secrets.nuget_api_key }} -s https://api.nuget.org/v3/index.json
+ run: dotnet nuget push --skip-duplicate "dafny/Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json
- - name: Install latex pandoc
+ - name: Install pandoc - Linux
+ if: runner.os == 'Linux'
+ run: |
+ wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
+ sudo dpkg -i *.deb
+ rm -rf *.deb
+ pandoc -v
+ sudo gem install rouge
+ - name: Install pandoc - MacOS
+ if: runner.os == 'MacOS'
run: |
unset HOMEBREW_NO_INSTALL_FROM_API
brew untap Homebrew/core
brew update-reset && brew update
brew install pandoc
- brew install --cask mactex
- eval "$(/usr/libexec/path_helper)"
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
pandoc -v
- which latex || echo NOT FOUND latex
- which xelatex || echo NOT FOUND xelatex
sudo gem install rouge -v 3.30.0
+ - name: Install Tectonic
+ uses: wtfjoke/setup-tectonic@v3
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ tectonic-version: 0.15
+
- name: Clean Dafny
run: dotnet clean dafny/Source/Dafny.sln
# First we build the ZIPs (which do not include the refman)
@@ -128,14 +137,17 @@ jobs:
# Additionally, since the refman build scripts expect to find Dafny in its usual Binaries/ folder (not in
# a platform-specific directory), we build Dafny once here.
- name: Re-build Dafny
+ if: ${{ !inputs.prerelease }}
run: dotnet build dafny/Source/Dafny.sln
- name: Build reference manual
+ if: ${{ !inputs.prerelease }}
run: |
eval "$(/usr/libexec/path_helper)"
make -C dafny/docs/DafnyRef
- - name: Create GitHub release
- uses: softprops/action-gh-release@v1
+ - name: Create GitHub release (release)
+ if: ${{ !inputs.prerelease }}
+ uses: softprops/action-gh-release@v2
with:
name: Dafny ${{ inputs.name }}
tag_name: ${{ inputs.tag_name }}
@@ -146,3 +158,17 @@ jobs:
dafny/Package/dafny-${{ inputs.name }}*
dafny/docs/DafnyRef/DafnyRef.pdf
fail_on_unmatched_files: true
+
+ # This step is separate from the release one because the refman is omitted
+ - name: Create GitHub release (prerelease)
+ if: ${{ inputs.prerelease }}
+ uses: softprops/action-gh-release@v2
+ with:
+ name: Dafny ${{ inputs.name }}
+ tag_name: ${{ inputs.tag_name }}
+ body: ${{ inputs.release_notes }}
+ draft: ${{ inputs.draft }}
+ prerelease: ${{ inputs.prerelease }}
+ files: |
+ dafny/Package/dafny-${{ inputs.name }}*
+ fail_on_unmatched_files: true
diff --git a/.github/workflows/publish-release.yml b/.github/workflows/publish-release.yml
index fd6476f5188..7b3ee73a7ef 100644
--- a/.github/workflows/publish-release.yml
+++ b/.github/workflows/publish-release.yml
@@ -7,13 +7,16 @@ on:
- 'v*'
env:
- dotnet-version: 6.0.x # SDK Version for building Dafny
+ dotnet-version: 8.0.x # SDK Version for building Dafny
jobs:
- check-deep-tests:
- uses: ./.github/workflows/check-deep-tests-reusable.yml
+ deep-integration-tests:
+ if: github.repository_owner == 'dafny-lang'
+ uses: ./.github/workflows/integration-tests-reusable.yml
with:
- sha: ${{ github.sha }}
+ ref: ${{ github.ref }}
+ all_platforms: true
+ num_shards: 5
get-version:
runs-on: ubuntu-22.04
@@ -26,11 +29,11 @@ jobs:
version: ${{ steps.get-version.outputs.version-without-v }}
publish-release:
- needs: [check-deep-tests, get-version]
+ needs: [deep-integration-tests, get-version]
uses: ./.github/workflows/publish-release-reusable.yml
with:
name: ${{ needs.get-version.outputs.version }}
- sha: ${{ github.sha }}
+ ref: ${{ github.sha }}
tag_name: ${{ github.ref }}
draft: true
release_nuget: true
diff --git a/.github/workflows/refman.yml b/.github/workflows/refman.yml
index 3a9db4edddc..93a65d4470b 100644
--- a/.github/workflows/refman.yml
+++ b/.github/workflows/refman.yml
@@ -4,6 +4,7 @@ on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
+ merge_group:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
@@ -12,76 +13,51 @@ concurrency:
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
- build:
+ build-refman:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
runs-on: ${{ matrix.os }}
strategy:
fail-fast: false
matrix:
- os: [ macos-latest ]
- # os: [macos-latest, ubuntu-latest ]
+ os: [ ubuntu-22.04 ]
steps:
- name: OS
run: echo ${{ runner.os }} ${{ matrix.os }}
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
- dotnet-version: 6.0.x
+ dotnet-version: 8.0.x
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
submodules: recursive
path: dafny
- name: Build Dafny
run: dotnet build dafny/Source/Dafny.sln
- - name: Install latex pandoc - Linux
+ - name: Install pandoc - Linux
if: runner.os == 'Linux'
run: |
- sudo apt-get install texlive texlive-xetex
- wget https://github.com/jgm/pandoc/releases/download/2.10.1/pandoc-2.10.1-1-amd64.deb
+ wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
sudo dpkg -i *.deb
rm -rf *.deb
- # apt-get has pandoc, but it is outdated
- - name: Extra linux packages
- if: matrix.os == 'ubuntu-latest'
- run: |
- sudo apt-get install texlive-science
- sudo tlmgr init-usertree
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
- pandoc -v
- which latex || echo NOT FOUND latex
- which xelatex || echo NOT FOUND xelatex
- sudo gem install rouge
- - if: matrix.os != 'ubuntu-latest' && runner.os == 'Linux'
- run: |
- sudo apt-get install texlive-math-extra
- sudo tlmgr init-usertree
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
pandoc -v
- which latex || echo NOT FOUND latex
- which xelatex || echo NOT FOUND xelatex
sudo gem install rouge
- - name: Install latex pandoc - MacOS
+ - name: Install pandoc - MacOS
if: runner.os == 'MacOS'
run: |
unset HOMEBREW_NO_INSTALL_FROM_API
brew untap Homebrew/core
brew update-reset && brew update
brew install pandoc
- brew install --cask basictex
- eval "$(/usr/libexec/path_helper)"
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
pandoc -v
- which latex || echo NOT FOUND latex
- which xelatex || echo NOT FOUND xelatex
sudo gem install rouge -v 3.30.0
+ - name: Install Tectonic
+ uses: wtfjoke/setup-tectonic@v3
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ tectonic-version: 0.15
- name: Build reference manual
run: |
eval "$(/usr/libexec/path_helper)"
@@ -89,7 +65,7 @@ jobs:
make -C dafny/docs/DafnyRef
- name: Check
run: ls -la dafny/docs/DafnyRef/DafnyRef.pdf
- - uses: actions/upload-artifact@v3
+ - uses: actions/upload-artifact@v4
if: always()
with:
name: DafnyRef
diff --git a/.github/workflows/release-brew.yml b/.github/workflows/release-brew.yml
index 70bdfb5de88..c6867f03326 100644
--- a/.github/workflows/release-brew.yml
+++ b/.github/workflows/release-brew.yml
@@ -10,7 +10,7 @@ concurrency:
jobs:
build:
- runs-on: macos-latest
+ runs-on: macos-13
steps:
- name: Install dafny
@@ -26,7 +26,7 @@ jobs:
java -version
python --version
- name: Set up Python
- uses: actions/setup-python@v4
+ uses: actions/setup-python@v5
with:
python-version: '3.11'
## To be consistent, the download should be tested with the quicktest.sh corresponding to
diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml
index 60c0393ed77..1d08a00ba40 100644
--- a/.github/workflows/release-downloads-nuget.yml
+++ b/.github/workflows/release-downloads-nuget.yml
@@ -17,7 +17,7 @@ on:
workflow_dispatch:
env:
- dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
+ dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
concurrency:
@@ -32,18 +32,18 @@ jobs:
fail-fast: false
matrix:
# This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
- os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ]
+ os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ]
steps:
- name: OS
run: echo ${{ runner.os }} ${{ matrix.os }}
- name: Set up JDK 18
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
- name: Setup dotnet
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
- name: Load Z3
@@ -85,13 +85,13 @@ jobs:
excludes: prerelease, draft
- name: Verify Dafny version
if: "${{ steps.dafny.outputs.release != '' }}"
- run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]{5}"
+ run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]+"
shell: bash
## Check that a simple program compiles and runs on each supported platform
## Now that the dotnet tool distribution doesn't include the Scripts,
## so we need to clone the repository to get them.
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
submodules: recursive
path: dafny-repo
@@ -111,7 +111,7 @@ jobs:
# but note we need to skip Dafny since nuget install doesn't work for dotnet tools.
library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ]
# This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
- os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+ os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ]
steps:
# Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer)
diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml
index 8cac8cd3ac8..74c68178672 100644
--- a/.github/workflows/release-downloads.yml
+++ b/.github/workflows/release-downloads.yml
@@ -18,14 +18,14 @@ jobs:
fail-fast: false
matrix:
# This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
- os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+ os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ]
include:
- os: 'ubuntu-latest'
osn: 'ubuntu-20.04'
- os: 'ubuntu-20.04'
osn: 'ubuntu-20.04'
- - os: 'macos-latest'
- osn: 'x64-macos-11'
+ - os: 'macos-13'
+ osn: 'x64-macos-13'
- os: 'windows-2019'
osn: 'windows-2019'
# There is no hosted environment for Ubuntu 14.04 or for debian
@@ -36,7 +36,7 @@ jobs:
- name: OS
run: echo ${{ runner.os }} ${{ matrix.os }}
- name: Set up JDK 18
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml
index ad927af4867..0d5888a133d 100644
--- a/.github/workflows/runtime-tests.yml
+++ b/.github/workflows/runtime-tests.yml
@@ -4,7 +4,8 @@ on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
-
+ merge_group:
+
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
@@ -12,8 +13,6 @@ concurrency:
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
- with:
- branch: master
build:
needs: check-deep-tests
@@ -23,14 +22,29 @@ jobs:
steps:
- name: Checkout Dafny
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
with:
submodules: true
+ # The Windows image was recently updated with a .NET 9 CLI which made CI fail,
+ # We added a global.json to force it to use any .NET CLI with 8 as a major version
+ - name: Setup dotnet
+ uses: actions/setup-dotnet@v4
+ with:
+ dotnet-version: 8.0.x
- name: Set up JDK 18
- uses: actions/setup-java@v3
+ uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
+ - name: Set up Go
+ uses: actions/setup-go@v5
+ with:
+ go-version: '1.21'
+ cache: false
+ - name: Set up goimports
+ env:
+ GO111MODULE: on
+ run: go install golang.org/x/tools/cmd/goimports@latest
- name: Build Dafny
run: dotnet build Source/Dafny.sln
- name: Get Z3
@@ -40,18 +54,36 @@ jobs:
cd ./Source/DafnyCore
make test
make check-format
+ make check-extract
+ - name: Test DafnyRuntime (C#, Rust)
+ run: |
+ cd ./Source/DafnyRuntime
+ make all
- name: Test DafnyRuntimeDafny
run: |
cd ./Source/DafnyRuntime/DafnyRuntimeDafny
- make test
- make check-format
+ make all
- name: Test DafnyRuntimeGo
run: |
cd ./Source/DafnyRuntime/DafnyRuntimeGo
- make test
- # This isn't strictly necessary since the Java runtime has to be built into a jar,
- # which also runs the tests.
- # But I prefer the simplicity of testing every testable runtime in this workflow
+ make all
+ - name: Test DafnyRuntimeGo-gomod
+ run: |
+ cd ./Source/DafnyRuntime/DafnyRuntimeGo-gomod
+ make all
- name: Test DafnyRuntimeJava
- run: ./Source/DafnyRuntime/DafnyRuntimeJava/gradlew -p ./Source/DafnyRuntime/DafnyRuntimeJava test
-
+ run: |
+ cd ./Source/DafnyRuntime/DafnyRuntimeJava
+ make all
+ - name: Test DafnyRuntimePython
+ run: |
+ cd ./Source/DafnyRuntime/DafnyRuntimePython
+ make all
+ - name: Test DafnyRuntimeJs
+ run: |
+ cd ./Source/DafnyRuntime/DafnyRuntimeJs
+ make all
+ - name: Test DafnyRuntimeRust
+ run: |
+ cd ./Source/DafnyRuntime/DafnyRuntimeRust
+ make all
diff --git a/.github/workflows/standard-libraries.yml b/.github/workflows/standard-libraries.yml
new file mode 100644
index 00000000000..dd966bbc82f
--- /dev/null
+++ b/.github/workflows/standard-libraries.yml
@@ -0,0 +1,48 @@
+name: Build and Test Dafny Standard Libraries
+
+on:
+ workflow_dispatch:
+ pull_request:
+ branches: [ master, main-* ]
+ merge_group:
+
+concurrency:
+ group: ${{ github.workflow }}-${{ github.ref }}
+ cancel-in-progress: true
+
+jobs:
+ check-deep-tests:
+ uses: ./.github/workflows/check-deep-tests-reusable.yml
+
+ build:
+ needs: check-deep-tests
+ if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
+ runs-on: macos-13
+
+ steps:
+ - name: Checkout Dafny
+ uses: actions/checkout@v4
+ with:
+ submodules: true
+ - name: Set up JDK 18
+ uses: actions/setup-java@v4
+ with:
+ java-version: 18
+ distribution: corretto
+ - name: Set up Go
+ uses: actions/setup-go@v5
+ with:
+ go-version: '1.21'
+ cache: false
+ - name: Set up goimports
+ env:
+ GO111MODULE: on
+ run: go install golang.org/x/tools/cmd/goimports@latest
+ - name: Build Dafny
+ run: dotnet build Source/Dafny.sln
+ - name: Get Z3
+ run: make z3-mac
+ - run: npm install bignumber.js
+ - name: Test DafnyStandardLibraries
+ run: make -C Source/DafnyStandardLibraries all
+
diff --git a/.github/workflows/test-report.yml b/.github/workflows/test-report.yml
index 29508c1a211..167889f4b90 100644
--- a/.github/workflows/test-report.yml
+++ b/.github/workflows/test-report.yml
@@ -14,7 +14,7 @@ jobs:
if: always()
steps:
- - uses: actions/checkout@v3
+ - uses: actions/checkout@v4
with:
submodules: recursive
diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml
index dff2b0da5a7..d6b768e6f3a 100644
--- a/.github/workflows/xunit-tests-reusable.yml
+++ b/.github/workflows/xunit-tests-reusable.yml
@@ -2,7 +2,17 @@ name: Run XUnit tests
on:
workflow_dispatch:
+ inputs:
+ soak_test:
+ required: false
+ type: boolean
+ default: false
workflow_call:
+ inputs:
+ soak_test:
+ required: false
+ type: boolean
+ default: false
## In the matrix:
## os - name of the Github actions runner
@@ -15,15 +25,34 @@ defaults:
working-directory: dafny
jobs:
+ populate-matrix-dimensions:
+ runs-on: ubuntu-latest
+ steps:
+ - name: Populate iterations (normal mode)
+ id: populate-iterations-normal
+ if: "!inputs.soak_test"
+ working-directory: .
+ run: echo "iterations=[1]" >> $GITHUB_OUTPUT
+ - name: Populate iterations (soak test mode)
+ id: populate-iterations-soak
+ if: inputs.soak_test
+ working-directory: .
+ run: echo "iterations=[`seq -s , 1 5`]" >> $GITHUB_OUTPUT
+ outputs:
+ iterations: ${{ steps.populate-iterations-normal.outputs.iterations }} ${{ steps.populate-iterations-soak.outputs.iterations }}
+
build:
+ needs: populate-matrix-dimensions
runs-on: ${{matrix.os}}
timeout-minutes: 60
- name: ${{matrix.suffix}}
+ name: ${{matrix.suffix}} (${{matrix.iteration}})
strategy:
fail-fast: false
matrix:
+ os: [ubuntu-20.04, windows-2019, macos-13]
+ iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }}
include:
- - os: macos-11
+ - os: macos-13
suffix: osx
chmod: true
- os: windows-2019
@@ -34,17 +63,17 @@ jobs:
chmod: true
env:
solutionPath: Source/Dafny.sln
- z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
+ z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10
Logging__LogLevel__Microsoft: Debug
steps:
- - uses: actions/checkout@v3
+ - uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- name: Setup .NET
- uses: actions/setup-dotnet@v3
+ uses: actions/setup-dotnet@v4
with:
- dotnet-version: 6.0.x
+ dotnet-version: 8.0.x
- name: Install dependencies
run: |
dotnet restore ${{env.solutionPath}}
@@ -66,27 +95,34 @@ jobs:
- name: Build
run: dotnet build --no-restore ${{env.solutionPath}}
- name: Run DafnyCore Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyCore.Test
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test
+ - name: Run DafnyLanguageServer Tests (soak test - iteration ${{matrix.iteration}})
+ if: inputs.soak_test
+ run: |
+ dotnet test --no-restore --blame-crash --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
- name: Run DafnyLanguageServer Tests
+ if: "!inputs.soak_test"
run: |
- ## Run twice to catch unstable code (Issue #2673)
- dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyLanguageServer.Test
- ## On the second run, collect test coverage data
## Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package
dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test
-
- name: Run DafnyDriver Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyDriver.Test
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test
- name: Run DafnyPipeline Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyPipeline.Test
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyPipeline.Test/coverlet.runsettings Source/DafnyPipeline.Test
- name: Run DafnyTestGeneration Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyTestGeneration.Test
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --blame-hang-timeout 5m --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test
- name: Run AutoExtern Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/AutoExtern.Test
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/AutoExtern.Test/coverlet.runsettings Source/AutoExtern.Test
- name: Run DafnyRuntime Tests
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyRuntime.Tests
- - uses: actions/upload-artifact@v3
- if: always()
+ if: "!inputs.soak_test"
+ run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyRuntime.Tests/coverlet.runsettings Source/DafnyRuntime.Tests
+ - uses: actions/upload-artifact@v4
+ if: always() && !inputs.soak_test
with:
name: unit-test-results-${{ matrix.os }}
path: |
diff --git a/.gitignore b/.gitignore
index 1a7a01535f0..bb6f6c501c0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -39,7 +39,6 @@ Source/DafnyCore/Scanner.cs.old
Source/DafnyRuntime/MSBuild_Logs/
TestResults/
-Test/.lit_test_times.txt
Docs/OnlineTutorial/DocumentationTransducer.exe
Docs/OnlineTutorial/DocumentationTransducer.pdb
@@ -58,6 +57,9 @@ Source/.vs
# Generated by VS Code
.vscode/*
+# Generated by Dafny tooling
+/Source/DafnyStandardLibraries/build
+
# Generated by Java tools (gradle/javac/etc)
/Source/DafnyRuntime/DafnyRuntimeJava/.gradle
@@ -70,3 +72,22 @@ package-lock.json
docs/dev/*.fix
docs/dev/*.feat
docs/dev/*.break
+
+Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/wrappers3.doo
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Build1
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions-lib
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/log.smt2
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
+Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1
+/Source/DafnyCore/Prelude/DafnyPrelude.bpl
+/Source/DafnyCore/Prelude/Sequences.bpl
+/venv
diff --git a/.gitmodules b/.gitmodules
index 90ba01b0d54..e69de29bb2d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +0,0 @@
-[submodule "Test/libraries"]
- path = Test/libraries
- url = https://github.com/dafny-lang/libraries.git
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index 7dff2b96253..f4cdfba04b2 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -4,5 +4,6 @@ repos:
- id: dotnet-format
name: dotnet-format
language: system
- entry: dotnet tool run dotnet-format --folder -w --include
+ entry: dotnet format whitespace Source/Dafny.sln -v:d --include
+ exclude: 'Source/DafnyCore/Scanner.cs|Source/DafnyCore/Parser.cs|.git/modules/Source/boogie|Source/DafnyCore/GeneratedFromDafny|Source/DafnyCore.Test/GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
types_or: ["c#"]
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e8ab3a05586..ddaf0541814 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -30,17 +30,17 @@ If you want to propose code changes for the Dafny project, please note:
- To propose code changes, use the standard Github multi-user project process, which is described for Dafny on the [wiki](https://github.com/dafny-lang/dafny/wiki/Setting-up-a-development-copy-of-Dafny).
If your change is user-visible, then part of the PR should be corresponding changes to the
-[`RELEASE_NOTES.md`](../RELEASE_NOTES.md) file and to the
+[`RELEASE_NOTES.md`](./RELEASE_NOTES.md) file (by following [this](./docs/dev/README.md)) and to the
[Dafny Reference Manual](./docs/DafnyRef).
Any PR should have tests that check whether the bug-fix fixes the problem addressed or that the new functionality
is properly working.
- - Dafny's integration tests are in [`Test`](../Test). PRs that fix issues reported on GitHub should include a test in [`Test/git-issues/`](../Test/git-issues/).
+ - Dafny's integration tests are in [this directory](Source/IntegrationTests/TestFiles/LitTests/LitTest). PRs that fix issues reported on GitHub should include a test under [`git-issues/`](Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/).
- Each `.dfy` file in `Test/` is a test, with a [`lit`](https://llvm.org/docs/CommandGuide/lit.html) header describing how to run it and a `.expect` file indicating the expected output. See [`Test/README.md`](../Test/README.md) for more info on running Dafny' integration tests.
+ Each `.dfy` file in this directory is a test, with a [`lit`](https://llvm.org/docs/CommandGuide/lit.html) header describing how to run it and a `.expect` file indicating the expected output. See [this README.md file](Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md) for more info on running Dafny' integration tests.
- - Dafny's unit tests are in various `*.Test` directories in [`Source`](../Source).
+ - Dafny's unit tests are in various `*.Test` directories in [`Source`](./Source).
Our CI is configured to run all tests when you create a PR. To run tests locally, use `dotnet test Source/Dafny.sln` (but note that running the tests for our compiler backends requires installing lots of additional software).
@@ -74,7 +74,7 @@ After doing these steps once, for other PRs, one only needs to re-run deep check
- If some required tests fail, investigate and push more commits, but know that each CI run takes a lot of time, so try to fix the problem with as few commits as possible (ideally 1)
It is also possible you find some tests that fail randomly, in that case, re-run them and report to the team. Avoid using the re-run all failed jobs here, because it will re-run _all_ jobs, so select them individually instead.
- Have someone approve the PR and merge it (or auto-merge).
-- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml
+- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml
- Select "Run workflow..."
- Select master
- Wait for this new run to succeed.
@@ -85,7 +85,7 @@ Subsequent CI runs should pick up the successful `deep-tests` run and make the `
### How can I write portions of Dafny in Dafny itself?
Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files.
-The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs`
+The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net8.0/GeneratedFromDafny.cs`
that is automatically included in the build process. This file contains also the Dafny run-time in C#.
One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point.
@@ -101,3 +101,9 @@ For example, `Formatting.dfy`
### What is the release process?
You can find a description of the release process in [docs/dev/RELEASE.md](https://github.com/dafny-lang/dafny/blob/master/docs/dev/RELEASE.md).
+
+### Backwards compatibility
+
+Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version.
+
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
diff --git a/Makefile b/Makefile
index fbd17ba228c..5d526d9ffd5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,71 +1,132 @@
-DIR=$(dir $(realpath $(firstword $(MAKEFILE_LIST))))
+# Run these tasks even if eponymous files or folders exist
+.PHONY: test-dafny exe
+
+DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
default: exe
all: exe refman
exe:
- (cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
+ (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
+
+format-dfy:
+ (cd "${DIR}"/Source/DafnyCore ; make format)
+ (cd "${DIR}"/Source/DafnyStandardLibraries ; make format)
+
+dfy-to-cs:
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
+
+dfy-to-cs-exe: dfy-to-cs
+ (cd "${DIR}" ; dotnet build Source/Dafny.sln )
+
+dfy-to-cs-noverify:
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)
+
+dfy-to-cs-noverify-exe: dfy-to-cs-noverify exe
boogie: ${DIR}/boogie/Binaries/Boogie.exe
tests:
- (cd ${DIR}; dotnet test Source/IntegrationTests)
+ (cd "${DIR}"; dotnet test Source/IntegrationTests)
+
+# make test name=
+# make test name= update=true to update the test
+# make test name= build=false don't build the solution
+test:
+ @DIR="$(DIR)" name="$(name)" update="$(update)" build="$(build)" bash scripts/test.sh
+
+# Run Dafny on an integration test case directly in the folder itself.
+# make test-dafny name= action="run ..." [build=false]
+test-dafny:
+ @name="$(name)" DIR="$(DIR)" action="$(action)" NO_BUILD=$$( [ "${build}" = "false" ] && echo "true" || echo "false" ) bash scripts/test-dafny.sh
tests-verbose:
- (cd ${DIR}; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
+ (cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
${DIR}/boogie/Binaries/Boogie.exe:
- (cd ${DIR}/boogie ; dotnet build -c Release Source/Boogie.sln )
+ (cd "${DIR}"/boogie ; dotnet build -c Release Source/Boogie.sln )
refman: exe
- make -C ${DIR}/docs/DafnyRef
+ make -C "${DIR}"/docs/DafnyRef
refman-release: exe
- make -C ${DIR}/docs/DafnyRef release
+ make -C "${DIR}"/docs/DafnyRef release
z3-mac:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p "${DIR}"/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
unzip z3-4.12.1-x64-macos-11-bin.zip
rm z3-4.12.1-x64-macos-11-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
unzip z3-4.8.5-x64-macos-11-bin.zip
rm z3-4.8.5-x64-macos-11-bin.zip
- mv z3-* ${DIR}/Binaries/z3/bin/
- chmod +x ${DIR}/Binaries/z3/bin/z3-*
+ mv z3-* "${DIR}"/Binaries/z3/bin/
+ chmod +x "${DIR}"/Binaries/z3/bin/z3-*
z3-mac-arm:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p "${DIR}"/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
unzip z3-4.12.1-arm64-macos-11-bin.zip
rm z3-4.12.1-arm64-macos-11-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
unzip z3-4.8.5-x64-macos-11-bin.zip
rm z3-4.8.5-x64-macos-11-bin.zip
- mv z3-* ${DIR}/Binaries/z3/bin/
- chmod +x ${DIR}/Binaries/z3/bin/z3-*
+ mv z3-* "${DIR}"/Binaries/z3/bin/
+ chmod +x "${DIR}"/Binaries/z3/bin/z3-*
z3-ubuntu:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p "${DIR}"/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip
unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip
rm z3-4.8.5-x64-ubuntu-20.04-bin.zip
- mv z3-* ${DIR}/Binaries/z3/bin/
- chmod +x ${DIR}/Binaries/z3/bin/z3-*
+ mv z3-* "${DIR}"/Binaries/z3/bin/
+ chmod +x "${DIR}"/Binaries/z3/bin/z3-*
format:
- dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
+ dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
clean:
- (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
- (cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
- make -C ${DIR}/Source/DafnyCore -f Makefile clean
- (cd ${DIR}/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
- (cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
- make -C ${DIR}/docs/DafnyRef clean
- (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
+ (cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
+ (cd "${DIR}" ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
+ make -C "${DIR}"/Source/DafnyCore -f Makefile clean
+ (cd "${DIR}"/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
+ (cd "${DIR}"/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
+ make -C "${DIR}"/docs/DafnyRef clean
+ (cd "${DIR}"; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
echo Source/*/bin Source/*/obj
+
+bumpversion-test:
+ node ./Scripts/bump_version_number.js --test 1.2.3
+
+update-cs-module:
+ (cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module)
+
+update-rs-module:
+ (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeRust; make update-system-module)
+
+update-go-module:
+ (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
+
+update-runtime-dafny:
+ (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
+
+pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module
+
+update-standard-libraries:
+ (cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)
+
+# `make pr` will bring you in a state suitable for submitting a PR
+# - Builds the Dafny executable
+# - Use the build to convert core .dfy files to .cs
+# - Rebuilds the Dafny executable with this .cs files
+# - Apply dafny format on all dfy files
+# - Apply dotnet format on all cs files except the generated ones
+# - Rebuild the Go and C# runtime modules as needed.
+pr: exe dfy-to-cs-exe pr-nogeneration
+
+# Same as `make pr` but useful when resolving conflicts, to take the last compiled version of Dafny first
+pr-conflict: dfy-to-cs-exe dfy-to-cs-exe pr-nogeneration
diff --git a/README.md b/README.md
index 85b5d451cc3..065b4134367 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,5 @@
+# Dafny
+
[](https://github.com/dafny-lang/dafny/actions?query=workflow%3A%22Build+and+Test%22) [](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
Dafny is a **verification-ready programming language**. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can **compile your code to C#, Go, Python, Java, or JavaScript** (more to come!), so it can integrate with your existing workflow.
@@ -19,29 +21,29 @@ This github site contains these materials:
* the [issue tracker](https://github.com/dafny-lang/dafny/issues)
* the wiki, including [frequently asked questions](https://github.com/dafny-lang/dafny/wiki/FAQ)
-Documentation about the dafny language and tools is located
+Documentation about the Dafny language and tools is located
[here](https://dafny-lang.github.io/dafny).
A reference manual is available both [online](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef) and as [pdf](https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/out/DafnyRef.pdf). (A LaTeX version can be produced if needed.)
-# Community
+## Community
-You can ask questions about Dafny on [Stack Overflow](https://stackoverflow.com/questions/tagged/dafny) or participate in general discussion on Dafny's [](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge).
+Feel free to report issues here on GitHub or to ask for questions on our :speech_balloon: [Zulip](https://dafny.zulipchat.com/) channel.
-# Try Dafny
+## Try Dafny
The easiest way to try out Dafny is to [install Dafny on your own machine in Visual Studio Code](https://github.com/dafny-lang/dafny/wiki/INSTALL#visual-studio-code)
and follow along with the [Dafny tutorial](https://dafny-lang.github.io/dafny/OnlineTutorial/guide).
You can also [download and install](https://github.com/dafny-lang/dafny/wiki/INSTALL#install-the-binaries) the Dafny CLI if you prefer to work from the command line.
-# Read more
+## Read more
Here are some ways to get started with Dafny:
* 4-part course on the _Basics of specification and verification of code_:
- - Lecture 0: [Pre- and postconditions](https://youtu.be/oLS_y842fMc) (19:08)
- - Lecture 1: [Invariants](https://youtu.be/J0FGb6PyO_k) (20:56)
- - Lecture 2: [Binary search](https://youtu.be/-_tx3lk7yn4) (21:14)
- - Lecture 3: [Dutch National Flag algorithm](https://youtu.be/dQC5m-GZYbk) (20:33)
+ * Lecture 0: [Pre- and postconditions](https://youtu.be/oLS_y842fMc) (19:08)
+ * Lecture 1: [Invariants](https://youtu.be/J0FGb6PyO_k) (20:56)
+ * Lecture 2: [Binary search](https://youtu.be/-_tx3lk7yn4) (21:14)
+ * Lecture 3: [Dutch National Flag algorithm](https://youtu.be/dQC5m-GZYbk) (20:33)
* New overview article: [Accessible Software Verification with Dafny](https://www.computer.org/csdl/mags/so/2017/06/mso2017060094-abs.html), IEEE Software, Nov/Dec 2017
* [Online tutorial](https://dafny-lang.github.io/dafny/OnlineTutorial/guide), focusing mostly on simple imperative programs
* [3-page tutorial notes](http://leino.science/papers/krml233.pdf) with examples (ICSE 2013)
@@ -49,7 +51,7 @@ Here are some ways to get started with Dafny:
* Language reference for the [Dafny type system](http://leino.science/papers/krml243.html), which also describes available expressions for each type
* [Cheatsheet](https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZhnb_6dzv-K3u79bMMis/edit?pref=2&pli=1): basic Dafny syntax on two pages
* Dafny Reference Manual [[html](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef)] [[pdf](https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/out/DafnyRef.pdf)]
-* [Dafny libraries](https://github.com/dafny-lang/libraries), a standard library of useful Dafny functions and lemmas
+* [Dafny libraries](Source/DafnyStandardLibraries/README.md), a standard library of useful Dafny functions and lemmas
* [Dafny Power User](http://leino.science/dafny-power-user)
* Videos at [Verification Corner](https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A)
* [Blog](https://dafny.org/blog)
@@ -63,18 +65,18 @@ The language itself draws pieces of influence from:
* ML (like the module system, and its functions and inductive datatypes), and
* Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).
-# External contributions
+## External contributions
* [Haskell-to-Dafny translator](http://www.doc.ic.ac.uk/~dcw/h2d.cgi), by Duncan White
* [Vim-loves-Dafny mode](https://github.com/mlr-msft/vim-loves-dafny) for vim, by Michael Lowell Roberts
* [Boogie-Friends Emacs mode](https://github.com/boogie-org/boogie-friends)
-# Contributors
+## Contributors
Information and instructions for potential contributors are provided [here](CONTRIBUTING.md).
-# License
+## License
Dafny itself is licensed under the MIT license. (See `LICENSE.txt` in the root
directory for details.) The subdirectory `Source/Dafny/Coco` contains third
-party material; see `Source/Dafny/Coco/LICENSE.txt` for more details.
+party material; see `Source/DafnyCore/Coco/LICENSE.txt` for more details.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index bdc52048954..120b43fdc64 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,642 @@
See [docs/dev/news/](docs/dev/news/).
+# 4.9.1
+
+## New features
+
+- Introduce the attributes {:isolate} and {:isolate "paths} that simplify the verification of an assertion by introducing additional verification jobs. {:isolate} can be applied to `assert`, `return` and `continue` statements. When using `{:isolate_assertions}` or `--isolate-assertions`, each return statement now creates a separate verification job for each ensures clause. Previously all ensures clauses where verified in a single job, for all return statements. (https://github.com/dafny-lang/dafny/pull/5832)
+
+- Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through. For backward compatibility, use an explicit `{:induction ...}` where `...` is the list of variables to use for the induction-hypothesis quantifier. Additionally, use a `{:nowarn}` attribute to suppress any warning about lack of matching patterns.
+
+ Improve the selection of induction variables.
+
+ Allow codatatype equality in matching patterns and as a focal predicate for extreme predicates.
+
+ More specifically:
+
+ * If a lemma bears `{:induction x, y, z}`, where `x, y, z` is a subset of the lemma's parameters (in the same order
+ that the lemma gives them), then an induction hypothesis (IH) is generated. The IH quantifies over the
+ given variables.
+
+ For an instance-member lemma, the variables may include the implicit `this` parameter.
+
+ For an extreme lemma, the IH generated is the for corresponding prefix lemma, and the given variables may
+ include the implicit parameter `_k`.
+
+ If good matching patterns are found for the quantifier, then these are indicated in tooltips.
+ If no patterns are found, then a warning is generated; except, if the lemma bears `{:nowarn}`, then only
+ an informational message is given.
+
+ * If a lemma bears `{:induction}` or `{:induction true}`, then a list of induction variables is determined heuristically.
+
+ If the list is empty, then a warning message is generated and no IH is generated. If the list is nonempty,
+ an IH is generated and the list of variables is indicated in a tooltip.
+
+ If good matching patterns are found for the quantifier, then these are indicated in tooltips.
+ If no patterns are found, then a warning is generated; except, if the lemma bears {:nowarn}, then only
+ an informational message is given.
+
+ * If a lemma bears `{:induction false}`, then no IH is generated.
+
+ * If a lemma bears an `:induction` attribute other than those listed above, then an error is generated.
+
+ * If a lemma bears no `:induction` attribute, and the `--manual-lemma-induction` flag is present, then no IH is generated.
+
+ * Otherwise, a list of induction variables is determined heuristically.
+
+ If this list is empty, then no IH is generated and no warning/info is given.
+
+ If the list is nonempty, then the machinery looks for matching patterns for the IH quantifier. If none are
+ found, then no IH is generated. An informational message is generated, saying which candidate variables were
+ used and saying that no matching patterns were found.
+
+ If patterns are found, then an IH is generated, the list of variables and the patterns are indicated in tooltips,
+ and the patterns are used with the IH quantifier.
+
+ The pattern search can be overriden by providing patterns explicitly using the `{:inductionTrigger}` attribute.
+ This attribute has the same syntax as the `{:trigger}` attribute. Using an empty list of triggers restores
+ Dafny's legacy behavior (no triggers for lemma induction hypotheses).
+ (https://github.com/dafny-lang/dafny/pull/5835)
+
+- Accept `decreases to` and `nonincreases to` expressions with 0 LHSs and/or 0 RHSs, and allow parentheses to be omitted when there is 1 LHS and 1 RHS. (https://github.com/dafny-lang/dafny/pull/5891)
+
+- Allow forall statements in statement expressions (https://github.com/dafny-lang/dafny/pull/5894)
+
+- When using `--isolate-assertions` or `{:isolate_assertions}`, a separate assertion batch will be generated per pair of return statement and ensures clause. (https://github.com/dafny-lang/dafny/pull/5917)
+
+## Bug fixes
+
+- `{:only}` on members only affects verification on the current file. (https://github.com/dafny-lang/dafny/pull/5730)
+
+- Fixed a bug that caused "hide *" and "reveal *" not to work when used in statement expressions,
+ after a variable assignment occurred in the same expression.
+ (https://github.com/dafny-lang/dafny/pull/5781)
+
+- Fix malformed Boogie in function override checks (https://github.com/dafny-lang/dafny/pull/5875)
+
+- Fix soundness issue where the verifier had assumed properties of `this` already during the first phase of a constructor (https://github.com/dafny-lang/dafny/pull/5876)
+
+- Don't assume type information before binding variables (for let expressions and named function results) (https://github.com/dafny-lang/dafny/pull/5877)
+
+- Enable using reveal statement expression inside witness expressions (https://github.com/dafny-lang/dafny/pull/5882)
+
+- Fix formatting of var by statements (https://github.com/dafny-lang/dafny/pull/5927)
+
+- Fix bugs that occur when using `{:extern}` to export members (https://github.com/dafny-lang/dafny/pull/5939)
+
+- Fixed a bug that would cause the symbol verification tasks to be done multiple times when using module refinement (https://github.com/dafny-lang/dafny/pull/5967)
+
+- Map range requires equality for enclosing type to support equality (https://github.com/dafny-lang/dafny/pull/5972)
+
+- Improved code navigation for datatype update expressions (https://github.com/dafny-lang/dafny/pull/5986)
+
+# 4.9.0
+
+## New features
+
+- Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (https://github.com/dafny-lang/dafny/pull/5761)
+
+- By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. (https://github.com/dafny-lang/dafny/pull/5779)
+
+- Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. (https://github.com/dafny-lang/dafny/pull/5812)
+
+- Support for [top-level @-attributes](https://dafny.org/latest/DafnyRef/DafnyRef#sec-at-attributes) (https://github.com/dafny-lang/dafny/pull/5825)
+
+## Bug fixes
+
+- Enable abstract imports to work well with match expression that occur in specifications (https://github.com/dafny-lang/dafny/pull/5808)
+
+- Fix a bug that prevented using reveal statement expressions in the body of a constant. (https://github.com/dafny-lang/dafny/pull/5823)
+
+- Improve performance of `dafny verify` for large applications, by removing memory leaks (https://github.com/dafny-lang/dafny/pull/5827)
+
+- Green gutter icons cover constants without RHS (https://github.com/dafny-lang/dafny/pull/5841)
+
+# 4.8.1
+
+## New features
+
+- feat: allow type parameters of `newtype` declarations
+ feat: support optional `witness` clause of constraint-less `newtype` declarations
+ feat: show tool tips for auto-completed type parameters
+ feat: show tool tips for inferred `(==)` characteristics
+ fix: Don't let `newtype` well-formedness checking affect witness checking (fixes ##5520)
+ fix: Check the emptiness status of constraint-less `newtype` declarations (fixes #5521)
+ (https://github.com/dafny-lang/dafny/pull/5495)
+
+- New feature: model extractor
+
+ ### CLI option
+
+ The `dafny verify` command now has an option `--extract:`, where (just like for the various print options) `` is allowed to be `-` to denote standard output.
+
+ ### Extract mechanism
+
+ Upon successful verification, the new extract mechanism visits the AST of the given program. For any module marked with `{:extract}`, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class `_default` has no bearing on the output order).
+
+ Three kinds of declarations are extract-worthy:
+
+ * A type declaration `A` that bears an attribute `{:extract_name B}` is extracted into a Boogie type declaration `type B _ _ _;`.
+
+ The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.)
+
+ * A function declaration `F(x: X, y: Y): Z` that bears an attribute `{:extract_name G}` is extracted into a Boogie function declaration `function G(x: X, y: Y): Z;`.
+
+ The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.)
+
+ * A lemma declaration `L(x: X, y: Y) requires P ensures Q` that bears an attribute `{:extract_pattern ...}` or an attribute `{:extract_used_by ...}` is extracted into a Boogie `axiom`. The axiom has the basic form `axiom (forall x: X, y: Y :: P ==> Q);`.
+
+ If the lemma has an attribute `{:extract_used_by F}`, then the axiom will be emitted into the `uses` clause of the Boogie function generated for Dafny function `F`.
+
+ If the lemma has no in-parameters, the axiom is just `P ==> Q`.
+
+ If the lemma has in-parameters, then any attribute `{:extract_pattern E, F, G}` adds a matching pattern `{ E, F, G }` to the emitted quantifier. Also, any attribute `{:extract_attribute "name", E, F, G}` adds an attribute `{:name E, F, G}` to the quantifier.
+
+ ### Expressions
+
+ The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types.
+
+ At this time, only a limited set of expressions and types are supported, but more can be added in the future.
+
+ Any `forall` and `exists` quantifiers in expressions are allowed to use `:extract_pattern` and `:extract_attribute` attributes, as described above for lemmas.
+
+ Some extracted expressions are simplified. For example, `true && !!P` is simplified to `P`.
+
+ ### Soundness
+
+ The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in `DafnyPrelude.bpl` to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency.
+ (https://github.com/dafny-lang/dafny/pull/5621)
+
+- Dafny-to-Rust: `{:test}` methods generate `#[test]` wrappers in Rust that can be invoked using `cargo test`.
+ Similarly, `{:rust_cfg_test}` on modules generates a `#[cfg(test)]` in the resulting rust module.
+ (https://github.com/dafny-lang/dafny/pull/5676)
+
+## Bug fixes
+
+- Allow hiding instance member using a static reference
+
+- Enable using "hide *" in the context of a recursive function
+
+- Support for double constant initialization in Dafny-to-Rust (https://github.com/dafny-lang/dafny/pull/5642)
+
+- Support for enumerating datatypes in the Rust backend (https://github.com/dafny-lang/dafny/pull/5643)
+
+- Tail-Recursion for the Dafny-to-Rust compiler (https://github.com/dafny-lang/dafny/pull/5647)
+
+- The new resolver (accessible using `--type-system-refresh`) can now handle revealing instance functions using a static receiver, as it is the case for the current resolver (https://github.com/dafny-lang/dafny/pull/5760)
+
+# 4.8.0
+
+## New features
+
+- Introduce `hide` statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. `Hide` statements make the opaque keyword on functions obsolete. (https://github.com/dafny-lang/dafny/pull/5562)
+
+- Let the command `measure-complexity` output which verification tasks performed the worst in terms of resource count. Output looks like:
+ ...
+ Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources
+ Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources
+ ...
+ (https://github.com/dafny-lang/dafny/pull/5631)
+
+- Enable the option `--enforce-determinism` for the commands `resolve` and `verify` (https://github.com/dafny-lang/dafny/pull/5632)
+
+- Method calls get an optional by-proof that hides the precondtion and its proof (https://github.com/dafny-lang/dafny/pull/5662)
+
+## Bug fixes
+
+- Clarify error location of inlined `is` predicates. (https://github.com/dafny-lang/dafny/pull/5587)
+
+- Optimize the compilation of single-LHS assignment statements to allow the RHS to be a deeply nested expression. This solves a problem in compiling to Java, since `javac` does not deal gracefully with nested lambda expressions. (https://github.com/dafny-lang/dafny/pull/5589)
+
+- Crash when compiling an empty source file while including testing code (https://github.com/dafny-lang/dafny/pull/5638)
+
+- Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work (https://github.com/dafny-lang/dafny/pull/5645)
+
+- Verification in the IDE now works correctly when declaring nested module in a different file than their parent. (https://github.com/dafny-lang/dafny/pull/5650)
+
+- Fix NRE that would occur when using --legacy-data-constructors (https://github.com/dafny-lang/dafny/pull/5655)
+
+# 4.7.0
+
+## New features
+
+- Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow.
+
+- Improved error reporting when verification times out or runs out of resources, so that when using `--isolate-assertions`, the error message points to the problematic assertion. (https://github.com/dafny-lang/dafny/pull/5281)
+
+- Support newtypes based on map and imap (https://github.com/dafny-lang/dafny/pull/5175)
+
+- To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. When using `dafny verify`, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag `--dont-verify-dependencies`. (https://github.com/dafny-lang/dafny/pull/5297)
+
+- Experimental Dafny-to-Rust compiler development
+ - Supports emitting code even if malformed with option `--emit-uncompilable-code`.
+ - Supports for immutable collections and operators
+ (https://github.com/dafny-lang/dafny/pull/5081)
+
+- Allow for plugins to add custom request handlers to the language server. (https://github.com/dafny-lang/dafny/pull/5161)
+
+- Deprecated the unicode-char option (https://github.com/dafny-lang/dafny/pull/5302)
+
+- Warn when passing a Dafny source file to `--library` (https://github.com/dafny-lang/dafny/pull/5313)
+
+- Add support for "translation records", which record the options used when translating library code.
+ * `--translation-record` - Provides a `.dtr` file from a previous translation of library code. Can be specified multiple times.
+ * `--translation-record-output` - Customizes where to write the translation record for the current translation. Defaults to the output directory.
+ Providing translation records is necessary to handle options such as `--outer-module` that affect how code is translated.
+ (https://github.com/dafny-lang/dafny/pull/5346)
+
+- The new `decreases to` expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (https://github.com/dafny-lang/dafny/pull/5367)
+
+- The new `assigned` expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (https://github.com/dafny-lang/dafny/pull/5501)
+
+- Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript.
+
+- Introduce additional warnings that previously only appeared when running the `dafny audit` command. Two warnings are as follows:
+ - Emit a warning when exporting a declaration that has requires clauses or subset type inputs
+ - Emit a warning when importing a declaration that has ensures clauses or subset type outputs
+Those two can be silenced with the flag `--allow-external-contracts`. A third new warning occurs when using bodyless functions marked with `{:extern}`, and can be silenced using the option `--allow-external-function`.
+
+- Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual.
+
+## Bug fixes
+
+- Fix a common memory leak that occurred when doing verification in the IDE that could easily consume gigabytes of memory.
+
+- Fix bugs that could cause the IDE to become unresponsive
+
+- Improve the performance of the Dafny IDE by fixing bugs in its caching code
+
+- No longer reuse SMT solver processes between different document version when using the IDE, making the IDE verification behavior more inline to that of the CLI
+
+- Fix bugs that caused Dafny IDE internal errors (https://github.com/dafny-lang/dafny/issues/5355, https://github.com/dafny-lang/dafny/pull/5543, https://github.com/dafny-lang/dafny/pull/5548)
+
+- Fix bugs in the Dafny IDEs code navigation and renaming features when working with definition that are not referred to.
+
+- Fix a code navigation bug that could occur when navigating to and from module imports
+-
+- Fix a code navigation bug that could occur when navigating to and from explicit types of variables
+ (https://github.com/dafny-lang/dafny/pull/5419)
+
+- Let the IDE no longer show diagnostics for projects for which all files have been closed (https://github.com/dafny-lang/dafny/pull/5437)
+
+- Fix bug that could lead to an unresponsive IDE when working with project files (https://github.com/dafny-lang/dafny/pull/5444)
+
+- Fix bugs in Dafny library files that could cause them not to work with certain option values, such as --function-syntax=3
+
+- Fix a bug that prevented building Dafny libraries for Dafny projects that could verify without errors.
+
+- Reserved module identifiers correctly escaped in GoLang (https://github.com/dafny-lang/dafny/pull/4181)
+
+- Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor (https://github.com/dafny-lang/dafny/pull/4700)
+
+- Ability to cast a datatype to its trait when overriding functions (https://github.com/dafny-lang/dafny/pull/4823)
+
+- Fix crash that could occur when using a constructor in a match pattern where a tuple was expected (https://github.com/dafny-lang/dafny/pull/4860)
+
+- No longer emit an incorrect internal error while waiting for verification message (https://github.com/dafny-lang/dafny/pull/5209)
+
+- More helpful error messages when read fields not mentioned in reads clauses (https://github.com/dafny-lang/dafny/pull/5262)
+
+- Check datatype constructors for bad type-parameter instantiations (https://github.com/dafny-lang/dafny/pull/5278)
+
+- Avoid name clashes with Go built-in modules (https://github.com/dafny-lang/dafny/pull/5283)
+
+- Invalid Python code for nested set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5287)
+
+- Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" (https://github.com/dafny-lang/dafny/pull/5295)
+
+- Rename the `dafny generate-tests` option `--coverage-report` to `--expected-coverage-report` (https://github.com/dafny-lang/dafny/pull/5301)
+
+- Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant. (https://github.com/dafny-lang/dafny/pull/5306)
+
+- No new resolver crash when datatype update expressions are partially resolved (https://github.com/dafny-lang/dafny/pull/5331)
+
+- Optional pre-type won't cause a crash anymore (https://github.com/dafny-lang/dafny/pull/5369)
+
+- Unguarded enumeration of bound variables in set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5402)
+
+- Reference the correct `this` after removing the tail call of a function or method (https://github.com/dafny-lang/dafny/pull/5474)
+
+- Apply name mangling to datatype names in Python more often (https://github.com/dafny-lang/dafny/pull/5476)
+
+- Only guard `this` when eliminating tail calls, if possible (https://github.com/dafny-lang/dafny/pull/5524)
+
+- Compiled disjunctive nested pattern matching no longer crashing (https://github.com/dafny-lang/dafny/pull/5572)
+
+# 4.6.0
+
+## New features
+
+- Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. (https://github.com/dafny-lang/dafny/pull/5097)
+
+- Add an option --progress that can be used to track the progress of verification. (https://github.com/dafny-lang/dafny/pull/5150)
+
+- Add the attribute `{:isolate_assertions}`, which does the same as `{:vcs_split_on_every_assert}`. Deprecated `{:vcs_split_on_every_assert}` (https://github.com/dafny-lang/dafny/pull/5247)
+
+## Bug fixes
+
+- (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (https://github.com/dafny-lang/dafny/pull/4844)
+
+- Add uniform checking of type characteristics in refinement modules (https://github.com/dafny-lang/dafny/pull/5146)
+
+- Fixed links associated with the standard libraries. (https://github.com/dafny-lang/dafny/pull/5176)
+
+- fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
+ feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
+ (https://github.com/dafny-lang/dafny/pull/5234)
+
+- Fix the default string value emitted for JavaScript (https://github.com/dafny-lang/dafny/pull/5239)
+
+# 4.5.0
+
+## New features
+
+- Add the option `--include-test-runner` to `dafny translate`, to enable getting the same result as `dafny test` when doing manual compilation. (https://github.com/dafny-lang/dafny/pull/3818)
+
+- - Fix: verification in the IDE no longer fails for iterators
+ - Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
+ - Fix: let the IDE correctly use the solver-path option when it's specified in a project file
+ - Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program.
+ (https://github.com/dafny-lang/dafny/pull/4798)
+
+- - Add an option `--filter-position` to the `dafny verify` command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with ``--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`
+ - Add an option `--filter-symbol` to the `dafny verify` command, that only verifies symbols whose fully qualified name contains the given argument. For example, `dafny verify dfyconfig.toml --filter-symbol=MyModule` will verify everything inside `MyModule`.
+ - The option `--boogie-filter` has been removed in favor of --filter-symbol
+ (https://github.com/dafny-lang/dafny/pull/4816)
+
+- Add a `json` format to those supported by `--log-format` and `/verificationLogger`, for producing thorough, machine readable logs of verification results. (https://github.com/dafny-lang/dafny/pull/4951)
+
+- - Flip the behavior of `--warn-deprecation` and change the name to `--allow-deprecation`, so the default is now false, which is standard for boolean options.
+ - When using `--allow-deprecation`, deprecated code is shown using tooltips in the IDE, and on the CLI when using `--show-tooltips`.
+ - Replace the option `--warn-as-error` with the option `--allow-warnings`. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous `--warn-as-error` option, warnings are always reported as warnings.
+ - During development, users must use `dafny run --allow-warnings` if they want to run their Dafny code when it contains warnings.
+ - If users have builds that were passing with warnings, they have to add `--allow-warnings` to allow them to still pass.
+ - If users upgrade to a new Dafny version, and are not using `--allow-warnings`, and do not want to migrate off of deprecated features, they will have to use `--allow-deprecation`.
+ - When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
+ - A doo file that was created using `--allow-warnings` causes a warning if used by a consumer that does not use it.
+ (https://github.com/dafny-lang/dafny/pull/4971)
+
+- The new `{:contradiction}` attribute can be placed on an `assert` statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when `--warn-contradictory-assumptions` is turned on. (https://github.com/dafny-lang/dafny/pull/5001)
+
+- Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (https://github.com/dafny-lang/dafny/pull/5032)
+
+- Under the CLI option `--general-newtypes`, the base type of a `newtype` declaration can now be (`int` or `real`, as before, or) `bool`, `char`, or a bitvector type.
+
+ `as` and `is` expressions now support more types than before. In addition, run-time type tests are supported for `is` expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both `as` and `is` allow many more useful cases than before, using `--general-newtypes` will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the `as`/`is` via `int`.
+ (https://github.com/dafny-lang/dafny/pull/5061)
+
+- Allow newtype declarations to be based on set/iset/multiset/seq. (https://github.com/dafny-lang/dafny/pull/5133)
+
+## Bug fixes
+
+- Fixed crash caused by cycle in type declaration (https://github.com/dafny-lang/dafny/pull/4471)
+
+- Fix resolution of unary minus in new resolver (https://github.com/dafny-lang/dafny/pull/4737)
+
+- The command line and the language server now use the same counterexample-related Z3 options. (https://github.com/dafny-lang/dafny/pull/4792)
+
+- Dafny no longer crashes when required parameters occur after optional ones. (https://github.com/dafny-lang/dafny/pull/4809)
+
+- Use defensive coding to prevent a crash in the IDE that could occur in the context of code actions. (https://github.com/dafny-lang/dafny/pull/4818)
+
+- Fix null-pointer problem in new resolver (https://github.com/dafny-lang/dafny/pull/4875)
+
+- Fixed a crash that could occur when a case body of a match that was inside a loop, had a continue or break statement. (https://github.com/dafny-lang/dafny/pull/4894)
+
+- Compile run-time constraint checks for newtypes in comprehensions (https://github.com/dafny-lang/dafny/pull/4919)
+
+- Fix null dereference in constant-folding invalid string-indexing expressions (https://github.com/dafny-lang/dafny/pull/4921)
+
+- Check for correct usage of type characteristics in specifications and other places where they were missing.
+
+ This fix will cause build breaks for programs with missing type characteristics (like `(!new)` and `(0)`). Any such error message is accompanied with a hint about what type characterics need to be added where.
+ (https://github.com/dafny-lang/dafny/pull/4928)
+
+- Initialize additional fields in the AST (https://github.com/dafny-lang/dafny/pull/4930)
+
+- Fix crash when a function/method with a specification is overridden in an abstract type. (https://github.com/dafny-lang/dafny/pull/4954)
+
+- Fix crash for lookup of non-existing member in new resolver (https://github.com/dafny-lang/dafny/pull/4955)
+
+- Fix: check that subset-type variable's type is determined (resolver refresh).
+ Fix crash in verifier when there was a previous error in determining subset-type/newtype base type.
+ Fix crash in verifier when a subset type has no explicit `witness` clause and has a non-reference trait as its base type.
+ (https://github.com/dafny-lang/dafny/pull/4956)
+
+- The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. The `--resource-limit` and `/rlimit` flags also now omit the multiplication, and the former allows exponential notation. (https://github.com/dafny-lang/dafny/pull/4975)
+
+- Allow a datatype to depend on traits without being told "datatype has no instances" (https://github.com/dafny-lang/dafny/pull/4997)
+
+- Don't consider `:= *` to be a definite assignment for non-ghost variables of a `(00)` type (https://github.com/dafny-lang/dafny/pull/5024)
+
+- Detect the same ghost usage in initializing assignments as in other expressions. The effect of this fix is to allow more iset/imap comprehensions to be compiled.
+
+ Also, report errors if the LHS of `:=` in compiled `map`/`imap` comprehensions contains ghosts.
+ (https://github.com/dafny-lang/dafny/pull/5041)
+
+- Escape names of nested modules in C# and Java (https://github.com/dafny-lang/dafny/pull/5049)
+
+- A parent trait that is a reference type can now be named via `import opened`.
+
+ Implicit conversions between a datatype and its parent traits no longer crashes the verifier.
+
+ (Dis)equality expressions of a (co)datatype and its parent traits no longer crashes the verifier.
+ (https://github.com/dafny-lang/dafny/pull/5058)
+
+- Fixed support for newtypes as sequence comprehension lengths in Java (https://github.com/dafny-lang/dafny/pull/5065)
+
+- Don't emit an error message for a `function-by-method` with unused type parameters. (https://github.com/dafny-lang/dafny/pull/5068)
+
+- The syntax of a predicate definition must always include parentheses. (https://github.com/dafny-lang/dafny/pull/5069)
+
+- Termination override check for certain non-reference trait implementations (https://github.com/dafny-lang/dafny/pull/5087)
+
+- Malformed Python code for some functions involving lambdas (https://github.com/dafny-lang/dafny/pull/5093)
+
+- Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types.
+
+ Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. (Previously, this had caused a crash.)
+ (https://github.com/dafny-lang/dafny/pull/5111)
+
+# 4.4.0
+
+## New features
+
+- Reads clauses on method declarations are now supported when the `--reads-clauses-on-methods` option is provided.
+ The `{:concurrent}` attribute now verifies that the `reads` and `modifies` clauses are empty instead of generating an auditor warning.
+ (https://github.com/dafny-lang/dafny/pull/4440)
+
+- Added two new options, `--warn-contradictory-assumptions` and `--warn-redundant-assumptions`, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (https://github.com/dafny-lang/dafny/pull/4542)
+
+- Verification of the `{:concurrent}` attribute on methods now allows non-empty `reads` and `modifies` clauses with the `{:assume_concurrent}` attribute. (https://github.com/dafny-lang/dafny/pull/4563)
+
+- Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/4619)
+
+- The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged. (https://github.com/dafny-lang/dafny/pull/4625)
+
+- Built-in types such as the `nat` subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
+ instead of emitted on every call to `dafny translate`, to avoid potential duplicate definitions when translating components separately.
+ (https://github.com/dafny-lang/dafny/pull/4658)
+
+- The new `--only-label` option to `merge-coverage-reports` includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification. (https://github.com/dafny-lang/dafny/pull/4673)
+
+- The Dafny distribution now includes standard libraries, available with the `--standard-libraries` option.
+ See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
+ (https://github.com/dafny-lang/dafny/pull/4678)
+
+- Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/4681)
+
+- The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime. (https://github.com/dafny-lang/dafny/pull/4755)
+
+- Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute `{:disable-nonlinear-arithmetic}`,
+ which optionally takes the value false to enable nonlinear arithmetic.
+ (https://github.com/dafny-lang/dafny/pull/4773)
+
+- Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (https://github.com/dafny-lang/dafny/pull/4855)
+
+## Bug fixes
+
+- Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (https://github.com/dafny-lang/dafny/pull/1373)
+
+- Subset type decl's witness correctly taken into account (https://github.com/dafny-lang/dafny/pull/3792)
+
+- Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations (https://github.com/dafny-lang/dafny/pull/4406)
+
+- Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. (https://github.com/dafny-lang/dafny/pull/4530)
+
+- Fix a bug that prevented certain types of lemma to be verified in the IDE (https://github.com/dafny-lang/dafny/pull/4607)
+
+- Dot completion now works on values the type of which is a type synonym. (https://github.com/dafny-lang/dafny/pull/4635)
+
+- Fix a case where the document symbol API would return incorrect data when working on a file with parse errors (https://github.com/dafny-lang/dafny/pull/4675)
+
+- Emit less nested target code in match-case expressions (nice for readability, and necessary for Java) (https://github.com/dafny-lang/dafny/pull/4683)
+
+- Ghost diagnostics are now correctly updated when they become empty (https://github.com/dafny-lang/dafny/pull/4693)
+
+- Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server (https://github.com/dafny-lang/dafny/pull/4703)
+
+- Prevent double-counting of covered/uncovered lines in test coverage reports (https://github.com/dafny-lang/dafny/pull/4710)
+
+- fix: correction of type inference for default expressions (https://github.com/dafny-lang/dafny/pull/4724)
+
+- The new type checker now also supports static reveals for instance functions (https://github.com/dafny-lang/dafny/pull/4733)
+
+- Resolve :- expressions with void outcomes in new resolver (https://github.com/dafny-lang/dafny/pull/4734)
+
+- Crash in the resolver on type parameters of opaque functions in refined modules (https://github.com/dafny-lang/dafny/pull/4768)
+
+- Fix error messages being printed after their context snippets (https://github.com/dafny-lang/dafny/pull/4787)
+
+- Override checks no longer crashing when substituting type parameters and equality (https://github.com/dafny-lang/dafny/pull/4812)
+
+- Removed one cause of need for restarting the IDE. (https://github.com/dafny-lang/dafny/pull/4833)
+
+- The Python compiler emits reserved names for datatypes (https://github.com/dafny-lang/dafny/pull/4843)
+
+# 4.3.0
+
+## New features
+
+- Add support for the Find References LSP request
+ - Returned references may be incomplete when not using project mode
+ (https://github.com/dafny-lang/dafny/pull/2320)
+
+- Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source (https://github.com/dafny-lang/dafny/pull/4255)
+
+- Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) (https://github.com/dafny-lang/dafny/pull/4326)
+
+- Add support for Rename LSP request
+ - Support requires enabling project mode and defining a Dafny project file
+ (https://github.com/dafny-lang/dafny/pull/4365)
+
+- Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. (https://github.com/dafny-lang/dafny/pull/4378)
+
+- The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a `dfyconfig.toml` can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A `dfyconfig.toml` can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the `dfyconfig.toml` resides. Project related features of the IDE are:
+ - Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly.
+ - If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed.
+ - The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file.
+ - The assisted rename feature (also added in this release), only works for files that are part of a project.
+ - When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found.
+ - If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly.
+ - The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file.
+
+ Try out the IDE's project support now by creating an empty `dfyconfig.toml` file in the root of your project repository.
+ (https://github.com/dafny-lang/dafny/pull/4435)
+
+- Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes.
+ Any such issues are reported to the user.
+ (https://github.com/dafny-lang/dafny/pull/4444)
+
+- Added documentation of the generate-tests command to the reference manual (https://github.com/dafny-lang/dafny/pull/4445)
+
+- When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. (https://github.com/dafny-lang/dafny/pull/4499)
+
+- - The Dafny IDE will now report errors that occur in project files.
+ - The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project.
+ (https://github.com/dafny-lang/dafny/pull/4539)
+
+## Bug fixes
+
+- Triggers warnings correclty converted into errors with --warn-as-errors (https://github.com/dafny-lang/dafny/pull/3358)
+
+- Allow JavaScript keywords as names of Dafny modules (https://github.com/dafny-lang/dafny/pull/4243)
+
+- Support odd characters in pathnames for Go (https://github.com/dafny-lang/dafny/pull/4257)
+
+- Allow Dafny filenames compiled to Java to start with a digit (https://github.com/dafny-lang/dafny/pull/4258)
+
+- Parser now supports files with a lot of consecutive single-line comments (https://github.com/dafny-lang/dafny/pull/4261)
+
+- Gutter icons more robust (https://github.com/dafny-lang/dafny/pull/4287)
+
+- Unresolved abstract imports no longer crash the resolver (https://github.com/dafny-lang/dafny/pull/4298)
+
+- Make capitalization of target Go code consistent (https://github.com/dafny-lang/dafny/pull/4310)
+
+- Refining an abstract module with a class with an opaque function no longer crashes (https://github.com/dafny-lang/dafny/pull/4315)
+
+- Dafny can now produce coverage reports indicating which parts of the program are expected to be covered by automatically generated tests.
+ The same functionality can be used to report other forms of coverage.
+ (https://github.com/dafny-lang/dafny/pull/4325)
+
+- Fix issue that would prevent the IDE from correctly handling default export sets (https://github.com/dafny-lang/dafny/pull/4328)
+
+- Allow function-syntax and other options with a custom default to be overridden in `dfyconfig.toml` (https://github.com/dafny-lang/dafny/pull/4357)
+
+- There were two differences between verification in the IDE and the CLI, one small and one tiny, which would only become apparent for proofs that Z3 had trouble verifying. The small difference has been resolved, while the tiny one still persists, so the IDE and CLI should behave almost equivalently now, including resource counts, on most code. (https://github.com/dafny-lang/dafny/pull/4374)
+
+- Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests (https://github.com/dafny-lang/dafny/pull/4385)
+
+- Fixed a bug leading to stack overflow during counterexample extraction on some programs. (https://github.com/dafny-lang/dafny/pull/4392)
+
+- Ability to use .Key as a constant name in datatypes and classes (https://github.com/dafny-lang/dafny/pull/4394)
+
+- Existential assertions are now printed correctly (https://github.com/dafny-lang/dafny/pull/4401)
+
+- When a symbol such as a method is not given a name, the error given by Dafny now shows where this problem occurs. (https://github.com/dafny-lang/dafny/pull/4411)
+
+- Fix flickering and incorrect results in the verification status bar, and improve responsiveness of verification diagnostics (https://github.com/dafny-lang/dafny/pull/4413)
+
+- Significantly improve IDE responsiveness for large projects, preventing it from appearing unresponsive or incorrect. Previously, for projects of a certain size, the IDE would not be able to keep up with incoming changes made by the user, possibly causing it to never catch up and appearing frozen or showing outdated results. (https://github.com/dafny-lang/dafny/pull/4419)
+
+- Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons (https://github.com/dafny-lang/dafny/pull/4432)
+
+- Fix issues that could cause the IDE status bar to show incorrect information (https://github.com/dafny-lang/dafny/pull/4454)
+
+- When verification times out, only show a red underline on the name of the verifiable for which verification timed out, instead of under its whole definition. (https://github.com/dafny-lang/dafny/pull/4477)
+
+- Prevent the IDE from becoming completely unresponsive after certain kinds of parse errors would occur. (https://github.com/dafny-lang/dafny/pull/4495)
+
+- Support all types of options in the Dafny project file (dfyconfig.toml) (https://github.com/dafny-lang/dafny/pull/4506)
+
+- Fix an issue that would cause some types of errors and other diagnostics not to appear in the IDE, if they appeared in files other than the active one. (https://github.com/dafny-lang/dafny/pull/4513)
+
+- Fix an IDE issue that would lead to exceptions when using module export declarations and making edits in imported modules that were re-exported (https://github.com/dafny-lang/dafny/pull/4556)
+
+- Fix a leak in the IDE that would cause it to become less responsive over time. (https://github.com/dafny-lang/dafny/pull/4570)
+
# 4.2.0
## New features
diff --git a/Scripts/bump_version_number.js b/Scripts/bump_version_number.js
new file mode 100644
index 00000000000..23e39fbf2cb
--- /dev/null
+++ b/Scripts/bump_version_number.js
@@ -0,0 +1,369 @@
+#!/bin/env node
+// Every comment of this file starting with //# comes from the file ../docs/dev/VERSIONBUMP.md
+// and vice-versa
+
+//# After each release, we change the version number by first running
+//# python3 Scripts/prepare_release.py NEXT_VERSION set-next-version
+//# where NEXT_VERSION is the version of the last release of the format
+//# `major.minor.patch` and the patch has been increased by 1. This script
+//# has for effect to change the version number in `Source/Directory.Build.props`.
+//# Then, many things in Dafny that depend on this version number have to be
+//# updated.
+//# This file is an exhaustive list of everything that needs to be updated
+//# whenever the version number changes. All these steps are
+//# executable by running
+//# ./Scripts/bump_version_number.js NEW_VERSION
+//# and `make bumpversion-test` run by the CI on each release
+//# verifies that this file is in sync with that script.
+
+const fs = require('fs');
+const { promisify } = require('util');
+const {exec, spawn} = require('child_process');
+const execAsync = promisify(exec);
+const minutes = 60*1000;
+const versionFile = "Source/Directory.Build.props";
+// Change the working directory to Dafny
+process.chdir(__dirname + "/..");
+const prefixLinkedComment = "//# ";
+var existingVersion = "";
+//# Assuming `` to be `Source/IntegrationTests/TestFiles/LitTests/LitTest`,
+//# perform the following:
+const TestDirectory = "Source/IntegrationTests/TestFiles/LitTests/LitTest";
+var {version, testMode} = processArgs(process.argv.slice(2)); // Remove "node" and the script's name.
+if(testMode) {
+ test();
+} else {
+ synchronizeRepositoryWithNewVersionNumber();
+}
+
+async function synchronizeRepositoryWithNewVersionNumber() {
+ existingVersion = await getVersionNumber();
+ if(version === false) {
+ version = existingVersion;
+ } else {
+ await bumpVersionNumber(version);
+ }
+ //# * Compile Dafny to ensure you have the right version number.
+ await execute("make exe");
+
+ //# * Compile the standard libraries and update their binaries which are checked in
+ await executeWithTimeout("make -C Source/DafnyStandardLibraries update-binary", 50*minutes);
+
+ //# * Recompile Dafny so that standard libraries are in the executable.
+ await execute("make exe");
+
+ //# * In the test directory `Source/IntegrationTests/TestFiles/LitTests/LitTest`,
+ await execute(
+ //# * Rebuild `pythonmodule/multimodule/PythonModule1.doo` from `pythonmodule/multimodule/dafnysource/helloworld.dfy`
+ `bash Scripts/dafny build -t:lib ${TestDirectory}/pythonmodule/multimodule/dafnysource/helloworld.dfy -o ${TestDirectory}/pythonmodule/multimodule/PythonModule1.doo`,
+ //# * Rebuild `pythonmodule/nestedmodule/SomeNestedModule.doo` from `pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy`
+ `bash Scripts/dafny build -t:lib ${TestDirectory}/pythonmodule/nestedmodule/dafnysource/SomeNestedModule.dfy -o ${TestDirectory}/pythonmodule/nestedmodule/SomeNestedModule.doo`,
+ //# * Rebuild `gomodule/multimodule/test.doo` from `gomodule/multimodule/dafnysource/helloworld.dfy`
+ `bash Scripts/dafny build -t:lib ${TestDirectory}/gomodule/multimodule/dafnysource/helloworld.dfy -o ${TestDirectory}/gomodule/multimodule/test.doo`);
+
+ //# * Search for `dafny_version = ` in checked-in `.dtr` files of the ``
+ //# and update the version number.
+ var files = await findFiles(TestDirectory, ".*\\.dtr");
+ assert_eq(files.length != 0, true);
+ for(let file of files) {
+ //# Except for the file NoGood.dtr which is not valid.
+ if(file.endsWith("NoGood.dtr")) {
+ continue;
+ }
+ //# Except for WrongDafnyVersion.dtr as well.
+ if(file.endsWith("WrongDafnyVersion.dtr")) {
+ continue;
+ }
+ await replaceInFile(/dafny_version = "\d+\.\d+\.\d+/, `dafny_version = "${version}`,
+ `${TestDirectory}/${file}`);
+ }
+
+ //# * In `Source/DafnyRuntime/DafnyRuntimeJava/build.gradle`, search for `version = ` and update the version number
+ await replaceInFile(/version = '(\d+\.\d+\.\d+)/, `version = '${version}`,
+ `Source/DafnyRuntime/DafnyRuntimeJava/build.gradle`, existingVersion);
+
+ //# * In `Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml`, search for `version = ` and update the version number
+ await replaceInFile(/version = "(\d+\.\d+\.\d+)"/, `version = "${version}"`,
+ `Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml`, existingVersion);
+
+ //# * Update `comp/separate-compilation/translation-records/InvalidFormat.dfy.expect` by updating the version number after `by Dafny `
+ await replaceInFile(/by Dafny \d+\.\d+\.\d+/, `by Dafny ${version}`,
+ `${TestDirectory}/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect`);
+
+ //# * Update the Dafny runtime version number by searching for `DafnyRuntime-` and updating the version right afterwards, in the files `DafnyPipeline.csproj` and `DafnyRuntime.csproj`
+ await replaceInFile(/DafnyRuntime-(\d+\.\d+\.\d+)\.jar/, `DafnyRuntime-${version}.jar`,
+ `Source/DafnyPipeline/DafnyPipeline.csproj`, existingVersion);
+ await replaceInFile(/DafnyRuntime-(\d+\.\d+\.\d+)\.jar/, `DafnyRuntime-${version}.jar`,
+ `Source/DafnyRuntime/DafnyRuntime.csproj`, existingVersion);
+}
+
+// Returns the current version number
+async function getVersionNumber() {
+ var versionFileContent = await fs.promises.readFile(versionFile, "utf-8");
+ var version = readVersionNumber(versionFileContent);
+ if(version === false) {
+ throw "Could not find version number in " + versionFile;
+ }
+ return version;
+}
+
+// Returns the version number from the given file content (see const versionFile)
+function readVersionNumber(versionFileContent) {
+ var versionMatch = versionFileContent.match(/(\d+\.\d+\.\d+)<\/VersionPrefix>/);
+ if(versionMatch != null) {
+ return versionMatch[1];
+ }
+ return false;
+}
+
+// Increases the patch of the given version number
+async function bumpVersionNumber(version) {
+ console.log(`Bumping version number to ${version}`);
+ var versionFileContent = await fs.promises.readFile(versionFile, "utf-8");
+ newVersionFileContent = replaceVersionNumber(versionFileContent, version);
+ if(testMode) {
+ if(newVersionFileContent === versionFileContent) {
+ throw "Expected to find " + version + " in " + versionFile;
+ }
+ console.log("Would have updated " + versionFile + " to " + newVersionFileContent);
+ return;
+ }
+ await fs.promises.writeFile(versionFile, newVersionFileContent);
+}
+
+// Replace the given version number in the given file that has the old version number
+function replaceVersionNumber(versionFileContent, newVersion) {
+ return versionFileContent.replace(/\d+\.\d+\.\d+<\/VersionPrefix>/, `${newVersion}`);
+}
+
+
+// Spawn async
+function spawnAsync(commandAndArgs) {
+ return new Promise((resolve, reject) => {
+ // Regular expression to match quoted arguments and non-quoted parts
+ const regex = /'[^']*'|"[^"]*"|\S+/g;
+
+ // Extract all matches and clean up quotes
+ const parts = commandAndArgs.match(regex).map(part => {
+ // Remove surrounding quotes (both single and double) if they exist
+ if ((part.startsWith('"') && part.endsWith('"')) ||
+ (part.startsWith("'") && part.endsWith("'"))) {
+ return part.slice(1, -1);
+ }
+ return part;
+ });
+
+ const command = parts[0];
+ const args = parts.slice(1);
+ const childProcess = spawn(command, args);
+
+ childProcess.stdout.on('data', (data) => {
+ process.stdout.write(`| ${data}`);
+ });
+
+ childProcess.stderr.on('data', (data) => {
+ process.stdout.write(`! ${data}`);
+ });
+
+ childProcess.on('close', (code) => {
+ if (code === 0) {
+ resolve();
+ } else {
+ reject(new Error(`Process exited with code ${code}`));
+ }
+ });
+ });
+}
+
+// Execute each command in its arguments
+async function execute() {
+ var commands = arguments;
+ for(let i = 0; i < commands.length; i++) {
+ let command = commands[i];
+ if(testMode) {
+ console.log("Would have run " + command);
+ } else {
+ console.log("Running " + command);
+ await spawnAsync(command);
+ }
+ }
+}
+
+// Find files in the given directory, recursively
+// Returns them with the relative path from the given directory
+async function findFiles(directory, regexString) {
+ var files = [];
+ var regexFilter = new RegExp(regexString);
+ var dir = await fs.promises.opendir(directory);
+ for await (const dirent of dir) {
+ if(dirent.isDirectory()) {
+ var subFiles = await findFiles(directory + "/" + dirent.name, regexString);
+ files = files.concat(subFiles.map(f => dirent.name + "/" + f));
+ } else if(dirent.isFile() && regexFilter.test(dirent.name)) {
+ files.push(dirent.name);
+ }
+ }
+ return files;
+}
+
+// Execute the given comment, with the possibility of timing out
+function executeWithTimeout(command, timeout) {
+ if(testMode) {
+ console.log("Would have run " + command + " with a timeout of " + timeout);
+ return new Promise((resolve, reject) => { resolve(); });
+ }
+ // Instead of having an async closure, we are going to return the promise directly
+ // so that it can be fullfilled either way.
+ return new Promise((resolve, reject) => {
+ var finished = false;
+ var childProcess = undefined;
+ var timeoutId = setTimeout(() => {
+ if(!finished) {
+ finished = true;
+ if(typeof childProcess != undefined) {
+ childProcess.kill();
+ }
+ resolve({ok: false, log: `Timeout after ${timeout/1000}s`});
+ }
+ }, timeout);
+ console.log(`Running ${command} with timeout of ${timeout/1000}s`)
+ childProcess = exec(command, (error, stdout, stderr) => {
+ clearTimeout(timeoutId);
+ finished = true;
+ if(error) {
+ resolve({ok: false, log: (error + "\n" + stderr + "\n" + stdout).trim()});
+ } else {
+ resolve({ok: true, log: stdout, answer: undefined});
+ }
+ });
+ // Add these two handlers
+ childProcess.stdout.on('data', (data) => {
+ process.stdout.write(`| ${data}`);
+ });
+
+ childProcess.stderr.on('data', (data) => {
+ process.stdout.write(`! ${data}`);
+ });
+ });
+}
+
+// Find the regex in the given file, and replaces it with the given replacement.
+async function replaceInFile(regex, replacement, fileName, testExistingVersion = null) {
+ var fileContent = await fs.promises.readFile(fileName, 'utf-8');
+ // Replace "Dafny \d.\d.\d" by the new version
+ var previous = fileContent.match(regex);
+ if(previous == null ) {
+ throw `Could not find ${regex} in ${fileName}`;
+ }
+ var newContent = fileContent.replace(regex, replacement);
+ if(testMode) {
+ if(testExistingVersion != null) {
+ assert_eq(previous[1], testExistingVersion);
+ }
+ console.log(`Would have replaced ${previous[0]} with ${replacement} in ${fileName}`);
+ if(newContent == fileContent) {
+ throw "Error in replaceInFile, replacement did not do anything";
+ }
+ } else {
+ await fs.promises.writeFile(fileName, newContent);
+ }
+}
+
+// Process the arguments.
+// If the first argument is --test, then we set the test mode where
+// we are going to read this file and verify that all lines of ../docs/dev/VERSIONBUMP.md
+// became a comment in this file.
+function processArgs(args) {
+ var testMode, version;
+ testMode = args[0] == "--test";
+ if (testMode) {
+ args = args.slice(1);
+ }
+
+ // If another argument is given, it's a version number that we can update
+ // If there is one argument, it must be the new version number.
+ var version = false;
+ if (args.length > 0) {
+ version = args[0];
+ if (!version.match(/^\d+\.\d+\.\d+$/)) {
+ console.log(`Invalid version number ${version}`);
+ process.exit(1);
+ }
+ }
+ return {version, testMode};
+}
+
+////////////////// Testing part to ensure this script is in sync /////////////
+
+async function test() {
+ await ensureTakesIntoAccountAllReleaseInstructions();
+ assert_eq(readVersionNumber(
+ "\n 1.2.3\n"), "1.2.3");
+ assert_eq(readVersionNumber(
+ " 1.2"), false);
+ assert_eq(replaceVersionNumber(
+ "\n 1.2.3\n", "1.2.4"),
+ "\n 1.2.4\n");
+ await synchronizeRepositoryWithNewVersionNumber(); // Test mode
+}
+
+// Step to ensure all the public release instructions are taken into account
+async function ensureTakesIntoAccountAllReleaseInstructions() {
+ if(version === false) {
+ version = await getVersionNumber();
+ } else {
+ await bumpVersionNumber(version);
+ }
+ // Read this file itself, and ensure every line of docs/dev/RELEASE.md
+ // appears somewhere in this file in its own line, possibly trimmed
+ var thisScript = await fs.promises.readFile(__filename, 'utf-8');
+ var publicBumpFile = 'docs/dev/VERSIONBUMP.md';
+ var publicReleaseInstructions = await fs.promises.readFile(publicBumpFile, 'utf-8');
+ var lines = publicReleaseInstructions.split("\n");
+ var thisScriptLines = thisScript.split("\n").
+ map(line => line.trim()).
+ filter(line => line.startsWith(prefixLinkedComment)).
+ map(line => line.substring(prefixLinkedComment.length).trim());
+ var missingLines = [];
+ var lineNumber = 1;
+ for(let line of lines) {
+ trimmedLine = line.trim();
+ if(trimmedLine.length > 0 && !trimmedLine.startsWith("#") && thisScriptLines.indexOf(trimmedLine) === -1) {
+ missingLines.push("//# " + line);
+ }
+ lineNumber++;
+ }
+ if(missingLines.length > 0) {
+ for(let line of missingLines) {
+ console.log(line);
+ }
+ console.log(`------------------------------------`);
+ console.log(`${missingLines.length} lines of ${publicBumpFile} were not found in ${__filename} ^^`);
+ console.log(`Please update either file.`);
+ process.exit(1);
+ }
+
+ // Now verify that each line of thisScriptLines is in the publicBumpFile
+ var extraLines = [];
+ var linesTrimmed = lines.map(line => line.trim());
+ for(let line of thisScriptLines) {
+ if(linesTrimmed.indexOf(line) === -1) {
+ extraLines.push(line);
+ }
+ }
+ if(extraLines.length > 0) {
+ for(let line of extraLines) {
+ console.log(line);
+ }
+ console.log(`------------------------------------`);
+ console.log(`${extraLines.length} comment lines of ${__filename} were not found in ${publicBumpFile} ^^`);
+ console.log(`Please update either file.`);
+ process.exit(1);
+ }
+}
+
+function assert_eq(got, expected) {
+ if(got != expected) {
+ throw "Expected " + expected + ", got " + got;
+ }
+}
\ No newline at end of file
diff --git a/Scripts/package.py b/Scripts/package.py
index f543d37715c..aaffbfe4e20 100755
--- a/Scripts/package.py
+++ b/Scripts/package.py
@@ -161,7 +161,6 @@ def build(self):
if path.exists(self.buildDirectory):
shutil.rmtree(self.buildDirectory)
run(["make", "--quiet", "clean"])
- self.run_publish("DafnyLanguageServer")
self.run_publish("DafnyServer")
self.run_publish("DafnyRuntime", "netstandard2.0")
self.run_publish("DafnyRuntime", "net452")
diff --git a/Scripts/prepare_release.py b/Scripts/prepare_release.py
index 4c8cbf0b630..bb625bb63c0 100755
--- a/Scripts/prepare_release.py
+++ b/Scripts/prepare_release.py
@@ -322,6 +322,18 @@ def _push_release_branch(self):
self.REMOTE, f"{self.release_branch_path}:{self.release_branch_path}",
check=True)
+ def set_next_version(self):
+ assert_one(f"Is {self.version} a valid version number?",
+ self._parse_vernum)
+ assert_one(f"Can we find `{self.build_props_path}`?",
+ self._build_props_file_exists)
+ assert_one(f"Can we parse `{self.build_props_path}`?",
+ self._build_props_file_parses)
+ assert_one(f"Can we create a section for `{self.version}` in `{self.release_notes_md_path}`?",
+ self._version_number_is_fresh)
+ run_one(f"Updating `{self.build_props_path}`...",
+ self._update_build_props_file)
+
# Still TODO:
# - Run deep test as part of release workflow
@@ -375,10 +387,11 @@ def prepare(self):
progress("Done!")
progress()
- DEEPTESTS_URL = "https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml"
+ DEEPTESTS_URL = "https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml"
progress(f"Now, start a deep-tests workflow manually for branch {self.release_branch_name} at\n"
- f"<{DEEPTESTS_URL}>.\n"
- "Once it completes, re-run this script with argument `release`.")
+ f"<{DEEPTESTS_URL}>\n"
+ f"To do so, click Run workflow, use workflow from {self.release_branch_name},\n"
+ f"Once it completes, just re-run this script as `./Scripts/prepare_release.py {self.version} release` to tag the branch and push it to trigger the release.")
progress()
def _tag_release(self):
@@ -429,7 +442,7 @@ def parse_arguments() -> argparse.Namespace:
parser.add_argument("--source-branch", help="Which branch to release from (optional, defaults to 'master')", default="master")
parser.add_argument("version", help="Version number for this release (A.B.C-xyz)")
parser.add_argument("action", help="Which part of the release process to run",
- choices=["prepare", "release"])
+ choices=["prepare", "release", "set-next-version"])
return parser.parse_args()
def main() -> None:
@@ -437,6 +450,7 @@ def main() -> None:
try:
release = (DryRunRelease if args.dry_run else Release)(args.version, args.source_branch)
{"prepare": release.prepare,
+ "set-next-version": release.set_next_version,
"release": release.release}[args.action]()
except CannotReleaseError:
sys.exit(1)
diff --git a/Scripts/quicktest.sh b/Scripts/quicktest.sh
index ae8053131b4..4909759f8e7 100755
--- a/Scripts/quicktest.sh
+++ b/Scripts/quicktest.sh
@@ -64,7 +64,7 @@ $DAFNY build -t:go c.dfy | diff - $tmp || exit 1
(cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go) | diff - $tmpx || exit 1
echo Building with Python
$DAFNY build -t:py c.dfy | diff - $tmp || exit 1
-python c-py/c.py | diff - $tmpx || exit 1
+python c-py/__main__.py | diff - $tmpx || exit 1
echo Building with Rust
$DAFNY build -t:rs c.dfy | diff - $tmp || exit 1
./c-rust/target/debug/c | diff - $tmpx || exit 1
diff --git a/Scripts/test-dafny.sh b/Scripts/test-dafny.sh
new file mode 100644
index 00000000000..cb684eea9aa
--- /dev/null
+++ b/Scripts/test-dafny.sh
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+# Check for required environment variables
+if [ -z "$DIR" ]; then
+ echo "Error: DIR environment variable is not set."
+ exit 1
+fi
+
+if [ -z "$name" ]; then
+ echo "Error: name environment variable is not set."
+ exit 1
+fi
+
+# Set the default build flag
+NO_BUILD=${NO_BUILD:-false}
+
+# Locate files matching the specified pattern
+files=$(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest" && find . -type f -wholename "*$name*" | grep -E '\.dfy$')
+
+if [ -z "$files" ]; then
+ echo "No files found matching pattern: $name"
+ exit 1
+else
+ count=$(echo "$files" | wc -l)
+ echo "$files"
+ echo "$count test files found."
+ for file in $files; do
+ filedir=$(dirname "$file")
+ (
+ cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$filedir" || exit
+
+ build_flag=""
+ [ "$NO_BUILD" = "true" ] && build_flag="--no-build"
+
+ dotnet run $build_flag --project "${DIR}/Source/Dafny" -- ${action} "$(basename "$file")"
+ )
+ done
+fi
\ No newline at end of file
diff --git a/Scripts/test.sh b/Scripts/test.sh
new file mode 100644
index 00000000000..c094b52c530
--- /dev/null
+++ b/Scripts/test.sh
@@ -0,0 +1,59 @@
+#!/bin/bash
+set -e
+
+# Ensure name is provided
+if [ -z "$name" ]; then
+ echo "Syntax: make test name= [update=true] [build=false]"
+ exit 1
+fi
+
+# Default values for update and build
+update_flag=${update:-false}
+build_flag=${build:-true}
+
+# Set the integration tests folder
+integration_tests_dir="${DIR}/Source/IntegrationTests"
+lit_tests_dir="${integration_tests_dir}/TestFiles/LitTests/LitTest"
+
+# Handle no-build logic
+if [ "$build_flag" = "false" ]; then
+ echo ""
+ echo "Build is disabled. Copying test files to the output directory..."
+
+ framework_dir=$(find "${integration_tests_dir}/bin/Debug" -maxdepth 1 -type d -name "net*" | sort | tail -n 1)
+ if [ -z "$framework_dir" ]; then
+ echo "Error: Could not find target framework directory in bin/Debug. Please run at least once with build=true."
+ exit 1
+ fi
+ output_dir="${framework_dir}/TestFiles/LitTests/LitTest"
+
+ # Find and copy all matching files to the output directory
+ files=$(cd "$lit_tests_dir" && find . -type f -regex '.*\.\(check\|dfy\|expect\)' -wholename "*$name*")
+ if [ -z "$files" ]; then
+ echo "No files found matching pattern: $name"
+ exit 1
+ fi
+
+ # Create output directory if it doesn't exist
+ mkdir -p "$output_dir"
+
+ # Copy files
+ echo "$files" | while IFS= read -r file; do
+ echo "Copying $file to $output_dir"
+ cp "$lit_tests_dir/$file" "$output_dir/$file"
+ done
+fi
+
+# Check if update flag is true
+if [ "$update_flag" = "true" ]; then
+ echo ""
+ echo "Update mode enabled."
+ echo "Going to update the .expect files to match the current Dafny output."
+fi
+
+# Run dotnet test
+echo "Running integration tests..."
+DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE="$update_flag" \
+dotnet test "$integration_tests_dir" \
+ $( [ "$build_flag" = "false" ] && echo "--no-build" ) \
+ --filter "DisplayName~$name"
diff --git a/Scripts/use-local-boogie.sh b/Scripts/use-local-boogie.sh
index e3e23d2c0b2..49f1f45613d 100755
--- a/Scripts/use-local-boogie.sh
+++ b/Scripts/use-local-boogie.sh
@@ -2,5 +2,5 @@ BOOGIE_PATH="boogie/"
allDlls=("Boogie.AbstractInterpretation.dll" "Boogie.BaseTypes.dll" "Boogie.CodeContractsExtender.dll" "Boogie.Concurrency.dll" "Boogie.Core.dll" "Boogie.ExecutionEngine.dll" "Boogie.Graph.dll" "Boogie.Houdini.dll" "Boogie.Model.dll" "Boogie.Predication.dll" "Boogie.Provers.SMTLib.dll" "Boogie.VCExpr.dll" "Boogie.VCGeneration.dll" "BoogieDriver.dll" "System.Configuration.ConfigurationManager.dll" "System.Runtime.Caching.dll" "System.Security.Cryptography.ProtectedData.dll" "System.Security.Permissions.dll")
for t in "${allDlls[@]}"
do
- cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net6.0/${t}" Binaries/
+ cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net8.0/${t}" Binaries/
done
diff --git a/Source/AutoExtern.Test/AutoExtern.Test.csproj b/Source/AutoExtern.Test/AutoExtern.Test.csproj
index 0c4e1dc0b51..08593d7dba6 100644
--- a/Source/AutoExtern.Test/AutoExtern.Test.csproj
+++ b/Source/AutoExtern.Test/AutoExtern.Test.csproj
@@ -2,7 +2,6 @@
Exe
- net6.0
enable
enable
false
diff --git a/Source/AutoExtern.Test/Minimal/Library.csproj b/Source/AutoExtern.Test/Minimal/Library.csproj
index 132c02c59c2..30402ac0e7a 100644
--- a/Source/AutoExtern.Test/Minimal/Library.csproj
+++ b/Source/AutoExtern.Test/Minimal/Library.csproj
@@ -1,7 +1,7 @@
- net6.0
+ net8.0
enable
enable
diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj
index 86b01ff865f..7ba274e8ce9 100644
--- a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj
+++ b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj
@@ -2,9 +2,9 @@
Exe
- net6.0
+ net8.0
enable
- CS3021; CS0162
+ CS8981; CS3021; CS0162
diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
index bdc3a6c4936..44366de2ee0 100644
--- a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
+++ b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
@@ -1,6 +1,8 @@
+Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
Dafny program verifier did not attempt verification
Wrote textual form of target program to GroceryListPrinter.cs
+Additional output written to GroceryListPrinter-cs.dtr
# Printing a grocery list
(2 items in the list)
## Apple: 3 @ 1.00
diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/LibraryModel.dfy.template b/Source/AutoExtern.Test/Tutorial/ClientApp/LibraryModel.dfy.template
index b26dde534c6..739861e177a 100644
--- a/Source/AutoExtern.Test/Tutorial/ClientApp/LibraryModel.dfy.template
+++ b/Source/AutoExtern.Test/Tutorial/ClientApp/LibraryModel.dfy.template
@@ -7,7 +7,7 @@ module {:extern "App"} {:compile false} App {}
module {:compile false} {:extern "ExactArithmetic"} App.ExactArithmetic {
import opened System
type {:compile false} {:extern} Decimal {
- function ToStr(): (s: System.String)
+ function {:axiom} ToStr(): (s: System.String)
}
}
diff --git a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj
index 132c02c59c2..30402ac0e7a 100644
--- a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj
+++ b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj
@@ -1,7 +1,7 @@
- net6.0
+ net8.0
enable
enable
diff --git a/Source/AutoExtern.Test/coverlet.runsettings b/Source/AutoExtern.Test/coverlet.runsettings
new file mode 100644
index 00000000000..11c8afc63f8
--- /dev/null
+++ b/Source/AutoExtern.Test/coverlet.runsettings
@@ -0,0 +1,12 @@
+
+
+
+
+
+
+ [*]DAST.*,[*]DCOMP.*
+
+
+
+
+
diff --git a/Source/AutoExtern/AutoExtern.csproj b/Source/AutoExtern/AutoExtern.csproj
index 0c00890cffc..f44de5524b4 100644
--- a/Source/AutoExtern/AutoExtern.csproj
+++ b/Source/AutoExtern/AutoExtern.csproj
@@ -2,7 +2,7 @@
Exe
- net6.0
+ net8.0
enable
enable
false
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 23297b185ed..91dbe9dc747 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -43,6 +43,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Scripts", "Scripts\Scripts.csproj", "{3FAB051A-1745-497B-B4C0-D49194BB5D32}"
+EndProject
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -130,6 +132,10 @@ Global
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
+ {3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Source/Dafny/Dafny.cs b/Source/Dafny/Dafny.cs
index 6de73007627..c99ff44e385 100644
--- a/Source/Dafny/Dafny.cs
+++ b/Source/Dafny/Dafny.cs
@@ -1,9 +1,10 @@
+using System.Threading.Tasks;
using Microsoft.Dafny;
namespace Dafny;
public class Dafny {
- public static int Main(string[] args) {
- return DafnyDriver.Main(args);
+ public static Task Main(string[] args) {
+ return DafnyBackwardsCompatibleCli.Main(args);
}
}
diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj
index 0ac53285657..7c639eb2b7e 100644
--- a/Source/Dafny/Dafny.csproj
+++ b/Source/Dafny/Dafny.csproj
@@ -5,7 +5,7 @@
Dafny
true
TRACE
- net6.0
+ Major
..\..\Binaries\
false
@@ -15,7 +15,7 @@
README.md
-
+
false
false
diff --git a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs
index 79daf0fd340..9a8291c09f3 100644
--- a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs
+++ b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs
@@ -6,12 +6,12 @@
public class BenchmarkingCompilerInstrumenter : CompilerInstrumenter {
public BenchmarkingCompilerInstrumenter(ErrorReporter reporter) : base(reporter) { }
- public override void Instrument(IExecutableBackend backend, SinglePassCompiler compiler, Program program) {
- if (compiler is JavaCompiler javaCompiler) {
+ public override void Instrument(IExecutableBackend backend, SinglePassCodeGenerator codeGenerator, Program program) {
+ if (codeGenerator is JavaCodeGenerator javaCompiler) {
javaCompiler.AddInstrumenter(new JavaBenchmarkCompilationInstrumenter(Reporter));
} else {
- Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, program.GetFirstTopLevelToken(),
- $"The benchmarking plugin does not support this compilation target: {compiler} (--target:{backend.TargetId})");
+ Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, program.GetStartOfFirstFileToken(),
+ $"The benchmarking plugin does not support this compilation target: {codeGenerator} (--target:{backend.TargetId})");
}
}
}
\ No newline at end of file
diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj
index badfad3b141..85823c27a94 100644
--- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj
+++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj
@@ -1,14 +1,20 @@
- net6.0
+ Major
enable
enable
..\..\Binaries\
+ MIT
+ README.md
+
+
+
+
diff --git a/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs b/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs
index 595e22f2e77..1093739a14c 100644
--- a/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs
+++ b/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs
@@ -21,7 +21,7 @@ public override void BeforeMethod(Method m, ConcreteSyntaxTree wr) {
if (Attributes.Contains(m.EnclosingClass.Attributes, "benchmarks")) {
if (m is Constructor) {
if (m.Ins.Any()) {
- Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.tok,
+ Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Origin,
$"Classes with {{:benchmarks}} can not accept parameters in their constructors");
}
@@ -34,7 +34,7 @@ public override void BeforeMethod(Method m, ConcreteSyntaxTree wr) {
wr.WriteLine("@org.openjdk.jmh.annotations.Setup(org.openjdk.jmh.annotations.Level.Iteration)");
} else if (Attributes.Contains(m.Attributes, "benchmarkTearDown")) {
if (m.Ins.Any()) {
- Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.tok,
+ Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.Origin,
$"Methods with {{:benchmarkTearDown}} can not accept parameters");
}
wr.WriteLine("@org.openjdk.jmh.annotations.TearDown(org.openjdk.jmh.annotations.Level.Iteration)");
diff --git a/Source/DafnyCore.Test/ClonerTest.cs b/Source/DafnyCore.Test/ClonerTest.cs
index 5a2b0227154..8d0dccc169a 100644
--- a/Source/DafnyCore.Test/ClonerTest.cs
+++ b/Source/DafnyCore.Test/ClonerTest.cs
@@ -1,6 +1,7 @@
using Microsoft.Dafny;
using Microsoft.Extensions.Logging;
using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
using Tomlyn;
namespace DafnyCore.Test;
@@ -10,28 +11,31 @@ class DummyDecl : Declaration {
public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
}
- public DummyDecl(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken, name,
+ public DummyDecl(IOrigin origin, Name name, Attributes attributes, bool isRefining) : base(origin, name,
attributes, isRefining) {
}
+
+ public override SymbolKind? Kind => null;
+ public override string GetDescription(DafnyOptions options) {
+ return "";
+ }
}
[Fact]
public void ClonerKeepsBodyStartTok() {
var tokenBodyStart = new Token() { line = 2 };
- var rangeToken = new RangeToken(Token.NoToken, Token.NoToken);
+ var rangeToken = new SourceOrigin(Token.NoToken, Token.NoToken);
var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1);
- var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) {
- RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+ var formal1 = new Formal(new SourceOrigin(tokenBodyStart, tokenBodyStart), "a", Microsoft.Dafny.Type.Bool, true, false, null) {
IsTypeExplicit = true
};
- var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) {
- RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+ var formal2 = new Formal(new SourceOrigin(tokenBodyStart, tokenBodyStart), "b", Microsoft.Dafny.Type.Bool, true, false, null) {
IsTypeExplicit = false
};
var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
false, false, new List(), new List { formal1, formal2 },
new List(), new List(),
- new Specification(new List(), null),
+ new Specification(), new Specification(new List(), null),
new List(), new Specification(new List(), null),
new BlockStmt(rangeToken, new List()), null, Token.NoToken, false);
@@ -39,9 +43,9 @@ public void ClonerKeepsBodyStartTok() {
var cloner = new Cloner();
var dummyDecl2 = cloner.CloneMethod(dummyDecl);
Assert.Equal(2, dummyDecl2.BodyStartTok.line);
- Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line);
+ Assert.Equal(2, dummyDecl2.Ins[0].Origin.StartToken.line);
Assert.True(dummyDecl2.Ins[0].IsTypeExplicit);
- Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line);
+ Assert.Equal(2, dummyDecl2.Ins[1].Origin.StartToken.line);
Assert.False(dummyDecl2.Ins[1].IsTypeExplicit);
}
}
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/DafnyCore.Test.csproj b/Source/DafnyCore.Test/DafnyCore.Test.csproj
index 8e9d3e8aeba..e585e29faf8 100644
--- a/Source/DafnyCore.Test/DafnyCore.Test.csproj
+++ b/Source/DafnyCore.Test/DafnyCore.Test.csproj
@@ -1,7 +1,6 @@
- net6.0
enable
enable
diff --git a/Source/DafnyCore.Test/DafnyProjectTest.cs b/Source/DafnyCore.Test/DafnyProjectTest.cs
index 836b21309bc..ca68a2ce67d 100644
--- a/Source/DafnyCore.Test/DafnyProjectTest.cs
+++ b/Source/DafnyCore.Test/DafnyProjectTest.cs
@@ -1,40 +1,37 @@
using Microsoft.Dafny;
-namespace DafnyCore.Test;
+namespace DafnyCore.Test;
public class DafnyProjectTest {
[Fact]
public void Equality() {
var randomFileName = Path.GetTempFileName();
- var first = new DafnyProject() {
- Uri = new Uri(randomFileName, UriKind.Absolute),
- Includes = new[] { "a", "a2" },
- Excludes = new[] { "b", "b2" },
- Options = new Dictionary() {
+ var first = new DafnyProject(null, new Uri(randomFileName, UriKind.Absolute), null,
+ new[] { "a", "a2" }.ToHashSet(),
+ new[] { "b", "b2" }.ToHashSet(), new Dictionary() {
{ "c", "d" },
{ "e", "f" }
}
- };
+ );
- var second = new DafnyProject() {
- Uri = new Uri(randomFileName, UriKind.Absolute),
- Includes = new[] { "a2", "a" },
- Excludes = new[] { "b2", "b" },
- Options = new Dictionary() {
+ var second = new DafnyProject(null, new Uri(randomFileName, UriKind.Absolute), null,
+ new[] { "a2", "a" }.ToHashSet(),
+ new[] { "b2", "b" }.ToHashSet(),
+ new Dictionary() {
{ "e", "f" },
{ "c", "d" },
}
- };
+ );
Assert.Equal(first, second);
- first.Options.Add("k", new[] { 1, 2, 3 });
- second.Options.Add("k", new[] { 1, 2, 3 });
+ first.Options.Add("k", "1, 2, 3");
+ second.Options.Add("k", "1, 2, 3");
Assert.Equal(first, second);
- first.Options.Add("m", new[] { 1, 2, 3 });
- second.Options.Add("m", new[] { 3, 2, 1 });
+ first.Options.Add("m", "1, 2, 3");
+ second.Options.Add("m", "3, 2, 1");
Assert.NotEqual(first, second);
}
}
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs
index 98705c6a52b..93e668fac27 100644
--- a/Source/DafnyCore.Test/DooFileTest.cs
+++ b/Source/DafnyCore.Test/DooFileTest.cs
@@ -7,15 +7,16 @@ namespace DafnyCore.Test;
public class DooFileTest {
[Fact]
- public void RoundTripCurrentVersion() {
+ public async Task RoundTripCurrentVersion() {
var options = DafnyOptions.Default;
options.ApplyDefaultOptionsWithoutSettingsDefault();
- var program = ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
+ var program = await ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
+ options.ProcessSolverOptions(program.Reporter, Token.Cli);
var dooFile = new DooFile(program);
var path = Path.GetTempFileName();
dooFile.Write(path);
- var loadedDooFile = DooFile.Read(path);
+ var loadedDooFile = await DooFile.Read(path);
Assert.Equal(loadedDooFile.Manifest.DooFileVersion, DooFile.ManifestData.CurrentDooFileVersion);
Assert.Equal(loadedDooFile.Manifest.DafnyVersion, options.VersionNumber);
@@ -30,13 +31,13 @@ public void UnknownManifestEntries() {
Assert.Throws(() => DooFile.ManifestData.Read(new StringReader(source)));
}
- private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
+ private static async Task ParseProgram(string dafnyProgramText, DafnyOptions options) {
const string fullFilePath = "untitled:foo";
var rootUri = new Uri(fullFilePath);
Microsoft.Dafny.Type.ResetScopes();
var errorReporter = new ConsoleErrorReporter(options);
- var program = new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
+ var parseResult = await new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
Assert.Equal(0, errorReporter.ErrorCount);
- return program;
+ return parseResult.Program;
}
}
diff --git a/Source/DafnyCore.Test/GeneratedDafnyTest.cs b/Source/DafnyCore.Test/GeneratedDafnyTest.cs
new file mode 100644
index 00000000000..3d4595d4e3f
--- /dev/null
+++ b/Source/DafnyCore.Test/GeneratedDafnyTest.cs
@@ -0,0 +1,26 @@
+using System.Collections.Concurrent;
+using Microsoft.Dafny;
+
+namespace DafnyCore.Test;
+
+public class GeneratedDafnyTest {
+ [Fact]
+ public void TestDafnyCoverage() {
+ DafnyToRustCompilerCoverage.__default.TestIsCopy(); ;
+ }
+
+ [Fact]
+ public void TestRustASTCoverage() {
+ RASTCoverage.__default.TestExpr();
+ }
+
+ [Fact]
+ public void TestPathSimplification() {
+ FactorPathsOptimizationTest.__default.TestApply();
+ }
+
+ [Fact]
+ public void TestDefsCoverage() {
+ DefsCoverage.__default.Tests();
+ }
+}
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs
new file mode 100644
index 00000000000..699aeffaaf2
--- /dev/null
+++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs
@@ -0,0 +1,32 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+// System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in .NET should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+// /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace DafnyToRustCompilerCoverage {
+
+ public partial class __default {
+ public static void TestIsCopy()
+ {
+ if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_Bool()))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(9,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_U128(true)))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(10,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_U128(false)))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(11,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ if (!(!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_BigInt())))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(12,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ if (!(!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_NoRange())))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(13,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ }
+ }
+} // end of namespace DafnyToRustCompilerCoverage
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs
new file mode 100644
index 00000000000..c31e0447b04
--- /dev/null
+++ b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs
@@ -0,0 +1,83 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+// System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in .NET should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+// /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace DefsCoverage {
+
+ public partial class __default {
+ public static void Expect(bool x)
+ {
+ if (!(x)) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy(17,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ }
+ public static void Tests()
+ {
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Join(Defs.AssignmentStatus.create_SurelyAssigned()), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Join(Defs.AssignmentStatus.create_NotAssigned()), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Join(Defs.AssignmentStatus.create_SurelyAssigned()), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Join(Defs.AssignmentStatus.create_NotAssigned()), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect((object.Equals((Defs.AssignmentStatus.create_Unknown()).Join(Defs.AssignmentStatus.create_NotAssigned()), (Defs.AssignmentStatus.create_NotAssigned()).Join(Defs.AssignmentStatus.create_Unknown()))) && (object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Join(Defs.AssignmentStatus.create_Unknown()), Defs.AssignmentStatus.create_Unknown())));
+ DefsCoverage.__default.Expect((object.Equals((Defs.AssignmentStatus.create_Unknown()).Join(Defs.AssignmentStatus.create_SurelyAssigned()), (Defs.AssignmentStatus.create_SurelyAssigned()).Join(Defs.AssignmentStatus.create_Unknown()))) && (object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Join(Defs.AssignmentStatus.create_Unknown()), Defs.AssignmentStatus.create_Unknown())));
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_Unknown()).Join(Defs.AssignmentStatus.create_Unknown()), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect((((object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Then(Defs.AssignmentStatus.create_Unknown()), (Defs.AssignmentStatus.create_SurelyAssigned()).Then(Defs.AssignmentStatus.create_NotAssigned()))) && (object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Then(Defs.AssignmentStatus.create_NotAssigned()), (Defs.AssignmentStatus.create_SurelyAssigned()).Then(Defs.AssignmentStatus.create_SurelyAssigned())))) && (object.Equals((Defs.AssignmentStatus.create_SurelyAssigned()).Then(Defs.AssignmentStatus.create_SurelyAssigned()), (Defs.AssignmentStatus.create_NotAssigned()).Then(Defs.AssignmentStatus.create_SurelyAssigned())))) && (object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Then(Defs.AssignmentStatus.create_SurelyAssigned()), Defs.AssignmentStatus.create_SurelyAssigned())));
+ DefsCoverage.__default.Expect((((object.Equals((Defs.AssignmentStatus.create_Unknown()).Then(Defs.AssignmentStatus.create_NotAssigned()), (Defs.AssignmentStatus.create_Unknown()).Then(Defs.AssignmentStatus.create_SurelyAssigned()))) && (object.Equals((Defs.AssignmentStatus.create_Unknown()).Then(Defs.AssignmentStatus.create_SurelyAssigned()), (Defs.AssignmentStatus.create_Unknown()).Then(Defs.AssignmentStatus.create_Unknown())))) && (object.Equals((Defs.AssignmentStatus.create_Unknown()).Then(Defs.AssignmentStatus.create_Unknown()), (Defs.AssignmentStatus.create_NotAssigned()).Then(Defs.AssignmentStatus.create_Unknown())))) && (object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Then(Defs.AssignmentStatus.create_Unknown()), Defs.AssignmentStatus.create_Unknown())));
+ DefsCoverage.__default.Expect(object.Equals((Defs.AssignmentStatus.create_NotAssigned()).Then(Defs.AssignmentStatus.create_NotAssigned()), Defs.AssignmentStatus.create_NotAssigned()));
+ Dafny.ISequence _0_x;
+ _0_x = Dafny.Sequence.UnicodeFromString("x");
+ Dafny.ISequence _1_y;
+ _1_y = Dafny.Sequence.UnicodeFromString("y");
+ DAST._IExpression _2_z;
+ _2_z = DAST.Expression.create_Ident(Dafny.Sequence.UnicodeFromString("z"));
+ Dafny.ISequence _3_assigns__x;
+ _3_assigns__x = Dafny.Sequence.FromElements(DAST.Statement.create_Assign(DAST.AssignLhs.create_Ident(_0_x), DAST.Expression.create_Ident(_1_y)));
+ Dafny.ISequence _4_assigns__y;
+ _4_assigns__y = Dafny.Sequence.FromElements(DAST.Statement.create_Assign(DAST.AssignLhs.create_Ident(_1_y), DAST.Expression.create_Ident(_0_x)));
+ DAST._IExpression _5_cond;
+ _5_cond = DAST.Expression.create_Ident(Dafny.Sequence.UnicodeFromString("cond"));
+ Dafny.ISequence _6_unknown__x;
+ _6_unknown__x = Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, _4_assigns__y));
+ Dafny.ISequence _7_surely__double__x;
+ _7_surely__double__x = Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, _3_assigns__x));
+ Dafny.ISequence _8_call__to__x;
+ _8_call__to__x = Dafny.Sequence.FromElements(DAST.Statement.create_Call(_2_z, DAST.CallName.create_SetBuilderAdd(), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(), Std.Wrappers.Option>>.create_Some(Dafny.Sequence>.FromElements(_0_x))));
+ Dafny.ISequence _9_declare__x__again;
+ _9_declare__x__again = Dafny.Sequence.FromElements(DAST.Statement.create_DeclareVar(_0_x, DAST.Type.create_Tuple(Dafny.Sequence.FromElements()), Std.Wrappers.Option.create_None()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_4_assigns__y, _0_x), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_3_assigns__x, _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_3_assigns__x, _1_y), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(_3_assigns__x, _4_assigns__y), _1_y), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_6_unknown__x, _0_x), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_7_surely__double__x, _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_7_surely__double__x, _1_y), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_8_call__to__x, _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(_8_call__to__x, _1_y), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(_8_call__to__x, _4_assigns__y), _1_y), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Labeled(Dafny.Sequence.UnicodeFromString("l"), _4_assigns__y)), _3_assigns__x), _1_y), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Labeled(Dafny.Sequence.UnicodeFromString("l"), _3_assigns__x)), _4_assigns__y), _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Labeled(Dafny.Sequence.UnicodeFromString("l"), _3_assigns__x)), _4_assigns__y), _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(_9_declare__x__again, _3_assigns__x), _0_x), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(_9_declare__x__again, _4_assigns__y), _1_y), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Return(_2_z)), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_EarlyReturn()), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_JumpTailCallStart()), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_NotAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Print(_2_z)), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Print(_2_z)), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_SurelyAssigned()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_While(_2_z, Dafny.Sequence.FromElements())), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, _4_assigns__y)))), _0_x), Defs.AssignmentStatus.create_Unknown()));
+ DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.FromElements(DAST.Statement.create_Return(_2_z)), Dafny.Sequence.FromElements())), _3_assigns__x), Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.FromElements(DAST.Statement.create_Return(_2_z)), Dafny.Sequence.FromElements())), _3_assigns__x), _4_assigns__y)))), _0_x), Defs.AssignmentStatus.create_Unknown()));
+ }
+ public static Dafny.ISequence IND { get {
+ return RAST.__default.IND;
+ } }
+ }
+} // end of namespace DefsCoverage
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
new file mode 100644
index 00000000000..04573118e97
--- /dev/null
+++ b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
@@ -0,0 +1,49 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+// System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in .NET should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+// /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace FactorPathsOptimizationTest {
+
+ public partial class __default {
+ public static void ShouldBeEqual(RAST._IMod a, RAST._IMod b)
+ {
+ Dafny.ISequence _0_sA;
+ _0_sA = (a)._ToString(Dafny.Sequence.UnicodeFromString(""));
+ Dafny.ISequence _1_sB;
+ _1_sB = (b)._ToString(Dafny.Sequence.UnicodeFromString(""));
+ if (!(_0_sA).Equals(_1_sB)) {
+ Dafny.Helpers.Print((Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Got:\n"), _0_sA), Dafny.Sequence.UnicodeFromString("\n"))).ToVerbatimString(false));
+ Dafny.Helpers.Print((Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Expected:\n"), _1_sB), Dafny.Sequence.UnicodeFromString("\n"))).ToVerbatimString(false));
+ if (!((_0_sA).Equals(_1_sB))) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(13,6): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ }
+ }
+ public static void TestApply()
+ {
+ RAST._ITypeParamDecl _0_T__Decl;
+ _0_T__Decl = RAST.TypeParamDecl.create(Dafny.Sequence.UnicodeFromString("T"), Dafny.Sequence.FromElements(RAST.__default.DafnyType));
+ RAST._ITypeParamDecl _1_T__Decl__simp;
+ _1_T__Decl__simp = RAST.TypeParamDecl.create(Dafny.Sequence.UnicodeFromString("T"), Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("DafnyType"))));
+ RAST._IType _2_T;
+ _2_T = RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("T"));
+ RAST._IPath _3_std__any__Any;
+ _3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence.UnicodeFromString("std"))).MSel(Dafny.Sequence.UnicodeFromString("any"))).MSel(Dafny.Sequence.UnicodeFromString("Any"));
+ RAST._IType _4_Any;
+ _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Any"));
+ FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(RAST.__default.NoDoc, Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements())))));
+ FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.FromElements())))));
+ FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummy"), (_3_std__any__Any).AsType(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("doit"), Std.Wrappers.Option.create_Some(((RAST.__default.std__rc__Rc).AsType()).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("unknown")))), Std.Wrappers.Option.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("something"))).ApplyType(Dafny.Sequence.FromElements(RAST.Type.create_DynType((RAST.__default.std__default__Default).AsType())))).Apply(Dafny.Sequence.FromElements(RAST.__default.std__default__Default__default, (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("rd!"))).AsExpr()).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyString"))).AsType()), ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType"))).AsType()))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__rc__Rc)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__default__Default)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("rd")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyString")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummy"), RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Any")), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("doit"), Std.Wrappers.Option.create_Some((RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Rc"))).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("unknown")))), Std.Wrappers.Option.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("something"))).ApplyType(Dafny.Sequence.FromElements(RAST.Type.create_DynType(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Default")))))).Apply(Dafny.Sequence.FromElements(((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("Default"))).FSel(Dafny.Sequence.UnicodeFromString("default"))).Apply(Dafny.Sequence.FromElements()), (RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("rd!"))).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("DafnyString"))), RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("DafnyType")))))))));
+ FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Something")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummyIntern"), (((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("nothing"))))))), RAST.Mod.create_Mod(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Something")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(RAST.__default.NoDoc, RAST.__default.NoAttr, Dafny.Sequence.UnicodeFromString("dummyIntern"), RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Something")), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("nothing")))))));
+ }
+ }
+} // end of namespace FactorPathsOptimizationTest
\ No newline at end of file
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs
new file mode 100644
index 00000000000..bebebfe2763
--- /dev/null
+++ b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs
@@ -0,0 +1,165 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+// System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in .NET should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+// /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace RASTCoverage {
+
+ public partial class __default {
+ public static void AssertCoverage(bool x)
+ {
+ if (!(x)) {
+ throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(26,4): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+ }
+ public static void TestExpr()
+ {
+ RASTCoverage.__default.TestOptimizeToString();
+ RASTCoverage.__default.TestPrintingInfo();
+ RASTCoverage.__default.TestNoExtraSemicolonAfter();
+ }
+ public static void TestNoOptimize(RAST._IExpr e)
+ {
+ }
+ public static RAST._IExpr ConversionNum(RAST._IType t, RAST._IExpr x)
+ {
+ return RAST.Expr.create_Call(RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.Path.create_PMemberSelect(RAST.Path.create_Global(), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("truncate!"))), Dafny.Sequence.FromElements(x, RAST.Expr.create_ExprFromType(t)));
+ }
+ public static RAST._IExpr DafnyIntLiteral(Dafny.ISequence