This Month in Hax: May 2025
In May, we successfully merged 19 pull requests!
@Nadrieril helped making the frontend more robust and complete with work on impl exprs (#1431), MIR extraction (#1444, #1457) and FnOnce (#1477).
@W95Psp worked on hax-lib with improved support for writing F* lemmas in Rust (#1456).
@cmester0 improved the Coq and SSProve backends (#1426 and #1108)
Apart from that, we contributed multiple F* core library additions.
Stay tuned for more updates next month!
Full list of PRs
- #1481: Update owners metadata
- #1477: Provide the
FnOnceshim for closures - #1476: Release 0.3.1
- #1473: fix(proof-libs) Remove fields that shouldn't be in PartialOrd.
- #1471: fix(engine) Add InlineConst in concrete_idents.
- #1465: Release 0.3.0
- #1458: feat(proof-libs): add
rem_euclidfor every int types - #1457: Simplify MIR place translation
- #1456: Fix unused in lemmas
- #1455: feat(proof-libs): F*: implement some wrapping operations on i64
- #1454: fix(engine/nix): pin ocamlgraph, waiting for https://github.com/NixOS/nixpkgs/pull/397883
- #1451: fix(engine): naming: items under closures
- #1445: Add interfaces to fstar core and rust_primitives
- #1444: Add missing unwind information in MIR
- #1439: Upstream evit changes up to Feb 21
- #1438: This month in hax April 2025.
- #1431: Consistently translate impl exprs for parent items
- #1426: Bertie ssprove
- #1108: Coq small fixes