-
Notifications
You must be signed in to change notification settings - Fork 254
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: 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
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 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
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: 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
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
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
Boogie translation error
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
#1995
opened Apr 8, 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)
#1926
opened Mar 22, 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
{:newType}
and {:newType true}
kind: enhancement
#1919
opened Mar 18, 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)
#1914
opened Mar 16, 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
Previous Next
ProTip!
Add no:assignee to see everything that’s not assigned.