-
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
Error ranges include non-relevant places
during 1: program development
Bad error message or documentation; IDE bug; crash compiling invalid program
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3176
opened Dec 11, 2022 by
MikaelMayer
Assert for the elephant let-or-fail operator in expressions
difficulty: good-first-issue
Good first issues
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
part: parser
First phase of Dafny's pipeline
#1791
opened Feb 7, 2022 by
MikaelMayer
[Feature request]: Assert simplification calculus (a.k.a. verification debugging or "Move assert up") with Code Actions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3114
opened Nov 25, 2022 by
MikaelMayer
[Feature request]: Weakest Precondition calculus (a.k.a. verification debugging or "Move assert up") with Code Actions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3102
opened Nov 23, 2022 by
MikaelMayer
[Feature request]: Name assertions in functions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3101
opened Nov 23, 2022 by
MikaelMayer
Misleading "verified" gutter icon
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3076
opened Nov 18, 2022 by
MikaelMayer
Implementations missings
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3071
opened Nov 17, 2022 by
MikaelMayer
[Bug]: Cannot declare extern ToString in C#
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
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
#3039
opened Nov 10, 2022 by
MikaelMayer
[Feature request]: Documentation on hover
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
[Feature request]: Generate explicit assertions
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
Unsound use of A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
introduced: pre-2012
{this}
in constant initialization
during 4: bad execution of correct program
#2923
opened Oct 25, 2022 by
MikaelMayer
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.