Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / dafny-lang/dafny issues and pull requests
#5234 - fix: Optimize datatype wrappers only in the absence of trait parents
Pull Request -
State: closed - Opened by RustanLeino 7 months ago
#5234 - fix: Optimize datatype wrappers only in the absence of trait parents
Pull Request -
State: closed - Opened by RustanLeino 7 months ago
#5233 - Datatype erasure and traits don't play together
Issue -
State: closed - Opened by RustanLeino 7 months ago
Labels: kind: bug, part: code-generation
#5232 - Crash on reads with different datatype ordering
Issue -
State: open - Opened by txiang61 7 months ago
- 1 comment
Labels: kind: bug, part: resolver, crash, priority: next, during 1: program development
#5232 - Crash on reads with different datatype ordering
Issue -
State: open - Opened by txiang61 7 months ago
- 1 comment
Labels: kind: bug, part: resolver, crash, priority: next, during 1: program development
#5231 - Various prelude cleanups
Pull Request -
State: open - Opened by atomb 7 months ago
#5230 - Chore: More precise documentation about export set names
Pull Request -
State: closed - Opened by MikaelMayer 7 months ago
#5229 - Flaky tests
Pull Request -
State: open - Opened by keyboardDrummer 7 months ago
#5229 - Add logging related to flaky tests
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5228 - Test `NoExtraThreadAfterEachChange` is unstable
Issue -
State: closed - Opened by keyboardDrummer 7 months ago
- 1 comment
Labels: kind: language development speed
#5228 - Test `NoExtraThreadAfterEachChange` is unstable
Issue -
State: closed - Opened by keyboardDrummer 7 months ago
- 1 comment
Labels: kind: language development speed
#5227 - Let child modules implicitly import their parent, instead of the other way around.
Issue -
State: open - Opened by keyboardDrummer 7 months ago
- 2 comments
Labels: kind: enhancement, part: language definition
#5226 - Hybrid Test Generation
Pull Request -
State: open - Opened by Dargones 7 months ago
- 1 comment
#5225 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 7 months ago
#5225 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: open - Opened by dafny-lang-bot 7 months ago
#5224 - (TEST ISSUE PLEASE IGNORE)
Issue -
State: closed - Opened by robin-aws 7 months ago
Labels: release-blocker, autocut
#5224 - (TEST ISSUE PLEASE IGNORE)
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: release-blocker, autocut
#5223 - (TEST ISSUE PLEASE IGNORE)
Issue -
State: closed - Opened by robin-aws 7 months ago
Labels: release-blocker
#5222 - (TEST ISSUE PLEASE IGNORE)
Issue -
State: closed - Opened by robin-aws 7 months ago
Labels: autocut
#5222 - (TEST ISSUE PLEASE IGNORE)
Issue -
State: closed - Opened by robin-aws 7 months ago
Labels: autocut
#5221 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 7 months ago
Labels: release-blocker, autocut
#5221 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 7 months ago
Labels: release-blocker, autocut
#5220 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 7 months ago
#5220 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 7 months ago
#5219 - set RangeToken for ParensExpression
Pull Request -
State: closed - Opened by arminvakil 7 months ago
#5219 - set RangeToken for ParensExpression
Pull Request -
State: closed - Opened by arminvakil 7 months ago
#5218 - Add progress option
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
- 4 comments
#5217 - Investigate potential bug in the filtering step of Dafny's trigger generation
Issue -
State: open - Opened by keyboardDrummer 7 months ago
Labels: kind: bug, part: verifier
#5216 - Add axiom warnings for functions and methods when using the new resolver
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5215 - Move the field replacement out of ModuleDefinition, to avoid caching issues
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
- 1 comment
#5214 - Do not use DafnyConsolePrinter when using the modular CLI front-end
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5213 - Instability: verification diverges when datatype taken out of module
Issue -
State: open - Opened by erniecohen 7 months ago
Labels: kind: bug, part: verifier, priority: next, during 2: compilation of correct program
#5212 - Add VERSIONING.md
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: kind: enhancement
#5211 - Support for bounded polymorphism / trait bounds
Issue -
State: open - Opened by dschoepe 7 months ago
Labels: kind: enhancement
#5210 - Documentation snapshot for v4.5.0
Pull Request -
State: closed - Opened by alex-chew 7 months ago
#5209 - internal error
Issue -
State: open - Opened by kjx 7 months ago
Labels: kind: bug
#5208 - (TEST ISSUE PLEASE IGNORE) Dafny nightly regression from smithy-lang/smithy-dafny/.github/workflows/manual.yml@refs/heads/robin-aws/cut-dafny-issues-on-nightly-failures
Issue -
State: closed - Opened by robin-aws 7 months ago
Labels: release-blocker
#5207 - Expand standard libraries documentation
Issue -
State: open - Opened by alexporter8013 7 months ago
Labels: part: documentation
#5206 - Facilitate integration of Dafny into larger projects
Issue -
State: open - Opened by alexporter8013 7 months ago
- 4 comments
Labels: kind: enhancement
#5205 - Release Dafny 4.5.0
Pull Request -
State: closed - Opened by alex-chew 7 months ago
#5203 - Rust backend always includes runtime code, doesn't emit it unless building the target program
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: lang: rust
#5202 - Crash related to export sets
Issue -
State: open - Opened by keyboardDrummer 7 months ago
Labels: kind: bug, part: resolver, during 2: compilation of correct program
#5201 - Debugging CI
Pull Request -
State: open - Opened by robin-aws 7 months ago
#5200 - Rust backend broken in master, not detected by CI
Issue -
State: open - Opened by robin-aws 7 months ago
- 1 comment
Labels: kind: bug
#5199 - chore: update version number and doo files for 4.5.0 release
Pull Request -
State: closed - Opened by alex-chew 7 months ago
#5198 - Make it possible to write at least some of Dafny's prelude axioms in Dafny
Issue -
State: open - Opened by atomb 7 months ago
- 1 comment
Labels: kind: enhancement
#5197 - Automate extracting an expression into a separately-defined function
Issue -
State: open - Opened by atomb 7 months ago
- 1 comment
Labels: kind: enhancement
#5196 - Module refinement leads to resolution errors with `--default-function-opacity AutoRevealDependencies`
Issue -
State: open - Opened by atomb 7 months ago
Labels: kind: bug
#5195 - docs: Update book recommendations
Pull Request -
State: open - Opened by fabiomadge 7 months ago
- 3 comments
#5194 - Internal error with datatype traits
Issue -
State: closed - Opened by erniecohen 7 months ago
- 1 comment
Labels: kind: bug
#5193 - Aporter/docs_fixing
Pull Request -
State: closed - Opened by alexporter8013 7 months ago
#5192 - Add `by` blocks to function and method calls
Issue -
State: closed - Opened by atomb 7 months ago
- 20 comments
Labels: kind: enhancement, area: performance, part: language definition, misc: brittleness
#5191 - chore: Update general-traits error message
Pull Request -
State: closed - Opened by RustanLeino 7 months ago
#5190 - Bump Boogie dependency to v3.1.3
Pull Request -
State: open - Opened by atomb 7 months ago
#5190 - Bump Boogie dependency to v3.1.3
Pull Request -
State: closed - Opened by atomb 7 months ago
#5189 - Fix bug that occurred when using resolution caching and replaceable modules
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5189 - Fix bug that occurred when using resolution caching and replaceable modules
Pull Request -
State: open - Opened by keyboardDrummer 7 months ago
#5188 - Always clone modules when retrieving them from the resolution cache
Issue -
State: closed - Opened by keyboardDrummer 7 months ago
Labels: part: language server, kind: language development speed
#5188 - Always clone modules when retrieving them from the resolution cache
Issue -
State: open - Opened by keyboardDrummer 7 months ago
Labels: part: language server, kind: language development speed
#5187 - IDE can't resolve more than once with --standard-libraries
Issue -
State: closed - Opened by robin-aws 7 months ago
- 1 comment
Labels: kind: bug, release-blocker
#5187 - IDE can't resolve more than once with --standard-libraries
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: kind: bug, release-blocker
#5186 - Add `--solver-option-help` flag
Issue -
State: open - Opened by atomb 7 months ago
- 1 comment
Labels: kind: enhancement
#5186 - Add `--solver-option-help` flag
Issue -
State: open - Opened by atomb 7 months ago
Labels: kind: enhancement
#5185 - Add `--attribute-help` flag
Issue -
State: open - Opened by atomb 7 months ago
Labels: kind: enhancement
#5185 - Add `--attribute-help` flag
Issue -
State: open - Opened by atomb 7 months ago
- 1 comment
Labels: kind: enhancement
#5184 - Python fails to cast Main arguments as strings correctly in --unicode-char:true mode
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: kind: bug, part: code-generation, lang: python, priority: next, during 4: bad execution of correct program
#5184 - Python fails to cast Main arguments as strings correctly in --unicode-char:true mode
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: kind: bug, during 4: execution of correct program
#5183 - chore: Remove warning on --type-system-refresh
Pull Request -
State: closed - Opened by robin-aws 7 months ago
#5183 - chore: Remove warning on --type-system-refresh
Pull Request -
State: closed - Opened by robin-aws 7 months ago
#5182 - Document HTML verification coverage reports
Issue -
State: open - Opened by atomb 7 months ago
Labels: part: documentation
#5182 - Document HTML verification coverage reports
Issue -
State: open - Opened by atomb 7 months ago
Labels: part: documentation
#5181 - Put a message in related location messages, even when using snippets
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
- 2 comments
#5180 - Return a failure exit code when there are warnings and they are not a…
Pull Request -
State: open - Opened by keyboardDrummer 7 months ago
#5180 - Return a failure exit code when there are warnings and they are not a…
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5179 - Stop using a cancelled task to present compilation states that could …
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5178 - Do not crash Boogie when an empty {:trigger} attribute occurs
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5178 - Do not crash Boogie when an empty {:trigger} attribute occurs
Pull Request -
State: closed - Opened by keyboardDrummer 7 months ago
#5177 - random seed vs verification coverage report?
Issue -
State: open - Opened by hmijail 7 months ago
- 1 comment
Labels: part: documentation
#5177 - random seed vs verification coverage report?
Issue -
State: open - Opened by hmijail 7 months ago
- 5 comments
Labels: part: documentation
#5176 - Standard Library documentation is broken
Issue -
State: open - Opened by alexporter8013 7 months ago
Labels: part: documentation
#5176 - Standard Library documentation is broken
Issue -
State: closed - Opened by alexporter8013 7 months ago
Labels: part: documentation
#5175 - feat: Add newtype support for map and imap
Pull Request -
State: closed - Opened by RustanLeino 7 months ago
#5174 - high CPU/RAM usage when should be idle
Issue -
State: closed - Opened by hmijail 7 months ago
- 24 comments
Labels: kind: bug, area: performance, part: language server, priority: not yet
#5173 - chore(deps): bump softprops/action-gh-release from 1 to 2
Pull Request -
State: closed - Opened by dependabot[bot] 7 months ago
Labels: dependencies, github_actions
#5172 - `reveal` should warn instead of error on non-opaque argument
Issue -
State: open - Opened by seanmcl 7 months ago
Labels: kind: enhancement, makes-mikael-grateful
#5171 - Peano and single-use integers
Issue -
State: open - Opened by GAJaloyan 7 months ago
- 1 comment
Labels: kind: enhancement
#5171 - Peano and single-use integers
Issue -
State: open - Opened by GAJaloyan 7 months ago
- 6 comments
Labels: kind: enhancement
#5170 - fix: Reject modules that were never verified when building doo files
Pull Request -
State: open - Opened by robin-aws 7 months ago
#5170 - fix: Reject modules that were never verified when building doo files
Pull Request -
State: open - Opened by robin-aws 7 months ago
- 2 comments
#5169 - Feature request: Type by class with private memory
Issue -
State: open - Opened by MikaelMayer 7 months ago
#5169 - Feature request: Type by class with private memory
Issue -
State: open - Opened by MikaelMayer 7 months ago
#5168 - Add syntactic sugar for specifying validity constraints on classes
Issue -
State: closed - Opened by keyboardDrummer 7 months ago
- 4 comments
Labels: kind: enhancement, part: language definition
#5168 - Add syntactic sugar for specifying validity constraints on classes
Issue -
State: closed - Opened by keyboardDrummer 7 months ago
- 3 comments
Labels: kind: enhancement, part: language definition
#5167 - Argument-less argument `:trigger` accepted (even encouraged!) but then crashes
Issue -
State: closed - Opened by RustanLeino 7 months ago
Labels: kind: bug, release-blocker
#5167 - Argument-less argument `:trigger` accepted (even encouraged!) but then crashes
Issue -
State: open - Opened by RustanLeino 7 months ago
Labels: kind: bug
#5166 - Compilation of `:| assume` omitted
Issue -
State: open - Opened by RustanLeino 7 months ago
- 2 comments
Labels: kind: bug, part: code-generation, during 4: execution of correct program
#5166 - Compilation of `:| assume` omitted
Issue -
State: open - Opened by RustanLeino 7 months ago
- 2 comments
Labels: kind: bug, part: code-generation, priority: next, during 4: bad execution of correct program
#5165 - Single expression for combined is and as
Issue -
State: open - Opened by robin-aws 7 months ago
- 5 comments
Labels: kind: enhancement
#5165 - Single expression for combined is and as
Issue -
State: open - Opened by robin-aws 7 months ago
- 5 comments
Labels: kind: enhancement
#5164 - Remove experimental warning on `--type-system-refresh`
Issue -
State: open - Opened by robin-aws 7 months ago
Labels: kind: enhancement, release-blocker