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
35 Open 12 Closed
35 Open 12 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

seq() should allow constrained integer types area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#6100 opened Feb 10, 2025 by ajewellamz
When specifying a Dafny project as a dependency, let Dafny used cached builds of that library when they're available area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#6013 opened Jan 2, 2025 by keyboardDrummer
forall comprehension over bounded newtype area: performance Performance issues kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#5897 opened Nov 4, 2024 by seebees
Compiled code has useless duplicate membership test area: performance Performance issues 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
#5465 opened May 20, 2024 by MikaelMayer
Bitvectors using too much time/resources area: performance Performance issues 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 part: verifier Translation from Dafny to Boogie (translator)
#5298 opened Apr 4, 2024 by seanmcl
3
Large Performance Regressions with Dafny 4.4.0? area: performance Performance issues part: boogie Happens after passing the program to Boogie part: verifier Translation from Dafny to Boogie (translator)
#4898 opened Dec 18, 2023 by DavePearce
6
[Python] function method externs are generated with odd syntax area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: python Dafny's Python transpiler and its runtime
#4853 opened Dec 7, 2023 by lucasmcdonald3
1
Base64.Decode has quadratic runtime on Go area: performance Performance issues lang: golang Dafny's transpiler to Go and its runtime part: standard libraries Standard libraries packaged in the Dafny distribution
#4794 opened Nov 16, 2023 by robin-aws
Verifying many file area: performance Performance issues 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
#4659 opened Oct 13, 2023 by seebees
1
Dafny generates double returns area: performance Performance issues 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 lang: java Dafny's Java transpiler and its runtime lang: python Dafny's Python transpiler and its runtime
#4520 opened Sep 6, 2023 by TheGrandmother
2
Prevent unnecessary diagnostics from being sent to the IDE client area: performance Performance issues part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#4377 opened Aug 3, 2023 by keyboardDrummer
Quantifying over map.Keys has quadratic runtime in Java area: performance Performance issues 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 priority: next Will consider working on this after in progress work is done
#4010 opened May 15, 2023 by robin-aws
@stefan-aws
3
Establishing witnesses for trivial predicates takes RU area: performance Performance issues
#3772 opened Mar 21, 2023 by stefan-aws
Investigate best setting for Z3 parameter smt.qi.eager_threshold area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: z3 Issue is in Z3
#3558 opened Feb 16, 2023 by atomb
1
Only use Boogie projects that are relevant for Dafny area: performance Performance issues 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 part: verifier Translation from Dafny to Boogie (translator)
#3029 opened Nov 9, 2022 by keyboardDrummer
Do not re-resolve previously resolved modules area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#3028 opened Nov 9, 2022 by keyboardDrummer
Z3 version control by attribute area: performance Performance issues 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: z3 Issue is in Z3
#2730 opened Sep 12, 2022 by seebees
3
Lit marker blocks computation on bitvectors area: performance Performance issues incompleteness Things that Dafny should be able to prove, but can't status: needs-expert Needs review by an expert on this part of the code
#2592 opened Aug 15, 2022 by cpitclaudel
Missing Lit marker on cast to bitvector area: performance Performance issues has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#2587 opened Aug 12, 2022 by cpitclaudel
Inefficient encoding of matches in Boogie area: performance Performance issues part: verifier Translation from Dafny to Boogie (translator)
#2554 opened Aug 5, 2022 by sonmarcho
@keyboardDrummer
Cache Boogie translation and preprocessing at the Dafny module level area: performance Performance issues 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 part: verifier Translation from Dafny to Boogie (translator) status: needs-approval Issue that needs approval from Dafny team members before moving to designed
#2361 opened Jul 5, 2022 by keyboardDrummer IDE performance scales to large projects
Investigate and fix low-level performance issues in Dafny area: performance Performance issues 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 part: verifier Translation from Dafny to Boogie (translator) status: needs-decision The cause of this issue is clear; the team needs to decide whether we want to work on it
#2358 opened Jul 4, 2022 by cpitclaudel
4
Proposal: improve performance of sequences 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
1
2
Task: Investigate memoization issues in computation on literals area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator) status: needs-expert Needs review by an expert on this part of the code
#2218 opened Jun 7, 2022 by cpitclaudel
Equality transitivity not useful in the presence of compound bit-vector expressions area: performance Performance issues difficulty: medium Issues that should take a few days to a week to fix part: verifier Translation from Dafny to Boogie (translator) status: needs-expert Needs review by an expert on this part of the code
#2199 opened Jun 2, 2022 by yongweiy
@atomb
ProTip! Type g i on any issue or pull request to go back to the issue listing page.