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
49 Open 82 Closed
49 Open 82 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

Incorrect printing of generically-typed strings in Go (a.k.a. should string != seq<char>?) breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends
#2582 opened Aug 11, 2022 by robin-aws
@robin-aws
15
Assert failing in strange way kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator)
#1570 opened Nov 6, 2021 by hmijail
@robin-aws
10
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
@robin-aws
9
Handle --coverage-report with dafny translate (or legacy compilation option) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4965 opened Jan 9, 2024 by codyroux
@robin-aws
6
Implement lazy sequence concatenation in remaining backends kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c++ Dafny's C++ transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime lang: python Dafny's Python transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#2390 opened Jul 11, 2022 by robin-aws
@robin-aws
6
(Idea) Implement built-in Dafny types in Dafny source code 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 part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1775 opened Feb 1, 2022 by robin-aws
@robin-aws
6
Track which compilers support which Dafny features 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
#1770 opened Jan 28, 2022 by robin-aws
@robin-aws
6
Design Proposal: Support for enumeration part: language definition Relating to the Dafny language definition itself
#1753 opened Jan 21, 2022 by robin-aws
@robin-aws
5
Move runtimes into distinct project in the solution kind: language development speed Slows down development of Dafny the language, flaky tests
#1530 opened Oct 22, 2021 by camrein
@robin-aws
5
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
@robin-aws
4
Detect and report use of mixing options that change semantics crash Dafny crashes on this input, or generates malformed code that can not be executed 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 introduced: pre-2012 invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) priority: not yet Will reconsider working on this when we're looking for work
#3556 opened Feb 16, 2023 by davidcok Library support
@robin-aws
4
Adding a check that libraries verify to nightly testing
#4034 opened May 17, 2023 by davidcok Loading…
@robin-aws
3
Consistency in array-length limits 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
#3212 opened Dec 16, 2022 by RustanLeino
@robin-aws
3
Enable specifying a remote Dafny dependency kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line
#3007 opened Nov 7, 2022 by keyboardDrummer Library support
@robin-aws
3
DafnyPipeline.Test build error kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: language development speed Slows down development of Dafny the language, flaky tests misc: cleanup Cleanups in the implementation or in corners of the language
#1565 opened Nov 5, 2021 by hirataqdees
@robin-aws
3
Outstanding issues with Dafny test support part: documentation Dafny's reference manual, tutorial, and other materials
#451 opened Dec 4, 2019 by robin-aws
@robin-aws
3
function refinement broken area: refinement Dafny's module-refinement machinery 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: java Dafny's Java transpiler and its runtime part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5366 opened Apr 25, 2024 by erniecohen
@robin-aws
2
Crash on running a program on the library backend crash Dafny crashes on this input, or generates malformed code that can not be executed 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
#5156 opened Mar 7, 2024 by robin-aws
@robin-aws
2
Support easy configuration of alternate Z3 version when installing Dafny kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3478 opened Feb 7, 2023 by robin-aws
@robin-aws
2
Enable Dafny support in Gradle 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
#3169 opened Dec 9, 2022 by keyboardDrummer Library support
@robin-aws
2
Publish nightly release to Nuget kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: ci Issue is with Dafny's CI infrastructure
#2394 opened Jul 11, 2022 by robin-aws
@robin-aws
2
Proposal: improve performance of sequences in C# runtime by making slices lazy area: performance Performance issues lang: c# Dafny's C# transpiler and its runtime part: language definition Relating to the Dafny language definition itself status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#2313 opened Jun 28, 2022 by cpitclaudel
@robin-aws
2
Improve set/map implementation for Go lang: golang Dafny's transpiler to Go and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1897 opened Mar 11, 2022 by RustanLeino
@robin-aws
2
PropagateFailure() and Result vs. Outcome kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1893 opened Mar 9, 2022 by robin-aws
@davidcok @robin-aws
2
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
ProTip! Find all open issues with in progress development work with linked:pr.