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
86 Open 127 Closed
86 Open 127 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

Unstable CI test OpeningDocumentWithMultipleVerificationCoresReturnsStableDiagnostics misc: tests New tests or tutorials part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#2210 by MikaelMayer was closed Jun 27, 2022
@keyboardDrummer
3
Compilation error: error CS0103: The name '_td___T' does not exist in the current context area: error-reporting Clarity of the error reporting logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1679 by MikaelMayer was closed Jan 7, 2022
1
@MikaelMayer
2
Newtonsoft.json has two versions, causing crashes in development
#1722 by MikaelMayer was closed Jan 26, 2022
1
Language Server crashing under heavy load 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)
#1913 by MikaelMayer was closed Jul 8, 2022
1
1
Crash of the language server for while * 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)
#1918 by MikaelMayer was closed May 11, 2022
2
@MikaelMayer
7
Bug: Using Dafny.dll to build an AST fails if no compiler specified. kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: parser First phase of Dafny's pipeline
#1932 by MikaelMayer was closed Mar 31, 2022
2
@MikaelMayer
6
Reads is checked even if nothing needs to be checked. kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1953 by MikaelMayer was closed Apr 29, 2022
1
@MikaelMayer
Null pointer exception on underconstrained closures crash Dafny crashes on this input, or generates malformed code that can not be executed 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)
#2074 by MikaelMayer was closed Jul 11, 2022
1
@MikaelMayer
1
Language server not robust enough and multiset keyword crash crash Dafny crashes on this input, or generates malformed code that can not be executed 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) part: parser First phase of Dafny's pipeline
#2078 by MikaelMayer was closed May 2, 2022
1
@MikaelMayer
1
Language server no longer sending diagnostics on untitled files 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)
#2147 by MikaelMayer was closed May 23, 2022
1
@MikaelMayer
DafnyLanguageServer Test stability issue
#2151 by MikaelMayer was closed May 19, 2022
Ranges are not highlighted properly area: error-reporting Clarity of the error reporting 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)
#2197 by MikaelMayer was closed Jul 11, 2022
1
@MikaelMayer
Reference types in comprehension soundness issue 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) part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#1604 by MikaelMayer was closed Apr 12, 2022
1
@MikaelMayer
Language server crashing when adding {:opaque} on datatype predicate. crash Dafny crashes on this input, or generates malformed code that can not be executed 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)
#2207 by MikaelMayer was closed Jun 7, 2022
1
2
Stressing the Language Server: Failure 1
#2237 by MikaelMayer was closed Jun 15, 2022
2
LSP Crashes during editing because failed position crash Dafny crashes on this input, or generates malformed code that can not be executed 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)
#2246 by MikaelMayer was closed Jul 8, 2022
@MikaelMayer
7
Crash on hover crash Dafny crashes on this input, or generates malformed code that can not be executed 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)
#2333 by MikaelMayer was closed Jul 1, 2022
1
2
Dafny 4.0 suggestion: opaque keyword breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2337 by MikaelMayer was closed Feb 8, 2023 Dafny 4.0
1
@RustanLeino
17
Automatic priority on verification never worked + misleading "verifying" gutter icons area: performance Performance issues has-workaround: no There are no known workarounds part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#2347 by MikaelMayer was closed Jul 8, 2022
1
1
Verification diagnostics not updated correctly 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) priority: not yet Will reconsider working on this when we're looking for work
#2349 by MikaelMayer was closed Sep 23, 2022
@keyboardDrummer
1
Dafny 4.0 suggestion: Remove the -compile and -spillTargetCode option breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: tools Tools built on top of Dafny
#2351 by MikaelMayer was closed Aug 12, 2022
5
Incompleteness in map cardinality equality incompleteness Things that Dafny should be able to prove, but can't
#2380 by MikaelMayer was closed Jul 31, 2023
1
@cpitclaudel
1
Crash on refinement crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#2402 by MikaelMayer was closed Nov 9, 2022
1
Hovering crashes the LSP (but recovers) 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)
#2438 by MikaelMayer was closed Jul 29, 2022
1
@MikaelMayer
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 by MikaelMayer was closed Jun 26, 2024
1
ProTip! no:milestone will show everything without a milestone.