-
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
Disjunctive pattern matching not correctly handled
during 4: bad execution of correct program
A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5572
opened Jun 25, 2024 by
MikaelMayer
updated Jun 25, 2024
Flaky test: ConcurrentCompilationDoesNotBreakCaching
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: next
Will consider working on this after in progress work is done
#5515
opened May 31, 2024 by
MikaelMayer
updated Jun 25, 2024
Flaky test: LanguageServer.IntegrationTest.Lookup.SignatureHelpTest.SignatureHelpOnOpeningParenthesesReturnsSignatureOfClosestFunction
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: next
Will consider working on this after in progress work is done
#5460
opened May 17, 2024 by
MikaelMayer
updated Jun 24, 2024
Flaky Test: LanguageServer.IntegrationTest.Lookup.DocumentSymbolTest.CanResolveSymbolsForMultiFileProjects
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: next
Will consider working on this after in progress work is done
#5443
opened May 14, 2024 by
MikaelMayer
updated Jun 24, 2024
Dafny-to-Rust code generator
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
priority: now
Will work on this now
#5561
opened Jun 14, 2024 by
MikaelMayer
updated Jun 21, 2024
7 tasks
Integrate MIRI as part of the CI to ensure no memory leak in the DafnyRuntimeRust
#5567
opened Jun 21, 2024 by
MikaelMayer
updated Jun 21, 2024
Issue with multi-backend-testing
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: not yet
Will reconsider working on this when we're looking for work
#5533
opened Jun 5, 2024 by
MikaelMayer
updated Jun 20, 2024
Flaky test: Unspecified
kind: language development speed
Slows down development of Dafny the language, flaky tests
part: ci
Issue is with Dafny's CI infrastructure
priority: not yet
Will reconsider working on this when we're looking for work
#5551
opened Jun 11, 2024 by
MikaelMayer
updated Jun 20, 2024
Make the Rust compiler run on nightly once it passes all tests
part: ci
Issue is with Dafny's CI infrastructure
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
priority: now
Will work on this now
#5560
opened Jun 14, 2024 by
MikaelMayer
updated Jun 17, 2024
Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash
kind: language development speed
Slows down development of Dafny the language, flaky tests
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
priority: next
Will consider working on this after in progress work is done
#5434
opened May 13, 2024 by
MikaelMayer
updated May 21, 2024
Flaky CI Test: LanguageServer.IntegrationTest.ProjectFiles.CompetingProjectFilesTest.ProjectFileDoesNotOwnAllSourceFilesItUses
kind: language development speed
Slows down development of Dafny the language, flaky tests
priority: next
Will consider working on this after in progress work is done
#5420
opened May 10, 2024 by
MikaelMayer
updated May 21, 2024
Compiled code has useless duplicate membership test
area: performance
Performance issues
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
#5465
opened May 20, 2024 by
MikaelMayer
updated May 20, 2024
this is not fresh and fresh in well-formedness
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: v4.1.0
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
makes-mikael-grateful
This issue, is fixed, would make Mikael Mayer grateful
part: verifier
Translation from Dafny to Boogie (translator)
priority: next
Will consider working on this after in progress work is done
#4700
opened Oct 20, 2023 by
MikaelMayer
updated May 14, 2024
Empty type initialization leads to proving false
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
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: verifier
Translation from Dafny to Boogie (translator)
priority: next
Will consider working on this after in progress work is done
#5136
opened Feb 29, 2024 by
MikaelMayer
updated May 14, 2024
Prover died on simple program
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: verifier
Translation from Dafny to Boogie (translator)
#5421
opened May 10, 2024 by
MikaelMayer
updated May 14, 2024
Export sets should transitively consider subset types
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
priority: next
Will consider working on this after in progress work is done
#5417
opened May 9, 2024 by
MikaelMayer
updated May 13, 2024
Cannot prove termination of datatype / seq / generics
during 2: compilation of correct program
Dafny rejects a valid program during compilation
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
makes-mikael-grateful
This issue, is fixed, would make Mikael Mayer grateful
part: verifier
Translation from Dafny to Boogie (translator)
priority: next
Will consider working on this after in progress work is done
#4783
opened Nov 15, 2023 by
MikaelMayer
updated May 13, 2024
Stuck in verification
incompleteness
Things that Dafny should be able to prove, but can't
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5160
opened Mar 7, 2024 by
MikaelMayer
updated May 1, 2024
Crash in Boogie when using Dafny rejects a valid program during compilation
has-workaround: yes
There is a known workaround
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: boogie
Happens after passing the program to Boogie
priority: next
Will consider working on this after in progress work is done
disable-nonlinear-arithmetic
during 2: compilation of correct program
#4760
opened Nov 9, 2023 by
MikaelMayer
updated Apr 29, 2024
Specification on codatatype function triggers wrong encoding
during 2: compilation of correct program
Dafny rejects a valid program during compilation
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
priority: next
Will consider working on this after in progress work is done
#4990
opened Jan 16, 2024 by
MikaelMayer
updated Apr 29, 2024
Verification symbols not correct when a declaration is marked Bad error message or documentation; IDE bug; crash compiling invalid program
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
priority: not yet
Will reconsider working on this when we're looking for work
{:only}
during 1: program development
#4544
opened Sep 13, 2023 by
MikaelMayer
updated Apr 26, 2024
Impossible to specify type characteristics when export provides
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
#4379
opened Aug 3, 2023 by
MikaelMayer
updated Apr 25, 2024
Print a string vs option of string
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
makes-mikael-grateful
This issue, is fixed, would make Mikael Mayer grateful
priority: not yet
Will reconsider working on this when we're looking for work
#4835
opened Dec 1, 2023 by
MikaelMayer
updated Apr 24, 2024
Resolution happens x4
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
priority: not yet
Will reconsider working on this when we're looking for work
#5151
opened Mar 6, 2024 by
MikaelMayer
updated Apr 23, 2024
Feature request: Type by class with private memory
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
#5169
opened Mar 8, 2024 by
MikaelMayer
updated Apr 23, 2024
Previous Next
ProTip!
Find all open issues with in progress development work with linked:pr.