Skip to content

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.

Sign up for GitHub

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

Clear current search query, filters, and sorts
85 Open 125 Closed
85 Open 125 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Dafny-to-Rust code generator
#5561 opened Jun 14, 2024 by MikaelMayer
6 tasks
Revert #5559 when the Rust compiler passes all tests
#5560 opened Jun 14, 2024 by MikaelMayer
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: unknown We have not evaluated the priority of this issue
#5551 opened Jun 11, 2024 by MikaelMayer
Issue with multi-backend-testing kind: language development speed Slows down development of Dafny the language, flaky tests priority: unknown We have not evaluated the priority of this issue
#5533 opened Jun 5, 2024 by MikaelMayer
Flaky test: ConcurrentCompilationDoesNotBreakCaching kind: language development speed Slows down development of Dafny the language, flaky tests
#5515 opened May 31, 2024 by MikaelMayer
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
Flaky test: LanguageServer.IntegrationTest.Lookup.SignatureHelpTest.SignatureHelpOnOpeningParenthesesReturnsSignatureOfClosestFunction kind: language development speed Slows down development of Dafny the language, flaky tests
#5460 opened May 17, 2024 by MikaelMayer
2
Flaky Test: LanguageServer.IntegrationTest.Lookup.DocumentSymbolTest.CanResolveSymbolsForMultiFileProjects kind: language development speed Slows down development of Dafny the language, flaky tests
#5443 opened May 14, 2024 by MikaelMayer
@keyboardDrummer
2
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
1
@keyboardDrummer
7
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
2
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
@keyboardDrummer
11
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
@MikaelMayer
Compilation to not use a global local variable counter, but a local one kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5330 opened Apr 17, 2024 by MikaelMayer
1
Array initialization as powerful as constructors kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5258 opened Mar 27, 2024 by MikaelMayer
1
Free statements with ownership tracking kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5257 opened Mar 27, 2024 by MikaelMayer
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
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
7
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
@keyboardDrummer
1
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
@stefan-aws
4
Having doo files part of the git index prevents agile development area: build-system Support for dependencies in Dafny, generation of target language build files kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5057 opened Feb 6, 2024 by MikaelMayer
1
@robin-aws
1
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
Class datatypes kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4882 opened Dec 14, 2023 by MikaelMayer
6
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
1
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
@MikaelMayer
Crash in Boogie when using disable-nonlinear-arithmetic during 2: compilation of correct program 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
#4760 opened Nov 9, 2023 by MikaelMayer
6
ProTip! What’s not been updated in a month: updated:<2024-05-16.