-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #9 from hacspec/this-month-in-hax
this month in hax: 2024-07
- Loading branch information
Showing
1 changed file
with
69 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) |