-
Notifications
You must be signed in to change notification settings - Fork 260
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
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
CI only builds the reference manual on macos
part: documentation
Dafny's reference manual, tutorial, and other materials
priority: not yet
Will reconsider working on this when we're looking for work
#1315
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
Lack of qualified type names makes error messages unclear
area: error-reporting
Clarity of the error reporting
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
#1309
opened Jul 15, 2021 by
joscoh
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
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
priority: not yet
Will reconsider working on this when we're looking for work
#1244
opened Jun 6, 2021 by
mingodad
Officially recommended way to use Dafny code from other languages?
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
misc: question
Questions about Dafny's implementation. For beginner questions use "discussions" or StackOverflow
part: documentation
Dafny's reference manual, tutorial, and other materials
priority: not yet
Will reconsider working on this when we're looking for work
#1239
opened May 31, 2021 by
hmijail
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)
priority: not yet
Will reconsider working on this when we're looking for work
#1236
opened May 25, 2021 by
parno
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
ProTip!
Adding no:label will show everything without a label.