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,031 Open 1,599 Closed
1,031 Open 1,599 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

Misleading error message when using reserved word as first member of datatype constructor kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: parser First phase of Dafny's pipeline
#1126 opened Feb 19, 2021 by mschlaipfer
Regression in set reasoning kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1223 opened May 12, 2021 by jaylorch
1
refining module doesn't respect type parameter variance kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1217 opened May 7, 2021 by tjhance
3
Singleton datatypes are inefficiently wrapped in interfaces in Go area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: golang Dafny's transpiler to Go and its runtime
#1214 opened May 4, 2021 by tchajed
1
Export set with type abbreviation doesn't work with const kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#1204 opened Apr 26, 2021 by seanmcl
2
feature request: newtype for arbitrary base types 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 priority: not yet Will reconsider working on this when we're looking for work
#1201 opened Apr 25, 2021 by erniecohen
@keyboardDrummer
3
Feature request: bit-vector array syntax 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
#1175 opened Apr 9, 2021 by seanmcl
7
Duplicate :extern name causes crash 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: verifier Translation from Dafny to Boogie (translator)
#1170 opened Apr 3, 2021 by RustanLeino
incompleteness in sequence extensionality proofs (possibly caused by boxing) 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: verifier Translation from Dafny to Boogie (translator)
#1162 opened Mar 29, 2021 by tjhance
3
Documentation: hard to figure out how to run Boogie manually part: documentation Dafny's reference manual, tutorial, and other materials
#1153 opened Mar 19, 2021 by tchajed
@davidcok
8
Witnesses can be a performance issue in Go area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: golang Dafny's transpiler to Go and its runtime
#1147 opened Mar 18, 2021 by tchajed
1
Support compilation to PHP kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1146 opened Mar 18, 2021 by robin-aws
Feature request: ability to re-export a module kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: question Questions about Dafny's implementation. For beginner questions use "discussions" or StackOverflow
#1133 opened Feb 24, 2021 by tchajed
4
RFC: Proposal for improving module system parameterizability kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#978 opened Dec 15, 2020 by jonhnet
2
Some function allocatedness test are suppressed during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: 2.0.0 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
#1120 opened Feb 16, 2021 by RustanLeino
1
Identical lambda expressions are not considered equal kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1117 opened Feb 15, 2021 by tchajed
1
Dafny 4.0 suggestion: Dafny needs an include path 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
#1114 opened Feb 12, 2021 by davidcok
7
Using Java keyword as filename causes crash 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 lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1104 opened Feb 5, 2021 by RustanLeino
Name conflicts in target code kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime 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
#1103 opened Feb 5, 2021 by RustanLeino
Consider adopting https://allcontributors.org/ part: documentation Dafny's reference manual, tutorial, and other materials
#1099 opened Feb 3, 2021 by robin-aws
@MikaelMayer
1
Dafny strings need a lexicographic comparison operator kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1070 opened Jan 28, 2021 by davidcok
2
Add behavior of collection axioms 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 part: verifier Translation from Dafny to Boogie (translator) status: implemented Candidate feature available for experimentation
#1026 opened Jan 8, 2021 by davidcok
Resolution of names in dependency analysis 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
#995 opened Dec 23, 2020 by davidcok
Investigate unintended complications of the resolution of qualified names status: needs-info Issue requires more information from poster
#994 opened Dec 23, 2020 by davidcok
@davidcok
3
Separate compilation issues status: needs-info Issue requires more information from poster
#980 opened Dec 17, 2020 by davidcok
@keyboardDrummer
2
ProTip! Follow long discussions with comments:>50.