-
Notifications
You must be signed in to change notification settings - Fork 256
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
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
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
"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
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
Exception in 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
Translator.GetField
crash
#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
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
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
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
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
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
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
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
Dafny can't have a static constant called 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
IsLimit
or IsNat
, and a few others
kind: bug
#1209
opened Apr 27, 2021 by
seanmcl
Export set with type abbreviation doesn't work with 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
const
kind: bug
#1204
opened Apr 26, 2021 by
seanmcl
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
ProTip!
Add no:assignee to see everything that’s not assigned.