Merge pull request #1491 from cryspen/this-month-in-hax-05-25

This month in hax May 2025.

Author: maximebuyse

docs/blog/posts/this-month-in-hax/2025-05.md

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