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

997 Open 1,560 Closed
997 Open 1,560 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

[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
#5462 opened May 17, 2024 by robin-aws
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
Translation records should not include options for empty models kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny release-blocker Must be resolved before the next release
#5459 opened May 17, 2024 by robin-aws
@robin-aws
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
#5449 opened May 15, 2024 by aws-crypto-tools-ci-bot
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
1
Unstable test ChangingTheDocumentStopsOnChangeVerification kind: language development speed Slows down development of Dafny the language, flaky tests
#5436 opened May 14, 2024 by keyboardDrummer
@keyboardDrummer
strange assertion failure incompleteness Things that Dafny should be able to prove, but can't
#5435 opened May 14, 2024 by toNanjingnan
1
Nighty failed because a MacOS node timed out 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
#5432 opened May 13, 2024 by keyboardDrummer
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
10
Standard Library: Parser combinators part: standard libraries Standard libraries packaged in the Dafny distribution
#5418 opened May 9, 2024 by robin-aws
1
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
--warn-missing-constructor-parentheses doesn't warn when missing constructor arguments kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5409 opened May 6, 2024 by robin-aws
@alex-chew
Add dafny migrate to support migration and reduce backwards compatibility requirements kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny kind: language development speed Slows down development of Dafny the language, flaky tests
#5407 opened May 6, 2024 by keyboardDrummer
2
forall statement and expression syntax gratuitously inconsistent -> horrible error messages LOW SEVERITY 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
#5404 opened May 6, 2024 by kjx
4
non-non-non-optional semicolons give horrible error messages - LOW SEVERITY area: error-reporting Clarity of the error reporting 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
#5403 opened May 6, 2024 by kjx
3
Clean up gomodule tests to not check in generated content kind: language development speed Slows down development of Dafny the language, flaky tests
#5399 opened May 3, 2024 by robin-aws
@ShubhamChaturvedi7
internal error on match with static const of newtype 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
#5405 opened May 3, 2024 by erniecohen
@keyboardDrummer
2
Support (!new) on trait kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: unknown We have not evaluated the priority of this issue
#5395 opened May 2, 2024 by txiang61
1
Type checking sometimes doesn't terminate when using --type-system-refresh 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: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5385 opened May 1, 2024 by dschoepe
@keyboardDrummer
1
Flaky test failure: Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles.StandardLibrary.EditWhenUsingStandardLibrary kind: language development speed Slows down development of Dafny the language, flaky tests
#5384 opened Apr 30, 2024 by robin-aws
4
fresh doesn't imply inequality with --general-traits=datatype 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: unknown We have not evaluated the priority of this issue
#5381 opened Apr 29, 2024 by dschoepe
4
Missing autocut step from some downstream customer nightly tests priority: next Will consider working on this after in progress work is done release-blocker Must be resolved before the next release
#5379 opened Apr 29, 2024 by robin-aws
@robin-aws
Dafny language server does not clean up z3 child processes kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: unknown We have not evaluated the priority of this issue
#5376 opened Apr 28, 2024 by mitchellholt
3
Add dedicated content on determinism and methods vs. functions to the reference manual part: documentation Dafny's reference manual, tutorial, and other materials priority: next Will consider working on this after in progress work is done
#5372 opened Apr 26, 2024 by robin-aws
@stefan-aws
ProTip! Adding no:label will show everything without a label.