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
876 Open 946 Closed
876 Open 946 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

Pretty printer - remove = from module imports with the same name kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST priority: not yet Will reconsider working on this when we're looking for work
#1343 opened Aug 6, 2021 by joscoh
Pretty printer spacing between decls is inconsistent kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST priority: not yet Will reconsider working on this when we're looking for work
#1342 opened Aug 6, 2021 by joscoh
sequence comprehensions are ugly 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
#1332 opened Jul 29, 2021 by jonhnet
12
Assumption failed from too deeply nested AST, resulting in a hard 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: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1331 opened Jul 27, 2021 by sorawee
2
"Dependabot can't parse your Gemfile.lock" 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 priority: not yet Will reconsider working on this when we're looking for work
#1329 opened Jul 26, 2021 by robin-aws
C# compilation error on a function returning complex sequence kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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 priority: not yet Will reconsider working on this when we're looking for work
#1326 opened Jul 25, 2021 by sorawee
Error: the type of this expression is underspecified kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1325 opened Jul 25, 2021 by sorawee
1
type inference failure for datatype methods kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1319 opened Jul 22, 2021 by jonhnet
Go compiler emits unused imports to extern modules kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#1317 opened Jul 19, 2021 by robin-aws
1
Exception in Translator.GetField 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) priority: not yet Will reconsider working on this when we're looking for work
#1316 opened Jul 19, 2021 by keyboardDrummer
Several tests don't pass on Windows 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 platform: windows Windows-specific issues priority: not yet Will reconsider working on this when we're looking for work
#1314 opened Jul 19, 2021 by keyboardDrummer
Dafny generates invalid Java code kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#1297 opened Jul 13, 2021 by sorawee
Twostate greatest predicates 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
#1296 opened Jul 13, 2021 by fpoli
1
C++ compilation error on a datatype with a type parameter kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c++ Dafny's C++ transpiler and its runtime priority: not yet Will reconsider working on this when we're looking for work
#1294 opened Jul 13, 2021 by fpoli
Type checking of match statements kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1292 opened Jul 13, 2021 by typerSniper
Output issue in compile:3 for Java kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime misc: cleanup Cleanups in the implementation or in corners of the language priority: not yet Will reconsider working on this when we're looking for work
#1291 opened Jul 13, 2021 by sorawee
4
Error reporting of wrong tuple types area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1283 opened Jul 9, 2021 by fpoli
1
Type of - inferred to be nat kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1263 opened Jun 30, 2021 by RustanLeino
5
C++ support for unconstrained ints 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 misc: update Updates to a Dafny dependency part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#1259 opened Jun 22, 2021 by robin-aws
6
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) priority: not yet Will reconsider working on this when we're looking for work
#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 priority: not yet Will reconsider working on this when we're looking for work
#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 priority: not yet Will reconsider working on this when we're looking for work
#1214 opened May 4, 2021 by tchajed
1
Dafny can't have a static constant called IsLimit or IsNat, and a few others kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: documentation Dafny's reference manual, tutorial, and other materials part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1209 opened Apr 27, 2021 by seanmcl
3
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 priority: not yet Will reconsider working on this when we're looking for work
#1204 opened Apr 26, 2021 by seanmcl
2
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 priority: not yet Will reconsider working on this when we're looking for work
#1175 opened Apr 9, 2021 by seanmcl
7
ProTip! Add no:assignee to see everything that’s not assigned.