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
48 Open 83 Closed
48 Open 83 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

Compiler.ReportError uses hardcoded comment syntax kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: cleanup Cleanups in the implementation or in corners of the language part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#1729 opened Jan 19, 2022 by cpitclaudel
@robin-aws
Design Proposal: Maintain exact verification behaviour within major versions of Dafny part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#1740 opened Jan 21, 2022 by robin-aws Verification Durability
@robin-aws
Provide targeted test cases for new compilers 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 priority: not yet Will reconsider working on this when we're looking for work
#1776 opened Feb 1, 2022 by robin-aws
@robin-aws
for loop turns into illegal decreases-* in iterator kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work
#1793 opened Feb 7, 2022 by RustanLeino
@robin-aws
docs: Completed (and corrected) IteratorSpec section
#1842 opened Feb 19, 2022 by robin-aws Loading…
@robin-aws
2
xlit CLI for easily running lit-style integration tests from the command line 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 priority: not yet Will reconsider working on this when we're looking for work
#2033 opened Apr 19, 2022 by robin-aws
@robin-aws
Uninitialized constants should be rejected by /definiteAssignment:3 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#2729 opened Sep 12, 2022 by robin-aws
@davidcok @robin-aws
Output encoding for Java kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#3344 opened Jan 9, 2023 by fabiomadge
@robin-aws
Name conflict in creating a .doo archive 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
#4068 opened May 23, 2023 by davidcok
@robin-aws
Allow more assumptions when building .doo files kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4517 opened Sep 5, 2023 by robin-aws
@robin-aws
Feature request: support {:termination false} on classes as well as traits kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#4642 opened Oct 11, 2023 by robin-aws
@robin-aws
Standard library: Interop kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution
#4654 opened Oct 11, 2023 by robin-aws
@robin-aws
Python fails to cast Main arguments as strings correctly in --unicode-char:true mode 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 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 priority: next Will consider working on this after in progress work is done
#5184 opened Mar 12, 2024 by robin-aws
@robin-aws
Precondition of merge sort too strong 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: next Will consider working on this after in progress work is done
#5286 opened Apr 1, 2024 by RustanLeino
@robin-aws
Holistic design for Dafny package management kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny status: planned The team is planning to work on this in the near future
#5323 opened Apr 16, 2024 by robin-aws Library support
@robin-aws
rise4fun can't open now,is there any backup link? kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: cleanup Cleanups in the implementation or in corners of the language priority: not yet Will reconsider working on this when we're looking for work
#1344 opened Aug 10, 2021 by Aaron-clou
@robin-aws
1
Compilation error with :extern module and _default class during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#2155 opened May 20, 2022 by cpitclaudel
@robin-aws
1
fix: Include standard header with every unsupported feature message
#2739 opened Sep 13, 2022 by cpitclaudel Loading…
1
@robin-aws
3
Re-add including-doo.dfy test file kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3984 opened May 10, 2023 by robin-aws
@robin-aws
1
Standard library: Actions kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution
#4646 opened Oct 11, 2023 by robin-aws
@robin-aws
1
Include directives can lead to including unverified code in doo files 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 part: tools Tools built on top of Dafny
#4762 opened Nov 9, 2023 by robin-aws
2
@robin-aws
1
Add --include-standard-libraries option to dafny translate 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
#5002 opened Jan 23, 2024 by robin-aws
@robin-aws
1
Support --unicode-char:false with --standard-libraries has-workaround: no There are no known workarounds
#5003 opened Jan 23, 2024 by robin-aws
@robin-aws
1
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
PropagateFailure() and Result vs. Outcome 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
#1893 opened Mar 9, 2022 by robin-aws
@davidcok @robin-aws
2