-
Notifications
You must be signed in to change notification settings - Fork 258
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
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
priority: not yet
Will reconsider working on this when we're looking for work
#1147
opened Mar 18, 2021 by
tchajed
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
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: 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
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
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)
priority: not yet
Will reconsider working on this when we're looking for work
#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)
priority: not yet
Will reconsider working on this when we're looking for work
#1162
opened Mar 29, 2021 by
tjhance
Documentation: hard to figure out how to run Boogie manually
part: documentation
Dafny's reference manual, tutorial, and other materials
priority: not yet
Will reconsider working on this when we're looking for work
#1153
opened Mar 19, 2021 by
tchajed
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
priority: not yet
Will reconsider working on this when we're looking for work
#995
opened Dec 23, 2020 by
davidcok
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
priority: not yet
Will reconsider working on this when we're looking for work
#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
priority: not yet
Will reconsider working on this when we're looking for work
#1133
opened Feb 24, 2021 by
tchajed
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
priority: not yet
Will reconsider working on this when we're looking for work
#1126
opened Feb 19, 2021 by
mschlaipfer
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
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)
priority: not yet
Will reconsider working on this when we're looking for work
#1117
opened Feb 15, 2021 by
tchajed
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
priority: not yet
Will reconsider working on this when we're looking for work
#1114
opened Feb 12, 2021 by
davidcok
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
priority: not yet
Will reconsider working on this when we're looking for work
#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
priority: not yet
Will reconsider working on this when we're looking for work
#1103
opened Feb 5, 2021 by
RustanLeino
regression in literal function unfolding proofs
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
#1097
opened Feb 3, 2021 by
tjhance
Dafny strings need a lexicographic comparison operator
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
priority: not yet
Will reconsider working on this when we're looking for work
#1070
opened Jan 28, 2021 by
davidcok
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)
priority: not yet
Will reconsider working on this when we're looking for work
status: implemented
Candidate feature available for experimentation
#1026
opened Jan 8, 2021 by
davidcok
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.