diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md new file mode 100644 index 0000000..e85fe63 --- /dev/null +++ b/content/posts/this-month-in-hax/2024-07.md @@ -0,0 +1,69 @@ +--- +author: "Lucas Franceschino" +title: "This month in hax: July 2024" +date: "2024-08-12" +tags: ["this-month-in-hax"] +ShowToc: false +ShowBreadCrumbs: false +--- + +In July, we merged 32 PRs! 🎉 + +On the side of the frontend and CLI, we had a lot of fixes and +improvements! The `hax` command line and rustc driver were +[refactored](https://github.com/hacspec/hax/pull/743), allowing for +better scaling and caching. We also improved the general ergonomics: +diagnostics can [now](https://github.com/hacspec/hax/pull/802) be +output in JSON, we have [improved error +messages](https://github.com/hacspec/hax/pull/796)... And we pushed +various bug fixes. + +In the engine, we now [resugar +asserts](https://github.com/hacspec/hax/pull/794) properly and +[support `dyn`](https://github.com/hacspec/hax/pull/788). We also +pushed various enhancements (visitors for the internal AST are +generated again, we propagate some more trait generics arguments...) +and bug fixes. + +On the topic of libraries and helper macros, users can [now add +`requires` and `ensures` +clauses](https://github.com/hacspec/hax/pull/790) directly on traits. + +# Merged Pull Requests +* #811: [Add mli for phase_reconstruct_for_index_loops.](https://github.com/hacspec/hax/pull/811) +* #802: [Add json format option](https://github.com/hacspec/hax/pull/802) +* #800: [feat(engine/ocaml_of_json_schema): add `val` to keyword list](https://github.com/hacspec/hax/pull/800) +* #799: [fix(bounded-ints): zero and one were inverted](https://github.com/hacspec/hax/pull/799) +* #797: [Fix potentially looping predicate_id.](https://github.com/hacspec/hax/pull/797) +* #796: [Add nicer error messages when rustc emits an error in detect_forking.](https://github.com/hacspec/hax/pull/796) +* #795: [fix: precondition constraints should be of the shape `true => pred`](https://github.com/hacspec/hax/pull/795) +* #794: [Resugar asserts](https://github.com/hacspec/hax/pull/794) +* #792: [feat(frontend): Add option to control output directory](https://github.com/hacspec/hax/pull/792) +* #790: [Allow `ensures` and `requires` on traits](https://github.com/hacspec/hax/pull/790) +* #788: [Fix #296](https://github.com/hacspec/hax/pull/788) +* #779: [Support let-else pattern.](https://github.com/hacspec/hax/pull/779) +* #777: [Small typo fixes for hax book](https://github.com/hacspec/hax/pull/777) +* #776: [feat(book): fix checkboxes](https://github.com/hacspec/hax/pull/776) +* #769: [Extensions to the proof-libs for libcrux-ml-kem](https://github.com/hacspec/hax/pull/769) +* #765: [fix(engine/lib): import associated item projection on generic bounds](https://github.com/hacspec/hax/pull/765) +* #764: [feat(hax-lib): allow requires & ensures on `&mut` inputs functions](https://github.com/hacspec/hax/pull/764) +* #763: [fix(hax-lib): refinements: various fixes](https://github.com/hacspec/hax/pull/763) +* #762: [fix(hax-lib): `use super::*` in refinement expansion](https://github.com/hacspec/hax/pull/762) +* #759: [fix(frontend): crashes on fn ptr](https://github.com/hacspec/hax/pull/759) +* #758: [fix color printing in util script](https://github.com/hacspec/hax/pull/758) +* #756: [fix(frontend): kill `crate_type` in `HaxMeta`](https://github.com/hacspec/hax/pull/756) +* #753: [ exporter: make it need nightly only when feature `rustc` is on](https://github.com/hacspec/hax/pull/753) +* #751: [Engine: propagate trait generics arguments](https://github.com/hacspec/hax/pull/751) +* #750: [feat(exporter): thir: call: separate trait VS method generic args](https://github.com/hacspec/hax/pull/750) +* #744: [doc(engine): ppx_functor_application](https://github.com/hacspec/hax/pull/744) +* #743: [Refactor of the frontend](https://github.com/hacspec/hax/pull/743) +* #730: [fix(frontend): make `path_to` breadth-first](https://github.com/hacspec/hax/pull/730) +* #729: [Move book from `hacspec/book` to `hacspec/hax`](https://github.com/hacspec/hax/pull/729) +* #727: [fix(engine): `Concrete_ident_generated`: `name` -> `t`, derive more](https://github.com/hacspec/hax/pull/727) +* #698: [Generate visitors automatically](https://github.com/hacspec/hax/pull/698) + +# Contributors +- [paulmure](https://github.com/paulmure) +- [maximebuyse](https://github.com/maximebuyse) +- [karthikbhargavan](https://github.com/karthikbhargavan) +- [W95Psp](https://github.com/W95Psp)