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

#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

#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

#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

#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

#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

#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

#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

#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