-
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
Dafny 4.0 suggestion: Remove automatic compile-time filtering of subset types
breaking-change
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
#2339
opened Jun 30, 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
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
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
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
var
pattern matching
breaking-change
#2343
opened Jun 30, 2022 by
MikaelMayer
Dafny 4.0 suggestion: get modern assignment operators
breaking-change
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
#2345
opened Jun 30, 2022 by
MikaelMayer
Assertion splits should display related locations
area: error-reporting
Clarity of the error reporting
part: verifier
Translation from Dafny to Boogie (translator)
#2348
opened Jul 1, 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
Dafny 4.0 suggestion: Break up {:extern} and support language specificities
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
misc: cleanup
Cleanups in the implementation or in corners of the language
misc: language proposals
Proposals for change to the language that go beyon simple enhancement requests
#2397
opened Jul 12, 2022 by
MikaelMayer
Unstable priority ordering test
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#2422
opened Jul 15, 2022 by
MikaelMayer
Dafny 4.0 suggestion: Line and Column indexed the same
breaking-change
Any change that will cause existing Dafny codebases to break (excluding verification instability)
#2452
opened Jul 19, 2022 by
MikaelMayer
Bug: Internal parse error.
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
#2466
opened Jul 21, 2022 by
MikaelMayer
Undeclared top-level issue
area: error-reporting
Clarity of the error reporting
#2550
opened Aug 4, 2022 by
MikaelMayer
Crash in translation to Boogie
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)
#2584
opened Aug 12, 2022 by
MikaelMayer
Missing where clause on handle types and incorrect subtyping checks on maps containing arrows
has-workaround: yes
There is a known workaround
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: resolver
Resolution and typechecking
part: verifier
Translation from Dafny to Boogie (translator)
#2835
opened Oct 3, 2022 by
MikaelMayer
At-attributes - new language feature
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5795
opened Sep 26, 2024 by
MikaelMayer
Function precondition might not hold without hint
area: error-reporting
Clarity of the error reporting
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)
#2918
opened Oct 24, 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)
Dafny 4 suggestion: Replace subset types "type" by "predicate type"
breaking-change
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
#2368
opened Jul 6, 2022 by
MikaelMayer
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.