This Month in Hax: September 2025
In September, we successfully merged 44 pull requests!
After a summer slow down, we focused on improving the new rust-written engine of Hax (that progressively replaces the OCaml one), along with its flagship backend (Lean), while consolidating the documentation and tutorial. We released a new version of hax 🎉
In the rust-engine, a lot of work went into the treatment of identifiers (#1648, #1689, #1693).
We improved the caching (#1701, #1719), and the control over extraction with attributes.
The Lean backend saw a lot of new features: structs, enums, basic support for traits, support for functionalized loops. Along those, we improved the documentation in the tutorial and in the manual. The F*-parity and the official launch of the Lean backend are getting closer!
Stay tuned for more updates next month!
Full list of PRs
- #1719: Improve rustc caching with
cargo-hax - #1718: feat(CONTRIBUTING): document issue prefixes style
- #1701: fix(ci): cache hax entirely on Cachix
- #1695: (Lean Backend) Improve support for functionalized loops
- #1694: Show Lean backend when doing
cargo hax into --help - #1693: Rust Engine: refactor names, change tuples representation
- #1692: Cargo hax: improve error reports
- #1691: Update CHANGELOG.md
- #1690: Website: add tests for dead links and playground integration
- #1689: Rust Engine: add interning table, intern
GlobalIds - #1688: Fix names in Lean tutorial.
- #1687: Docs: fix build
- #1686: Docs: hide RFCs tab and add toolchain structure page.
- #1685: Allow hax_lib::include to override -i flags.
- #1684: Fix libcrux-ref for the merge queue.
- #1683: Update README.md
- #1682: Add documentation for the Lean backend (manual)
- #1681: fix(engine): add rewrite local self as a proper phase
- #1679: (Lean Backend) Add basic support for traits
- #1678: Merge evit Aug 21
- #1676: Temporarily remove ocaml doc build because of odoc issue.
- #1669: feat(rengine): output diagnostics in
todo!s in printers - #1665: Improve readme
- #1662: feat(rengine): add resugaring for tuples
- #1661: CONTRIBUTING.md: change and clarify the meaning of assignee
- #1659: feat(rengine): resugaring: add
FunctionsToConstants - #1655: fix(just): rename
show-jsonintodebug-json: that's the correct name - #1654: feat(engine): import thir: add missing borrows
- #1649: feat(gh actions): job that creates a "this month in hax" skeleton
- #1648: feat(rengine): use
ExplicitDefIdinstead ofDefIdfor names - #1647: Release hax 0.3.4
- #1645: fix(rengine): missed case
Staticin name rendering - #1644: Hax release 0.3.3
- #1643: feat(frontend/hir): add visibility to items
- #1642: feat(blog): this month in hax
- #1640: Rust engine: Optimize communication with hax driver and Ocaml engine.
- #1635: Lean backend - Run rustc coverage tests for lean.
- #1634: chore(deps): bump tracing-subscriber from 0.3.19 to 0.3.20
- #1633: Rust-engine / Lean backend: pass include flag from the ocaml engine to the rust engine.
- #1626: Lean tutorial first version.
- #1623: feat(Lean backend) Add support for enums and structs
- #1591: Lean backend (M2) - 3/3 - Resugarings
- #1564: feat(ci): add an action to ensure changelog updates
- #1559: Merge frontend improvements