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
#5347 - Fix: Standard libraries to be compatible with general newtypes
Pull Request -
State: open - Opened by MikaelMayer 2 months ago
- 1 comment
#5347 - Fix: Standard libraries compatibility with general newtypes
Pull Request -
State: closed - Opened by MikaelMayer 2 months ago
- 1 comment
#5346 - feat: Translation records
Pull Request -
State: open - Opened by robin-aws 2 months ago
- 1 comment
#5346 - feat: Translation records
Pull Request -
State: closed - Opened by robin-aws 2 months ago
- 2 comments
#5345 - Standard libraries not working with general-newtypes=true
Issue -
State: closed - Opened by MikaelMayer 2 months ago
- 1 comment
Labels: kind: bug, priority: now, during 2: compilation of correct program
#5337 - Enable reusing the specification of options in a dfyconfig.toml
Issue -
State: closed - Opened by keyboardDrummer 3 months ago
- 2 comments
Labels: kind: enhancement, area: build-system
#5335 - Enable safely using doo files that were verified against other doo files
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 4 comments
Labels: kind: bug, priority: not yet, during 3: execution of incorrect program
#5333 - Test ResolutionErrors[45679] with new resolver
Pull Request -
State: closed - Opened by RustanLeino 3 months ago
#5333 - Test ResolutionErrors[45679] with new resolver
Pull Request -
State: closed - Opened by RustanLeino 3 months ago
#5331 - Internal Error: System.NullReferenceException
Issue -
State: closed - Opened by erniecohen 3 months ago
- 1 comment
Labels: kind: bug, part: resolver, crash, priority: next, during 2: compilation of correct program
#5329 - Do not refer to auditor code when building a Dafny library
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5329 - Do not refer to auditor code when building a Dafny library
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5327 - [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 3 months ago
- 2 comments
Labels: release-blocker
#5327 - [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 3 months ago
- 2 comments
Labels: release-blocker
#5321 - Unstable test due to timeout when executing Rust back-end
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: kind: language development speed, priority: next
#5319 - Unstable test 'VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: kind: language development speed, priority: next
#5318 - Add retries to NoExtraThreadAfterEachChange
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
- 1 comment
#5317 - Add first pass of proof obligation description expressions
Pull Request -
State: closed - Opened by alex-chew 3 months ago
#5316 - When running many iterations, they get progressively slower until one gets stuck
Issue -
State: open - Opened by hmijail 3 months ago
- 5 comments
Labels: kind: bug
#5315 - [WIP] Refactoring to support `decreases to`
Pull Request -
State: open - Opened by atomb 3 months ago
#5314 - Exception in TestNotificationReceiver due to race condition
Issue -
State: closed - Opened by keyboardDrummer 3 months ago
Labels: kind: language development speed
#5313 - Warn when using non doo file as a library
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5312 - Update Z3 to 4.12.6
Pull Request -
State: open - Opened by atomb 3 months ago
#5311 - Support members for the new newtypes
Pull Request -
State: open - Opened by RustanLeino 3 months ago
#5310 - Resolve concurrency bug in TestNotificationReceiver, improving test stability
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
- 2 comments
#5309 - Unstable test EditWhenUsingStandardLibrary
Issue -
State: closed - Opened by keyboardDrummer 3 months ago
Labels: kind: language development speed
#5308 - Remove branches part from merge_group GH actions configuration
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5307 - Fix incorrect missing {:axiom} warning message
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5306 - Opaque constant gives an incorrect missing {:axiom} warning
Issue -
State: closed - Opened by keyboardDrummer 3 months ago
Labels: kind: bug, part: verifier
#5305 - feat: Call graph specs
Pull Request -
State: open - Opened by fabiomadge 3 months ago
#5304 - Unstable test QuickEditsInLargeFile
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: kind: language development speed, priority: next
#5303 - Rename the hidden option --show-inference to --show-hints
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5302 - Deprecate unicode-char
Pull Request -
State: open - Opened by keyboardDrummer 3 months ago
- 4 comments
#5301 - Rename --coverage-report to --expected-coverage-report
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5300 - Update tests that use --progress, so they are stable
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
- 1 comment
#5299 - Resolve a concurrency bug that could cause the IDE server not to send updates for a particular version
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5298 - Bitvectors using too much time/resources
Issue -
State: open - Opened by seanmcl 3 months ago
Labels: kind: bug
#5297 - Allow using project files together with --library
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5296 - Refactor reading doo manifest from Backend to AST
Issue -
State: open - Opened by ShubhamChaturvedi7 3 months ago
Labels: kind: enhancement, kind: language development speed
#5295 - Error: Dafny encountered an internal error while waiting for this symbol to verify.
Issue -
State: open - Opened by benreynwar 3 months ago
- 3 comments
Labels: kind: bug, part: boogie, during 1: program development
#5294 - [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
Issue -
State: open - Opened by dafny-lang-bot 3 months ago
#5293 - [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot 3 months ago
#5292 - Unstable VerificationErrorDetectedAfterCanceledSave
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: kind: language development speed, priority: next
#5291 - Unstable ChangedImportAffectsExport and ProjectFileDoesNotOwnAllSourceFilesItUses
Issue -
State: closed - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: kind: language development speed
#5290 - Chore: Move tests in the correct directory
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
#5289 - Fix oopsie in TestNotificationReceiver
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5288 - feat: Extended call graph
Pull Request -
State: open - Opened by fabiomadge 3 months ago
#5287 - fix: Invalid Python code for nested set and map comprehensions
Pull Request -
State: closed - Opened by fabiomadge 3 months ago
#5286 - Precondition of merge sort too strong
Issue -
State: open - Opened by RustanLeino 3 months ago
Labels: kind: bug, part: standard libraries
#5285 - [Python] Nested set comprehension results in invalid generated code
Issue -
State: closed - Opened by lucasmcdonald3 3 months ago
Labels: kind: bug, lang: python, during 4: execution of correct program
#5284 - PR for debugging tests, do not merge
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5283 - Reserved keywords in Go in need of escape
Issue -
State: closed - Opened by MikaelMayer 3 months ago
Labels: kind: bug, part: code-generation, lang: golang, priority: next, during 2: compilation of correct program
#5283 - Reserved keywords in Go in need of escape
Issue -
State: open - Opened by MikaelMayer 3 months ago
Labels: kind: bug
#5282 - Provide more information when waiting for notification times out
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5282 - Provide more information when waiting for notification times out
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5281 - Out of resources error reporting
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5280 - chore(deps): bump actions/configure-pages from 4 to 5
Pull Request -
State: closed - Opened by dependabot[bot] 3 months ago
Labels: dependencies, github_actions
#5279 - Verification of adding elements of a sequence to a multiset fails if the sequence is not converted from an array
Issue -
State: closed - Opened by zeertzjq 3 months ago
- 3 comments
Labels: kind: bug
#5278 - Check datatype constructors for bad type-parameter instantiations
Pull Request -
State: closed - Opened by RustanLeino 3 months ago
#5277 - Chore: Work to enable merge queues
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
#5276 - Fix 2026 test
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
Labels: run-deep-tests
#5275 - Fix deep tests path missing
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
Labels: run-deep-tests
#5274 - Missing type-characteristic checks
Issue -
State: closed - Opened by RustanLeino 3 months ago
Labels: kind: bug, part: resolver, during 3: execution of incorrect program
#5273 - chore: add config for PyPI runtime publishing
Pull Request -
State: open - Opened by alex-chew 3 months ago
#5272 - Using `--default-function-opacity=AutoRevealDependencies` can perform badly
Issue -
State: open - Opened by atomb 3 months ago
Labels: kind: bug
#5271 - Chore: Fixed broken URL
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
#5270 - Documentation snapshot for v4.6.0
Pull Request -
State: open - Opened by robin-aws 3 months ago
#5269 - Documentation snapshot for v4.6.0
Pull Request -
State: closed - Opened by robin-aws 3 months ago
#5268 - Release 4.6.0
Pull Request -
State: closed - Opened by robin-aws 3 months ago
#5266 - Remove paths in test that were causing the Windows build to fail
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
- 1 comment
Labels: run-deep-tests
#5265 - Fix: Enhanced "insufficient reads clause to read field"
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
- 1 comment
#5264 - Make `--filter-*` work with `measure-complexity`
Pull Request -
State: open - Opened by atomb 3 months ago
#5263 - chore: Prep for 4.6.0
Pull Request -
State: closed - Opened by robin-aws 3 months ago
#5262 - Unhelpful error message about reads clause
Issue -
State: closed - Opened by MikaelMayer 3 months ago
Labels: kind: enhancement, part: documentation
#5261 - Use proof dependencies for more thorough brittleness reduction warnings
Issue -
State: open - Opened by atomb 3 months ago
- 6 comments
Labels: kind: enhancement
#5260 - Chore: Explain difference between bounds and indices in the documentation
Pull Request -
State: closed - Opened by MikaelMayer 3 months ago
#5259 - Suggest changes that could reduce brittleness
Issue -
State: open - Opened by atomb 3 months ago
- 1 comment
Labels: kind: enhancement
#5258 - Array initialization as powerful as constructors
Issue -
State: open - Opened by MikaelMayer 3 months ago
- 1 comment
Labels: kind: enhancement
#5257 - Free statements with ownership tracking
Issue -
State: open - Opened by MikaelMayer 3 months ago
Labels: kind: enhancement
#5256 - Resolution slowdown
Issue -
State: open - Opened by MikaelMayer 3 months ago
Labels: kind: bug
#5256 - Resolution slowdown
Issue -
State: open - Opened by MikaelMayer 3 months ago
- 1 comment
Labels: kind: bug
#5255 - Move cli tests to new cli
Pull Request -
State: open - Opened by keyboardDrummer 3 months ago
#5255 - Migrate almost all CLI tests to use the command based CLI
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5254 - Give `--resource-limit` a default value
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 3 comments
Labels: kind: enhancement
#5254 - Give `--resource-limit` a default value
Issue -
State: open - Opened by keyboardDrummer 3 months ago
- 2 comments
Labels: kind: enhancement
#5253 - Warn about potential brittleness due to use of difficult constructs
Issue -
State: open - Opened by atomb 3 months ago
- 1 comment
Labels: kind: enhancement
#5253 - Warn about potential brittleness due to use of difficult constructs
Issue -
State: open - Opened by atomb 3 months ago
- 5 comments
Labels: kind: enhancement
#5252 - Allow termination ordering to be written in expressions
Issue -
State: closed - Opened by atomb 3 months ago
Labels: kind: enhancement
#5252 - Allow termination ordering to be written in expressions
Issue -
State: closed - Opened by atomb 3 months ago
Labels: kind: enhancement
#5251 - Add predicate for definite assignment
Issue -
State: closed - Opened by atomb 3 months ago
Labels: kind: enhancement
#5251 - Add predicate for definite assignment
Issue -
State: closed - Opened by atomb 3 months ago
Labels: kind: enhancement
#5250 - Dafny Encounters internal translation error for nested quantifier expressions when a subtitute is required
Issue -
State: open - Opened by arminvakil 3 months ago
Labels: kind: bug, part: verifier, during 2: compilation of correct program
#5249 - Add deprecation warning for old CLI
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5248 - Fix a soundness issue that could be triggered by calling ensures fres…
Pull Request -
State: open - Opened by keyboardDrummer 3 months ago
#5248 - Fix a soundness issue that could be triggered by calling ensures fres…
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
- 2 comments
#5247 - Isolate assertions attribute
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
#5246 - More phase usage
Pull Request -
State: open - Opened by keyboardDrummer 3 months ago
- 2 comments
#5245 - predicate subtypes of functions not propagating predicates
Issue -
State: open - Opened by erniecohen 3 months ago
- 3 comments
Labels: incompleteness, has-workaround: yes
#5244 - Incorrectly inferring type as nullable
Issue -
State: open - Opened by txiang61 3 months ago
- 1 comment
Labels: kind: bug, priority: now, during 2: compilation of correct program
#5243 - Introduce generic mechanism for combining state from multiple compilations
Pull Request -
State: closed - Opened by keyboardDrummer 3 months ago
Labels: makes-mikael-grateful