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

#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

#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

#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

#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

#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

#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

#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: 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