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
#5577 - Ensure the presence of a `by {...}` block does not affect the SMT of the surrounding proofs
Issue -
State: open - Opened by keyboardDrummer 5 days ago
Labels: kind: enhancement, part: verifier, misc: brittleness
#5576 - Add `--isolate-paths` option
Issue -
State: open - Opened by keyboardDrummer 5 days ago
Labels: kind: enhancement, part: verifier, misc: brittleness
#5575 - Enable hiding of functions to an extend that it could make opaque obsolete
Issue -
State: open - Opened by keyboardDrummer 6 days ago
- 1 comment
#5574 - Fix: Compiled disjunctive nested pattern matching no longer crashing
Pull Request -
State: closed - Opened by MikaelMayer 6 days ago
- 1 comment
#5573 - Chore: Internal backends should not fail CI
Pull Request -
State: closed - Opened by MikaelMayer 6 days ago
#5572 - Disjunctive pattern matching not correctly handled
Issue -
State: closed - Opened by MikaelMayer 6 days ago
Labels: kind: bug, during 4: bad execution of correct program
#5571 - Attempt to stabilize ConcurrentCompilationDoesNotBreakCaching test
Pull Request -
State: closed - Opened by keyboardDrummer 6 days ago
#5570 - Malformed Boogie for if-then-else with non-reference traits
Issue -
State: open - Opened by RustanLeino 7 days ago
Labels: kind: bug
#5569 - Ordering problem in Python code generator
Issue -
State: open - Opened by RustanLeino 7 days ago
Labels: kind: bug, part: code-generation, lang: python
#5568 - Add --find-project option
Pull Request -
State: closed - Opened by keyboardDrummer 7 days ago
#5567 - Integrate MIRI as part of the CI to ensure no memory leak in the DafnyRuntimeRust
Issue -
State: open - Opened by MikaelMayer 10 days ago
#5566 - ci: Fix nightly build tests broken by skipping Rust
Pull Request -
State: closed - Opened by robin-aws 12 days ago
Labels: run-deep-tests
#5565 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
Issue -
State: open - Opened by aws-crypto-tools-ci-bot 13 days ago
- 8 comments
#5564 - Ensure nightly skips Rust (fixed)
Pull Request -
State: closed - Opened by MikaelMayer 14 days ago
Labels: run-deep-tests
#5562 - Blind callables
Pull Request -
State: open - Opened by keyboardDrummer 16 days ago
#5561 - Dafny-to-Rust code generator
Issue -
State: open - Opened by MikaelMayer 17 days ago
Labels: part: code-generation, priority: now
#5560 - Make the Rust compiler run on nightly once it passes all tests
Issue -
State: open - Opened by MikaelMayer 17 days ago
Labels: part: code-generation, priority: now, part: ci
#5559 - Chore: Omit Rust from the nightly release workflow
Pull Request -
State: closed - Opened by MikaelMayer 17 days ago
- 1 comment
#5558 - fix: Legacy datatype constructor compatibility in Java
Pull Request -
State: closed - Opened by robin-aws 18 days ago
#5557 - C# and Go Backends: Incorrect finite map semantics
Issue -
State: open - Opened by khemichew 19 days ago
- 1 comment
Labels: kind: bug, lang: golang, lang: js, priority: not yet, during 3: execution of incorrect program
#5556 - Potential enhancement: array initialisation that is incompatible with declared size
Issue -
State: open - Opened by khemichew 19 days ago
Labels: kind: bug, kind: enhancement, priority: not yet, during 3: execution of incorrect program
#5555 - Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions
Issue -
State: open - Opened by robin-aws 19 days ago
- 4 comments
Labels: kind: bug, release-blocker, priority: now
#5554 - C# backend: Multiset size overflow
Issue -
State: open - Opened by khemichew 19 days ago
Labels: kind: bug, lang: c#, priority: not yet, during 4: bad execution of correct program
#5553 - Helpers.unsignedLongToBigInteger removed from Java runtime
Issue -
State: closed - Opened by robin-aws 19 days ago
Labels: release-blocker
#5552 - JavaScript and Go backend: Incorrect map cardinality
Issue -
State: open - Opened by khemichew 19 days ago
- 1 comment
Labels: kind: bug, part: code-generation, lang: golang, lang: js, priority: not yet
#5551 - Flaky test: Unspecified
Issue -
State: open - Opened by MikaelMayer 20 days ago
Labels: kind: language development speed, priority: not yet, part: ci
#5550 - Flaky test Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.ProjectManagerDatabaseTest.ChangeAndUndoProjectWithMultipleFile
Issue -
State: closed - Opened by MikaelMayer 21 days ago
- 1 comment
Labels: kind: language development speed
#5549 - Flaky test: DafnyTestGeneration
Issue -
State: closed - Opened by MikaelMayer 21 days ago
- 3 comments
Labels: kind: language development speed
#5548 - Fix null ref in covered tokens
Pull Request -
State: closed - Opened by keyboardDrummer 21 days ago
#5547 - feat: Add bounded polymorphism
Pull Request -
State: open - Opened by RustanLeino 23 days ago
- 6 comments
#5546 - Implement `GetAssertedExpr` for `CalculationStep`
Pull Request -
State: closed - Opened by atomb 24 days ago
#5545 - Fix bug in projectAsLibrary test
Pull Request -
State: closed - Opened by keyboardDrummer 24 days ago
- 1 comment
#5544 - Named ensure clause
Issue -
State: open - Opened by keyboardDrummer 24 days ago
Labels: kind: enhancement, part: language definition, priority: not yet
#5543 - Prevent LSP server from crashing on code actions
Pull Request -
State: closed - Opened by keyboardDrummer 24 days ago
#5542 - feat: Implement frame-related asserted exprs and TraitDecreases
Pull Request -
State: closed - Opened by alex-chew 24 days ago
#5541 - textDocument/codeAction failed
Issue -
State: closed - Opened by keyboardDrummer 24 days ago
Labels: part: language server, during 1: program development
#5540 - can't label assumptions
Issue -
State: open - Opened by kjx 24 days ago
Labels: kind: enhancement, part: language definition, priority: not yet
#5539 - can't label forall-ensuring statement
Issue -
State: open - Opened by kjx 24 days ago
Labels: kind: enhancement, part: language definition, priority: not yet
#5538 - Reverted internal prefix for every backend except Dafny
Pull Request -
State: closed - Opened by MikaelMayer 25 days ago
- 1 comment
#5537 - Unstable CLI test `git-issues/git-issue-697j.dfy`, related to Rust backend
Issue -
State: open - Opened by keyboardDrummer 25 days ago
- 5 comments
Labels: kind: language development speed, priority: not yet, part: ci
#5536 - Costless by clause in `assert .. by { }` when using --isolate-assertions
Issue -
State: open - Opened by keyboardDrummer 25 days ago
- 3 comments
Labels: kind: enhancement, part: boogie, priority: not yet
#5535 - Use Macos13 instead of 14
Pull Request -
State: closed - Opened by keyboardDrummer 25 days ago
Labels: run-deep-tests
#5534 - Verification hang apparently caused by Std import
Issue -
State: open - Opened by nverhaaren 25 days ago
- 3 comments
Labels: kind: bug, priority: not yet, part: standard libraries, during 2: compilation of correct program
#5533 - Issue with multi-backend-testing
Issue -
State: open - Opened by MikaelMayer 26 days ago
Labels: kind: language development speed, priority: not yet
#5532 - Bad encoding for `this` in tail recursive functions when compiling to Java
Issue -
State: open - Opened by fabiomadge 26 days ago
- 1 comment
Labels: kind: bug, lang: java, priority: not yet, during 2: compilation of correct program
#5531 - ci: Align mostly on macos-11
Pull Request -
State: closed - Opened by robin-aws 26 days ago
- 1 comment
Labels: run-deep-tests
#5530 - Flaky CI cancelled before completing
Issue -
State: closed - Opened by MikaelMayer 26 days ago
- 1 comment
#5529 - chore: Remove typos in docs
Pull Request -
State: closed - Opened by fabiomadge 26 days ago
#5528 - No flatten for most backends
Pull Request -
State: closed - Opened by keyboardDrummer 26 days ago
- 2 comments
#5527 - assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion)
Issue -
State: open - Opened by kjx 27 days ago
- 2 comments
Labels: kind: enhancement, part: verifier, incompleteness, priority: not yet
#5526 - Split off parts of single pass compiler
Pull Request -
State: closed - Opened by keyboardDrummer 27 days ago
#5525 - Verification ignores resource limits
Issue -
State: open - Opened by hmijail 27 days ago
- 6 comments
Labels: kind: bug, part: z3, priority: not yet
#5524 - fix: Only guard `this` when eliminating tail calls, if possible
Pull Request -
State: closed - Opened by fabiomadge 27 days ago
#5523 - Error when guarding nonexistent `this`
Issue -
State: closed - Opened by fabiomadge 27 days ago
Labels: kind: bug, lang: c#, release-blocker, during 2: compilation of correct program
#5522 - Add `const`, `export` and `expect` to LaTeX keyword list
Pull Request -
State: closed - Opened by zeertzjq 27 days ago
#5521 - Constraint-less newtypes assumed to be nonempty
Issue -
State: open - Opened by RustanLeino 28 days ago
Labels: kind: bug, during 3: execution of incorrect program
#5519 - chore: Clean up build
Pull Request -
State: closed - Opened by RustanLeino 28 days ago
#5517 - Use a separate dotnet process for compiling C# programs
Pull Request -
State: open - Opened by keyboardDrummer 28 days ago
Labels: run-deep-tests
#5515 - Flaky test: ConcurrentCompilationDoesNotBreakCaching
Issue -
State: closed - Opened by MikaelMayer about 1 month ago
- 3 comments
Labels: kind: language development speed, priority: next
#5514 - Fix minor README typo
Pull Request -
State: closed - Opened by lucasmcdonald3 about 1 month ago
#5513 - Chore: Dafny to Rust refactorings
Pull Request -
State: closed - Opened by MikaelMayer about 1 month ago
Labels: run-integration-tests
#5512 - Add timeout support to tests of TestGeneration.Test
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
- 1 comment
#5511 - Chore: Using instantiated type for coercion
Pull Request -
State: closed - Opened by MikaelMayer about 1 month ago
Labels: run-integration-tests
#5510 - Unstable test ChangeAndUndoProjectWithMultipleFiles
Issue -
State: open - Opened by keyboardDrummer about 1 month ago
- 3 comments
Labels: kind: language development speed, priority: next
#5509 - Do not flatten matches for C#
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
- 1 comment
Labels: run-integration-tests
#5508 - Include stacktrace in parser internal error message
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
#5507 - chore: remove byte-order mark from test files
Pull Request -
State: closed - Opened by alex-chew about 1 month ago
- 1 comment
#5506 - Chore: No extra newtype test
Pull Request -
State: closed - Opened by MikaelMayer about 1 month ago
- 1 comment
#5505 - Confusing type error due to missing path qualifier
Issue -
State: open - Opened by mschlaipfer about 1 month ago
Labels: kind: bug
#5504 - Update testing documentation
Pull Request -
State: closed - Opened by stefan-aws about 1 month ago
#5503 - Revert "ci: Use macos-11 in all CI (#5493)"
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
Labels: run-deep-tests
#5502 - Only let DafnyCore reference the LSP protocol
Pull Request -
State: open - Opened by keyboardDrummer about 1 month ago
#5501 - feat: Implement assigned(e) expression
Pull Request -
State: closed - Opened by alex-chew about 1 month ago
#5500 - ci: Migrate off macos-11
Pull Request -
State: open - Opened by robin-aws about 1 month ago
Labels: run-deep-tests
#5499 - Integration tests getting really slow
Issue -
State: open - Opened by robin-aws about 1 month ago
Labels: kind: language development speed
#5498 - fix: Disambiguation priority not preserved when importing modules
Pull Request -
State: open - Opened by stefan-aws about 1 month ago
#5497 - fix: Ignore values not in a multiset when computing its hash in C#
Pull Request -
State: open - Opened by fabiomadge about 1 month ago
Labels: run-deep-tests
#5496 - Catch crash on reads with different datatype ordering
Pull Request -
State: open - Opened by stefan-aws about 1 month ago
#5495 - feat: Allow type parameters on newtypes
Pull Request -
State: open - Opened by RustanLeino about 1 month ago
#5494 - Assign-such-that documentation
Pull Request -
State: open - Opened by stefan-aws about 1 month ago
#5493 - ci: Use macos-11 in all CI
Pull Request -
State: closed - Opened by robin-aws about 1 month ago
Labels: run-deep-tests
#5492 - Revert "fix: Ignore values not in a multiset when computing its hash …
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
- 1 comment
Labels: run-deep-tests
#5491 - Do not emit incorrect linting warnings
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
#5490 - Incorrect multiplication in Dafny: Show Counterexample
Issue -
State: open - Opened by cdstanford about 1 month ago
- 4 comments
Labels: kind: bug, incompleteness, part: counterexamples
#5489 - Implement `GetAssertedExpr` for `DecreasesBoundedBelow`
Pull Request -
State: closed - Opened by atomb about 1 month ago
#5488 - Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long
Issue -
State: open - Opened by keyboardDrummer about 1 month ago
- 9 comments
Labels: kind: language development speed, priority: next
#5486 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
Issue -
State: open - Opened by aws-crypto-tools-ci-bot about 1 month ago
- 37 comments
Labels: breaking-change
#5485 - [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny
Issue -
State: closed - Opened by dafny-lang-bot about 1 month ago
- 14 comments
Labels: breaking-change
#5484 - No longer show generated symbols as workspace symbols
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
#5483 - Improve code navigation for unreferenced declaration
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
#5482 - No memory leaks boogie
Pull Request -
State: closed - Opened by keyboardDrummer about 1 month ago
#5481 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
Issue -
State: closed - Opened by fabiomadge about 1 month ago
- 2 comments
#5480 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
Issue -
State: closed - Opened by aws-crypto-tools-ci-bot about 1 month ago
#5479 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
Issue -
State: closed - Opened by aws-crypto-tools-ci-bot about 1 month ago
- 1 comment
#5478 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny
Issue -
State: closed - Opened by aws-crypto-tools-ci-bot about 1 month ago
#5477 - New Failure
Issue -
State: closed - Opened by fabiomadge about 1 month ago
#5476 - fix: Apply name mangling to datatype names in Python more often
Pull Request -
State: closed - Opened by fabiomadge about 1 month ago
#5475 - Omit empty modules from translation records
Pull Request -
State: closed - Opened by robin-aws about 1 month ago
#5474 - fix: Reference the correct `this` after removing the tail call of a function or method
Pull Request -
State: closed - Opened by fabiomadge about 1 month ago
- 1 comment
#5473 - [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library
Issue -
State: closed - Opened by aws-crypto-tools-ci-bot about 1 month ago
- 18 comments
Labels: breaking-change