From f66b361aa94a3b063d3dc0a85b3206d4f5382f4f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 08:59:25 +0200 Subject: [PATCH 1/6] this month in hax: 2024-07 --- content/posts/this-month-in-hax/2024-07.md | 70 ++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 content/posts/this-month-in-hax/2024-07.md 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..46f018b --- /dev/null +++ b/content/posts/this-month-in-hax/2024-07.md @@ -0,0 +1,70 @@ +--- +author: "Lucas Franceschino" +title: "This month in hax: July 2024" +date: "2024-08-12" +tags: ["this-month-in-hax"] +ShowToc: false +ShowBreadCrumbs: false +--- + +That's the second blog post of our "This Month in hax" series, and +this month, 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 +outputted in JSON, we have [improved error +messages](https://github.com/hacspec/hax/pull/796)... And we pushed +various bug fixes. + +On 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 thematic 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) From 4ab71ed4bab187b3b031aa807e67943177327419 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 11:29:25 +0200 Subject: [PATCH 2/6] Update content/posts/this-month-in-hax/2024-07.md Co-authored-by: Franziskus Kiefer --- content/posts/this-month-in-hax/2024-07.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md index 46f018b..70b545c 100644 --- a/content/posts/this-month-in-hax/2024-07.md +++ b/content/posts/this-month-in-hax/2024-07.md @@ -7,8 +7,7 @@ ShowToc: false ShowBreadCrumbs: false --- -That's the second blog post of our "This Month in hax" series, and -this month, in july, we merged 32 PRs! 🎉 +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 From 4e1c6a96df86dd26078c282016b42e5140cfc667 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 11:29:32 +0200 Subject: [PATCH 3/6] Update content/posts/this-month-in-hax/2024-07.md Co-authored-by: Franziskus Kiefer --- content/posts/this-month-in-hax/2024-07.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md index 70b545c..435a581 100644 --- a/content/posts/this-month-in-hax/2024-07.md +++ b/content/posts/this-month-in-hax/2024-07.md @@ -14,7 +14,7 @@ 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 -outputted in JSON, we have [improved error +output in JSON, we have [improved error messages](https://github.com/hacspec/hax/pull/796)... And we pushed various bug fixes. From 0dbb420704279a8f44079bd3e9065c494824b371 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 11:29:37 +0200 Subject: [PATCH 4/6] Update content/posts/this-month-in-hax/2024-07.md Co-authored-by: Franziskus Kiefer --- content/posts/this-month-in-hax/2024-07.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md index 435a581..d48f1be 100644 --- a/content/posts/this-month-in-hax/2024-07.md +++ b/content/posts/this-month-in-hax/2024-07.md @@ -18,7 +18,7 @@ output in JSON, we have [improved error messages](https://github.com/hacspec/hax/pull/796)... And we pushed various bug fixes. -On the engine, we now [resugar +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 From 199deefc85693de578032c6ae5ab59616a8e2322 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 11:29:45 +0200 Subject: [PATCH 5/6] Update content/posts/this-month-in-hax/2024-07.md Co-authored-by: Franziskus Kiefer --- content/posts/this-month-in-hax/2024-07.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md index d48f1be..267d2be 100644 --- a/content/posts/this-month-in-hax/2024-07.md +++ b/content/posts/this-month-in-hax/2024-07.md @@ -25,7 +25,7 @@ pushed various enhancements (visitors for the internal AST are generated again, we propagate some more trait generics arguments...) and bug fixes. -On the thematic of libraries and helper macros, users can [now add +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. From 38f07f2f2c85c600e0031252de860d4981a60bee Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 12 Aug 2024 11:30:04 +0200 Subject: [PATCH 6/6] Update content/posts/this-month-in-hax/2024-07.md Co-authored-by: Franziskus Kiefer --- content/posts/this-month-in-hax/2024-07.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/content/posts/this-month-in-hax/2024-07.md b/content/posts/this-month-in-hax/2024-07.md index 267d2be..e85fe63 100644 --- a/content/posts/this-month-in-hax/2024-07.md +++ b/content/posts/this-month-in-hax/2024-07.md @@ -63,7 +63,7 @@ clauses](https://github.com/hacspec/hax/pull/790) directly on traits. * #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) +- [paulmure](https://github.com/paulmure) +- [maximebuyse](https://github.com/maximebuyse) +- [karthikbhargavan](https://github.com/karthikbhargavan) +- [W95Psp](https://github.com/W95Psp)