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
1,021 Open 1,591 Closed
1,021 Open 1,591 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
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-encryption-sdk-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5486 opened May 23, 2024 by aws-crypto-tools-ci-bot updated Jun 25, 2024
36
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
#5565 opened Jun 18, 2024 by aws-crypto-tools-ci-bot updated Jun 25, 2024
7
Dafny Go runtime (Binaries/DafnyRuntime.go) should be published as a Go module kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: golang Dafny's transpiler to Go and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#494 opened Jan 10, 2020 by robin-aws updated Jun 25, 2024
@atomb
1
Enable hiding of functions to an extend that it could make opaque obsolete
#5575 opened Jun 25, 2024 by keyboardDrummer updated Jun 25, 2024
@keyboardDrummer
1
Costless by clause in assert .. by { } when using --isolate-assertions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: boogie Happens after passing the program to Boogie priority: not yet Will reconsider working on this when we're looking for work
#5536 opened Jun 6, 2024 by keyboardDrummer updated Jun 25, 2024
@keyboardDrummer
3
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
1
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
1
3
New Logo for Dafny part: documentation Dafny's reference manual, tutorial, and other materials priority: not yet Will reconsider working on this when we're looking for work
#4324 opened Jul 23, 2023 by booniepepper updated Jun 25, 2024
17
Nested LetExpr chain compiles to tons of nested Java lambdas, which javac chokes on kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
#3868 opened Apr 13, 2023 by robin-aws updated Jun 25, 2024
1
3
Malformed Boogie for if-then-else with non-reference traits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5570 opened Jun 24, 2024 by RustanLeino updated Jun 24, 2024
Ordering problem in Python code generator kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#5569 opened Jun 24, 2024 by RustanLeino updated Jun 24, 2024
Unstable test ChangeAndUndoProjectWithMultipleFiles 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
#5510 opened May 30, 2024 by keyboardDrummer updated Jun 24, 2024
@keyboardDrummer
3
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
2
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
@keyboardDrummer
2
Unstable test ChangingTheDocumentStopsOnChangeVerification 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
#5436 opened May 14, 2024 by keyboardDrummer updated Jun 24, 2024
@keyboardDrummer
2
Unstable test due to timeout when executing Rust back-end 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
#5321 opened Apr 15, 2024 by keyboardDrummer updated Jun 24, 2024
1
Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long 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
#5488 opened May 24, 2024 by keyboardDrummer updated Jun 24, 2024
@robin-aws
9
Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now release-blocker Must be resolved before the next release
#5555 opened Jun 12, 2024 by robin-aws updated Jun 24, 2024
@robin-aws
4
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
Verification hang apparently caused by Std import 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: standard libraries Standard libraries packaged in the Dafny distribution priority: not yet Will reconsider working on this when we're looking for work
#5534 opened Jun 6, 2024 by nverhaaren updated Jun 20, 2024
3
Dafny language server does not clean up z3 child processes 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
#5376 opened Apr 28, 2024 by mitchellholt updated Jun 20, 2024
3
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: not yet Will reconsider working on this when we're looking for work
#5381 opened Apr 29, 2024 by dschoepe updated Jun 20, 2024
4
Support (!new) on trait kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work
#5395 opened May 2, 2024 by txiang61 updated Jun 20, 2024
1
Verification ignores resource limits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: z3 Issue is in Z3 priority: not yet Will reconsider working on this when we're looking for work
#5525 opened Jun 4, 2024 by hmijail updated Jun 20, 2024
6
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.