Thanks for contributing to Dafny! Github is the right place to discuss feature requests, report issues with Dafny, or contact the Dafny developers. Dafny is an Open Source project and welcomes contributions.
Before reporting an issue here, consider whether it would be better handled in one of the following places:
- Stack Overflow, an online Q&A website, for help with writing and proving Dafny programs.
dafny-lang/ide-vscode
, Dafny's VSCode plugin, for issues or feature requests specific to the plugin itself. Issues with the LSP should be reported to `dafny-lang/dafny.boogie-org/boogie-friends
, Dafny's Emacs mode, for Emacs-specific problems.boogie-org/boogie
, Dafny's intermediate verification language, for questions and issues specific to Boogie.
Other issues can be reported to the Dafny project. Please include your Dafny version number, any relevant code, and expected results in the issue report.
Developers who would like to experiment with and perhaps modify Dafny source should note these resources:
- First, there are resources to learn about Dafny as a user.
- And note the community Code of Conduct expected of all participating in the project.
- The Dafny project is at github with related sibling repositories.
- Instructions for compiling Dafny are on the wiki
If you want to propose code changes for the Dafny project, please note:
- The Dafny License
- The requirement that all contributions are made under the terms of that MIT License.
- To propose code changes, use the standard Github multi-user project process, which is described for Dafny on the wiki.
If your change is user-visible, then part of the PR should be corresponding changes to the
RELEASE_NOTES.md
file and to the
Dafny Reference Manual.
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
. PRs that fix issues reported on GitHub should include a test inTest/git-issues/
.Each
.dfy
file inTest/
is a test, with alit
header describing how to run it and a.expect
file indicating the expected output. SeeTest/README.md
for more info on running Dafny' integration tests. -
Dafny's unit tests are in various
*.Test
directories inSource
.
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).
Pull Requests should be merged using 'Squash and merge' unless otherwise noted.
For pull requests that move more than a thousand lines of code from an existing to a new file, please take the following steps:
- Create a separate pull request that includes just the code move.
- Use the script found in Scripts/git-cp.sh. Running git-cp.sh src dst will copy file src to dst using a branch and a merge, and you can then remove the duplicated parts from src and dst to complete the code move (this process allows git to track the file copy, as described in this StackOverflow answer).
- Merge the pull request using 'Create a merge commit' instead of 'Squash and merge'.
If the test in a PR named Build and Test / check-deep-tests / check-deep-tests
failed, clicking on its "details" reveals a view (view 1) in which you can see a failed run with the failure being something like "Error: Last run of deep-tests.yml did not succeed (some URL in parentheses).
Clicking on this URL will reveal the deep tests that were run (view 2). If one of these tests is just a "download failure", then one simply needs to re-run it (button on the top right). Once it succeeds, one has to go back to (view 1) and re-run the failed jobs, so that it will retrieve the latest successful deep tests.
After doing these steps once, for other PRs, one only needs to re-run deep checks in (view 1)
- Create a branch (e.g.
fix-ci-<date>
) that should fix the nightly build. (Either an actual fix, or reverting a PR that caused the problem - look at the logs) - Push your branch to the main Dafny repository.
- After pushing, you'll get a link to create a PR, click on it.
- Before clicking on the "Create PR" button, add the label
run-deep-tests
. If you add it later, you will have to push a new commit to trigger the deep tests. - Click on the "Create PR" button. The CI will run the deep tests within this PR (and for every new commit pushed to the branch). Note that only the "required" tests block merging.
- 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
- Select "Run workflow..."
- Select master
- Wait for this new run to succeed.
- Now go back to all the PRs where
check-deep-tests
were failing and re-run the failing tests by updating the PRs.
Subsequent CI runs should pick up the successful deep-tests
run and make the check-deep-tests
jobs succeed.
Since dafny-lang#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
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.
Since Dafny cannot read C# files directly, you have to declare the C# functions it is calling using the {:extern}
attribute to
interoperate with Dafny.
For example, Formatting.dfy
- Defines
System.CsString
as an alias for c# strings and concatenation, so that we can interoperate with existing strings rather than using sequences of characters - Defines
CsStringEmpty
as an alias forSystem.String.Empty
- Defines
Microsoft.Dafny.HelperString.FinishesByNewline
by also using externs. That helper is defined inIndentationFormatter.cs
- Defines a trait
IIndentationFormatter
that Dafny can extend and provide toReindentProgramFromFirstToken