Skip to content

Issues: dafny-lang/dafny

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.

Sign up for GitHub

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

Clear current search query, filters, and sorts
1,021 Open 1,591 Closed
1,021 Open 1,591 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

When running many iterations, they get progressively slower until one gets stuck during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5316 opened Apr 11, 2024 by hmijail
6
Unstable test QuickEditsInLargeFile kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5304 opened Apr 5, 2024 by keyboardDrummer
@keyboardDrummer
1
Bitvectors using too much time/resources area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: boogie Happens after passing the program to Boogie part: verifier Translation from Dafny to Boogie (translator)
#5298 opened Apr 4, 2024 by seanmcl
3
Refactor reading doo manifest from Backend to AST kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny kind: language development speed Slows down development of Dafny the language, flaky tests
#5296 opened Apr 4, 2024 by ShubhamChaturvedi7
Unstable VerificationErrorDetectedAfterCanceledSave kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5292 opened Apr 3, 2024 by keyboardDrummer
@keyboardDrummer
1
Precondition of merge sort too strong during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: standard libraries Standard libraries packaged in the Dafny distribution priority: next Will consider working on this after in progress work is done
#5286 opened Apr 1, 2024 by RustanLeino
@robin-aws
Using --default-function-opacity=AutoRevealDependencies can perform badly during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#5272 opened Mar 28, 2024 by atomb
Use proof dependencies for more thorough brittleness reduction warnings kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5261 opened Mar 27, 2024 by atomb
@keyboardDrummer
6
Suggest changes that could reduce brittleness kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5259 opened Mar 27, 2024 by atomb
@atomb
1
Array initialization as powerful as constructors kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5258 opened Mar 27, 2024 by MikaelMayer
1
Free statements with ownership tracking kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5257 opened Mar 27, 2024 by MikaelMayer
Give --resource-limit a default value kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5254 opened Mar 27, 2024 by keyboardDrummer
3
Warn about potential brittleness due to use of difficult constructs kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5253 opened Mar 26, 2024 by atomb
@atomb
5
Dafny Encounters internal translation error for nested quantifier expressions when a subtitute is required during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#5250 opened Mar 26, 2024 by arminvakil
predicate subtypes of functions not propagating predicates has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't
#5245 opened Mar 23, 2024 by erniecohen
3
Incorrectly inferring type as nullable during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now
#5244 opened Mar 22, 2024 by txiang61
@ssomayyajula
1
Enable module resolution caching to work, even if the file containing the module has changed kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#5241 opened Mar 22, 2024 by keyboardDrummer
@keyboardDrummer
1
Crash on reads with different datatype ordering crash Dafny crashes on this input, or generates malformed code that can not be executed during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5232 opened Mar 21, 2024 by txiang61
1
@stefan-aws
1
Let child modules implicitly import their parent, instead of the other way around. kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself
#5227 opened Mar 21, 2024 by keyboardDrummer
2
Investigate potential bug in the filtering step of Dafny's trigger generation during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#5217 opened Mar 20, 2024 by keyboardDrummer
Instability: verification diverges when datatype taken out of module during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#5213 opened Mar 19, 2024 by erniecohen
Add VERSIONING.md kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5212 opened Mar 19, 2024 by robin-aws
@alex-chew
Support for bounded polymorphism / trait bounds kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5211 opened Mar 18, 2024 by dschoepe
1
Expand standard libraries documentation part: documentation Dafny's reference manual, tutorial, and other materials
#5207 opened Mar 16, 2024 by alexporter8013
Facilitate integration of Dafny into larger projects kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5206 opened Mar 16, 2024 by alexporter8013
4
ProTip! Type g i on any issue or pull request to go back to the issue listing page.