-
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
Wrong cyclic dependency error reported
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
#3271
opened Dec 25, 2022 by
MikaelMayer
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
[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)
[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)
[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
Implementations missings
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3071
opened Nov 17, 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
[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
TokenWrapper to be a concrete all-in-one-class instead of the token hierarchy
kind: language development speed
Slows down development of Dafny the language, flaky tests
status: designed
Issues that have a complete story on how to implement this feature and why we want it
#3354
opened Jan 11, 2023 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
Error highlighted at the default parameter site instead of the call site
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#3170
opened Dec 9, 2022 by
MikaelMayer
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
Can't prove modifies clause
area: error-reporting
Clarity of the error reporting
incompleteness
Things that Dafny should be able to prove, but can't
#3265
opened Dec 23, 2022 by
MikaelMayer
Dafny 4.0 suggestion: Get rids of Any change that will cause existing Dafny codebases to break (excluding verification instability)
misc: language proposals
Proposals for change to the language that go beyon simple enhancement requests
part: language definition
Relating to the Dafny language definition itself
returns
keyword to unify function, predicate and methods
breaking-change
#2342
opened Jun 30, 2022 by
MikaelMayer
Ghost code incorrectly rendered
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3278
opened Dec 27, 2022 by
MikaelMayer
Refactoring needed: Replace "Tok" with a format
kind: language development speed
Slows down development of Dafny the language, flaky tests
#3290
opened Dec 29, 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
priority: not yet
Will reconsider working on this when we're looking for work
#1791
opened Feb 7, 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
Language server not reporting error when z3 is not installed
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)
priority: not yet
Will reconsider working on this when we're looking for work
#1914
opened Mar 16, 2022 by
MikaelMayer
Inconsistent 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: language definition
Relating to the Dafny language definition itself
priority: not yet
Will reconsider working on this when we're looking for work
{:newType}
and {:newType true}
kind: enhancement
#1919
opened Mar 18, 2022 by
MikaelMayer
Resolution error not displayed when previous verification errors occurred
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)
priority: not yet
Will reconsider working on this when we're looking for work
#1926
opened Mar 22, 2022 by
MikaelMayer
Boogie translation error
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
#1995
opened Apr 8, 2022 by
MikaelMayer
Figure out why DocumentURI is heterogeneous
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
#2160
opened May 23, 2022 by
MikaelMayer
Cannot prove tautology with map, opaque function and transparent function.
has-workaround: yes
There is a known workaround
incompleteness
Things that Dafny should be able to prove, but can't
part: boogie
Happens after passing the program to Boogie
part: verifier
Translation from Dafny to Boogie (translator)
#2308
opened Jun 28, 2022 by
MikaelMayer
Dafny 4.0 suggestion: Any change that will cause existing Dafny codebases to break (excluding verification instability)
misc: language proposals
Proposals for change to the language that go beyon simple enhancement requests
part: language definition
Relating to the Dafny language definition itself
for i <- 0 to 10
instead of for i := 0 to 10
breaking-change
#2341
opened Jun 30, 2022 by
MikaelMayer
ProTip!
Updated in the last three days: updated:>2024-10-11.