Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support all option types in the project file #4506

Merged
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
0beaffb
Support all option types in the project file
keyboardDrummer Sep 1, 2023
4946ac6
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
7a6914d
Add release note and fix path resolution in Dafny project file
keyboardDrummer Sep 7, 2023
81c7863
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 7, 2023
8b3b1ee
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
32c61ba
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
e913591
Fixes for using library in options
keyboardDrummer Sep 8, 2023
c89fd32
Update release notes
keyboardDrummer Sep 8, 2023
327817f
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 8, 2023
8df76c8
Run formatter
keyboardDrummer Sep 8, 2023
9e29a2a
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 8, 2023
7dde794
More fixes
keyboardDrummer Sep 8, 2023
19ca042
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 8, 2023
177f6cb
Trigger CI
keyboardDrummer Sep 10, 2023
3146dc2
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 10, 2023
e6a4a50
usesLibrary test now passes
keyboardDrummer Sep 11, 2023
d52dd2c
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
e7c0a23
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
282a0ec
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
5e499c2
Make test more stable
keyboardDrummer Sep 12, 2023
bbab8ae
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 12, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update release notes
  • Loading branch information
keyboardDrummer committed Sep 8, 2023
commit c89fd3261fb7fae06925e0d2e0e1cfe9cb88f5a5
8 changes: 4 additions & 4 deletions docs/dev/news/4435.feat
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
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 in 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.
- 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.
- 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.
- For files that are part of a project, the Dafny IDE does not require the use of include directives to work, and neither does the CLI if you run it using the project file. This means that Dafny projects can be used without use include directives for files inside the project. When using library files that are outside the project, it's still necessary to use includes.
- 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.
Loading