This Month in Hax: August 2025
In August, we successfully merged 17 pull requests!
This month, we continued the effort of building out the new hax engine in Rust, with a focus on creating a robust infrastructure for backend development. We introduced a generic Backend trait and a new printing infrastructure, which will simplify the process of creating new backends. We also improved how global identifiers are handled and added visitors.
Building on this new infrastructure, the Lean backend saw significant progress. This month, we merged the first Lean proofs and a set of Lean examples. The Lean printer was also updated to leverage the latest improvements in the Rust engine.
Stay tuned for more updates next month!
Full list of PRs
- #1624: Rust Engine: global identifiers: add view and rendering
- #1613: ci(rengine): clippy: deny lints
- #1612: misc(rengine): stop pinning
derive-generic-visitorwith a git branch - #1609: feat(nix/ci): run examples outside of the sandbox
- #1608: Rust Engine: improve debug utility
show-json - #1607: Update Lean printer to new infrastructure
- #1605: rename explicit_panic
- #1603: Rust Engine: add a
Backendtrait - #1600: Rust Engine: print infrastructure
- #1597: Fixes this month in hax
- #1596: This month in hax July 2025.
- #1594: Update publications.md
- #1593: Lean backend [M2] - 2/3 - Examples
- #1592: Upstream changes from evit up to June 11th 2025.
- #1590: Lean backend [M2] - 1/3 - First proofs
- #1588: fix(engine) Export traits defined in bundles.
- #1585: Visitors using
derive-generic-visitor