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

#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

#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

#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

#5215 - Move the field replacement out of ModuleDefinition, to avoid caching issues

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago - 1 comment

#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

#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

#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

#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

#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

#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 - 2 comments

#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

#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