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
87 Open 125 Closed
87 Open 125 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

Flaky test Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.ProjectManagerDatabaseTest.ChangeAndUndoProjectWithMultipleFile kind: language development speed Slows down development of Dafny the language, flaky tests
#5550 by MikaelMayer was closed Jun 10, 2024
1
Flaky test: DafnyTestGeneration kind: language development speed Slows down development of Dafny the language, flaky tests
#5549 by MikaelMayer was closed Jun 11, 2024
3
Flaky CI cancelled before completing
#5530 by MikaelMayer was closed Jun 5, 2024
1
Resolution errors do not get migrated / do not disappear when there are parse errors
#5428 by MikaelMayer was closed May 14, 2024
1
Flaky test failure: dafny0/snapshots/Snapshots9.run.legacy.dfy kind: language development speed Slows down development of Dafny the language, flaky tests
#5396 by MikaelMayer was closed May 3, 2024
2
Standard libraries not working with general-newtypes=true 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 priority: now Will work on this now
#5345 by MikaelMayer was closed Apr 30, 2024
1
1
Reserved keywords in Go in need of escape 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 lang: golang Dafny's transpiler to Go and its runtime 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
#5283 by MikaelMayer was closed May 17, 2024
1
@MikaelMayer
Unhelpful error message about reads clause kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials
#5262 by MikaelMayer was closed Mar 29, 2024
1
@MikaelMayer
Resolution slowdown kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5256 by MikaelMayer was closed Apr 23, 2024
2
Error documentation improvement area: error-reporting Clarity of the error reporting
#5132 by MikaelMayer was closed Mar 21, 2024
1
dafny run file.dfy --include file.cs does not raise errors 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
#5097 by MikaelMayer was closed Mar 20, 2024
1
9
Sequence comprehension and Type descriptors issue 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
#5065 by MikaelMayer was closed Feb 7, 2024
1
Decreases clauses crashing in datatype traits 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
#4982 by MikaelMayer was closed Feb 14, 2024
@fabiomadge
3
IDE extremely slow 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)
#4917 by MikaelMayer was closed Apr 24, 2024
3
Standard libraries included twice kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release
#4858 by MikaelMayer was closed Dec 11, 2023
1
@robin-aws
1
Allocation soundness issue 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 logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful
#4844 by MikaelMayer was closed Mar 21, 2024
1
6
Cannot define subset types on kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4842 by MikaelMayer was closed Apr 24, 2024
@RustanLeino
1
Project files prevent formatting from happening correctly 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
#4836 by MikaelMayer was closed Jan 8, 2024
1
1
Dafny IDE needs restarting every 3-4 minutes kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4833 by MikaelMayer was closed Dec 1, 2023
1
Formatting gets rid of includes kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release
#4827 by MikaelMayer was closed Nov 29, 2023
1
@MikaelMayer
New type system refresh issue crash Dafny crashes on this input, or generates malformed code that can not be executed 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
#4823 by MikaelMayer was closed Apr 1, 2024
1
@RustanLeino
Dafny Language Server crashing occasionally 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
#4818 by MikaelMayer was closed Feb 9, 2024
1
Error proving override check kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4812 by MikaelMayer was closed Nov 21, 2023
1
@MikaelMayer
Abstract module + type parameter crashes Dafny kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4768 by MikaelMayer was closed Nov 15, 2023
1
2
Crash using subset type 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 release-blocker Must be resolved before the next release
#4724 by MikaelMayer was closed Nov 29, 2023
1
@jtristan
3
ProTip! no:milestone will show everything without a milestone.