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

Emit Rust code kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#601 opened Apr 20, 2020 by johnterickson
3 ❤️ 10
Thoughts on a Dafny standard library? area: ffi The {:extern} attribute and otherwise interfacing with code in other languages kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1236 opened May 25, 2021 by parno
@wilcoxjay @parno
@RustanLeino @jaylorch
22 ❤️ 3
Dafny 4.0 suggestion: Remove automatic compile-time filtering of subset types breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2339 opened Jun 30, 2022 by MikaelMayer
3 ❤️ 2
Iterating over sets in compiled code is slow area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#2062 opened Apr 23, 2022 by robin-aws
5 ❤️ 1
Upcoming changes to Boogie part: documentation Dafny's reference manual, tutorial, and other materials
#4005 opened May 14, 2023 by shazqadeer
8 ❤️ 1
Deprecate include directives kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4988 opened Jan 15, 2024 by keyboardDrummer
1 ❤️ 1
Termination of dynamic dispatch kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1588 opened Nov 13, 2021 by RustanLeino
14 ❤️ 1
Enable the Dafny CLI to download the recommended solver version kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line
#3183 opened Dec 14, 2022 by keyboardDrummer
2 ❤️ 1
Fine-grained frame expressions for arrays kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1590 opened Nov 15, 2021 by RustanLeino
❤️ 1
Visualise verification error traces using the call-stack of a debugger 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: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3098 opened Nov 23, 2022 by keyboardDrummer
❤️ 1
Proposal: improve performance of sequences in C# runtime by making slices lazy area: performance Performance issues lang: c# Dafny's C# transpiler and its runtime part: language definition Relating to the Dafny language definition itself status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#2313 opened Jun 28, 2022 by cpitclaudel
@robin-aws
2 ❤️ 1
Grammar railroad diagram kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials part: parser First phase of Dafny's pipeline
#1244 opened Jun 6, 2021 by mingodad
@davidcok
9 ❤️ 1
Refactoring needed: Replace "Tok" with a format kind: language development speed Slows down development of Dafny the language, flaky tests
#3290 opened Dec 29, 2022 by MikaelMayer
❤️ 1
Add dafny migrate to support migration and reduce backwards compatibility requirements 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
#5407 opened May 6, 2024 by keyboardDrummer
2 ❤️ 1
dafny fails to deduce body of function across an abstract module boundary area: refinement Dafny's module-refinement machinery has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking part: verifier Translation from Dafny to Boogie (translator) status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#255 opened Jun 7, 2019 by tjhance
2
issue in datatype/module name conflict area: ffi The {:extern} attribute and otherwise interfacing with code in other languages kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#259 opened Jun 10, 2019 by gancherj
Enable hiding of functions to an extend that it could make opaque obsolete
#5575 opened Jun 25, 2024 by keyboardDrummer
@keyboardDrummer
1
Constructor should be able to call another constructor kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#295 opened Jul 5, 2019 by samuelgruetter
Feature request: Ability to state and prove running time kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#298 opened Jul 8, 2019 by saglam
1
Dafny can't model C# classes without public constructors area: ffi The {:extern} attribute and otherwise interfacing with code in other languages kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#313 opened Jul 11, 2019 by samuelgruetter
1
Predicates containing higher-order assertions behave oddly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#359 opened Aug 21, 2019 by csgordon
8
Forgetting a reads clause allows to prove false (not a soundness bug, but room for improvement) area: ffi The {:extern} attribute and otherwise interfacing with code in other languages kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#316 opened Jul 12, 2019 by samuelgruetter
1
Add built-in Map Keys to Seq function 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
#424 opened Nov 12, 2019 by lavaleri
3
Opaque functions cause failing override checks kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#422 opened Nov 12, 2019 by RustanLeino
"compilation of seq<TRAIT> is not supported"; consider introducing a ghost kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#406 opened Oct 28, 2019 by robin-aws
@RustanLeino
1
ProTip! What’s not been updated in a month: updated:<2024-05-25.