9 Pull requests merged by 3 people

• fix: Correct null-related checking of type bounds, and add axioms

  #5738 merged Sep 5, 2024

• fix: Fix various type-system-refresh issues

  #5712 merged Sep 5, 2024

• Fix: Support for enumerating datatypes in the Rust backend

  #5670 merged Sep 5, 2024

• Chore: Use of concurrentbag instead of list for LSP trees

  #5745 merged Sep 5, 2024

• For function postcondition violations, point to the problematic expression branch

  #5681 merged Sep 4, 2024

• Feat rust externs subsets eta names tests

  #5613 merged Sep 4, 2024

• Release 4.8.0

  #5733 merged Sep 3, 2024

• Chore: Ordering of modules now deterministic in compiled code

  #5684 merged Sep 3, 2024

• feat: Prelude extractor

  #5621 merged Aug 30, 2024

3 Pull requests opened by 2 people

• Feat: Add --rust-module-name to specify a module name

  #5747 opened Sep 4, 2024

• Verified java

  #5748 opened Sep 5, 2024

• Chore: Removal of debug line for better mergeability

  #5750 opened Sep 5, 2024

4 Issues closed by 2 people

• Verification fragility on trait extension

  #5719 closed Sep 5, 2024

• Null-related issues with bounded polymorphism

  #5726 closed Sep 5, 2024

• Support for enumerating finite datatypes in Rust

  #5643 closed Sep 5, 2024

• LSP MigrateVerificationTrees is enumerating a collection possibly being modified concurrently

  #5744 closed Sep 5, 2024

8 Issues opened by 6 people

• Matching pattern uses Unbox as outermost expression

  #5751 opened Sep 5, 2024

• Dafny-generated files are not mergeable due to hard-coded line number debugging info

  #5749 opened Sep 5, 2024

• C# backend not handling well module and datatype homonyms

  #5746 opened Sep 4, 2024

• Depending on the assert position, the verifier freezes

  #5743 opened Sep 3, 2024

• Crash when foo() calls Main()

  #5742 opened Sep 2, 2024

• Java doesn't like nested array of chars

  #5741 opened Aug 30, 2024

• [PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny

  #5740 opened Aug 30, 2024

• Dafny IR contains singleton tuples when compiling pair with ghost

  #5739 opened Aug 30, 2024

18 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Fix: Tail-Recursion for the Dafny-to-Rust compiler

  #5668 commented on Sep 5, 2024 • 1 new comment

• fix: Frame and termination checks are now subject to by-proofs of method calls

  #5735 commented on Aug 30, 2024 • 0 new comments

• Feat rust exactboundedpool

  #5706 commented on Sep 4, 2024 • 0 new comments

• Chore: Increase Runtime coverage

  #5694 commented on Sep 5, 2024 • 0 new comments

• Feat: Translate Dafny tests to Rust tests

  #5676 commented on Sep 4, 2024 • 0 new comments

• Fix: Support for double constant initialization in Dafny-to-Rust

  #5667 commented on Sep 5, 2024 • 0 new comments

• Use refresh resolver by default

  #5653 commented on Sep 5, 2024 • 0 new comments

• Dafny fails with most languages when using UTF-16 escape sequences

  #5737 commented on Sep 5, 2024 • 0 new comments

• Dafny-to-Rust code generator

  #5561 commented on Sep 5, 2024 • 0 new comments

• [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library

  #5565 commented on Sep 5, 2024 • 0 new comments

• [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny

  #5486 commented on Sep 5, 2024 • 0 new comments

• [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb

  #5640 commented on Sep 5, 2024 • 0 new comments

• Rust backend needs an option similar to `--go-module-name` or `--python-module-name`

  #5641 commented on Sep 4, 2024 • 0 new comments

• Backend-specific options should be available for all backend-specific CLI commands

  #5707 commented on Sep 3, 2024 • 0 new comments

• Find a way for DafnyWrittenCodeGenerators to report unsupported features from the Dafny side

  #5714 commented on Sep 3, 2024 • 0 new comments

• `expect` statements to print more user-friendly outputs

  #5720 commented on Sep 3, 2024 • 0 new comments

• Busy z3 process leaked

  #5616 commented on Aug 30, 2024 • 0 new comments

• Fragility issue when inherited trait function used in inherited contract

  #5652 commented on Aug 30, 2024 • 0 new comments