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,046 Open 1,614 Closed
1,046 Open 1,614 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

/useBaseNameForFileName and /showSnippets:1 can't be used together area: error-reporting Clarity of the error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#1518 opened Oct 18, 2021 by robin-aws
@davidcok
Hint when tuples are used in decreases clauses difficulty: good-first-issue Good first issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1517 opened Oct 15, 2021 by RustanLeino
enhancement: renaming area: refinement Dafny's module-refinement machinery kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1503 opened Oct 10, 2021 by erniecohen
Ignored test: ChangeDocumentRightAfterOpeningCancelsLoad kind: language development speed Slows down development of Dafny the language, flaky tests misc: cleanup Cleanups in the implementation or in corners of the language
#1493 opened Oct 6, 2021 by robin-aws
Resolution crash when refining a module and defining a const with a subset type area: refinement Dafny's module-refinement machinery crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1481 opened Oct 3, 2021 by robin-aws
refined traits/classes should be able to add trait extensions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1471 opened Sep 30, 2021 by erniecohen
Refining abstract module with class that extends foreign trait results in a crash area: refinement Dafny's module-refinement machinery crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#1469 opened Sep 29, 2021 by unboxedtype
axioms in traits should not have to be implemented in extending classes kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#1466 opened Sep 29, 2021 by erniecohen
Evaluate sequence slices (and potentially other operations) lazily in the runtimes area: performance Performance issues 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)
#1460 opened Sep 24, 2021 by robin-aws
Solver does not abide by /timeLimit kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1457 opened Sep 23, 2021 by RustanLeino
Feature request: C# .Equals based on properties, not ref equality. Records? kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c# Dafny's C# transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1451 opened Sep 22, 2021 by hmijail
confusing line number in error message for conjuncts in forall area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1442 opened Sep 17, 2021 by tjhance
Incorrect type error kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1440 opened Sep 17, 2021 by fpoli
Incorrect compile-time error reporting: NullReferenceException crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1438 opened Sep 15, 2021 by sorawee
Info tool tips repeated during export consistency checks kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1433 opened Sep 13, 2021 by RustanLeino
Lemmas not working properly inside of old() kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1421 opened Sep 7, 2021 by erniecohen
traits with {:autocontracts} should not fully define Valid() by default kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1418 opened Sep 7, 2021 by erniecohen
NullReferenceException in Compiler crash Dafny crashes on this input, or generates malformed code that can not be executed 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
#1411 opened Sep 1, 2021 by IsaacOscar
Feature request: casting a map<X, Y> as an imap<X, Y> 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
#1408 opened Aug 31, 2021 by robin-aws
Feature request: comparison operations on (i)maps 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
#1407 opened Aug 31, 2021 by robin-aws
module cycle detection assumes refines/imports A.B takes a dependence on A kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#1403 opened Aug 28, 2021 by erniecohen
Problem with set of arrays kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime lang: js Dafny's JavaScript transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1402 opened Aug 28, 2021 by sorawee
internal translation error for type parameter kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1401 opened Aug 28, 2021 by IsaacOscar
C#: compilation error on if expression of arrow type kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1396 opened Aug 27, 2021 by sorawee
assumption not used within quantified assert kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1371 opened Aug 22, 2021 by erniecohen
ProTip! Type g i on any issue or pull request to go back to the issue listing page.