-
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 #11 from hacspec/this-month-in-hax-09-24
this month in hax: 09
- Loading branch information
Showing
1 changed file
with
77 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,77 @@ | ||
| --- | ||
| author: "Lucas Franceschino" | ||
| title: "This month in hax: September 2024" | ||
| date: "2024-10-01" | ||
| tags: ["this-month-in-hax"] | ||
| ShowToc: false | ||
| ShowBreadCrumbs: false | ||
| --- | ||
|
|
||
| In July, we merged 33 PRs! 🎉 | ||
|
|
||
| On the side of the frontend, [Nadrieril](https://github.com/Nadrieril) | ||
| and I worked at making hax handling of binders (e.g. `'a` in `for<'a> | ||
| &'a T: PartialEq<i32>`) and traits better. This is not finished yet, | ||
| but we made great progress. Our goal is to make the frontend work on | ||
| every valid Rust code. | ||
|
|
||
| In the engine, thanks to [paulmure](https://github.com/paulmure), we | ||
| now are able to process `unsafe` blocks. Thanks to | ||
| [maximebuyse](https://github.com/maximebuyse), the engine can now | ||
| rewrite more `return` expressions: we are now planning on supporting | ||
| `return` inside loops, along with `break` and `continue`. | ||
|
|
||
| We've been improving F* support and F* libraries. Importantly, | ||
| [cmester0](https://github.com/cmester0) is working on a model of | ||
| `core`, in Rust: we aim at replacing our hand-crafted F* model of core | ||
| by an hax extraction of this new core model implemented in Rust. We | ||
| will also be able to extract this model of core in every of our | ||
| backends, enabling a uniform and pain-free `core` multi-backend | ||
| library. | ||
|
|
||
| # Merged Pull Requests | ||
| * #934: [chore: assign an issue id for every error in the engine](https://github.com/hacspec/hax/pull/934) | ||
| * #932: [chore: assign an issue for every error in `import_thir`](https://github.com/hacspec/hax/pull/932) | ||
| * #919: [fix #422](https://github.com/hacspec/hax/pull/919) | ||
| * #918: [chore: remove stale `Hax.Lib.fst`](https://github.com/hacspec/hax/pull/918) | ||
| * #917: [doc: disambiguate_local_idents](https://github.com/hacspec/hax/pull/917) | ||
| * #916: [update Cargo.lock](https://github.com/hacspec/hax/pull/916) | ||
| * #909: [Revert "fix(engine/fstar): fix super typeclasses attributes"](https://github.com/hacspec/hax/pull/909) | ||
| * #908: [fix(engine/deps): stop re-computing over and over the set of assoc items](https://github.com/hacspec/hax/pull/908) | ||
| * #907: [Add RewriteControlFlow phase.](https://github.com/hacspec/hax/pull/907) | ||
| * #906: [Cleanup trait resolution](https://github.com/hacspec/hax/pull/906) | ||
| * #902: [fix(engine/fstar): fix super typeclasses attributes](https://github.com/hacspec/hax/pull/902) | ||
| * #901: [Determine emuerate value by index](https://github.com/hacspec/hax/pull/901) | ||
| * #898: [Fix some binder-related crashes](https://github.com/hacspec/hax/pull/898) | ||
| * #895: [Don't eval constants eagerly](https://github.com/hacspec/hax/pull/895) | ||
| * #894: [Detangle trait solving from `SInto`](https://github.com/hacspec/hax/pull/894) | ||
| * #892: [Support other variants of MIR](https://github.com/hacspec/hax/pull/892) | ||
| * #891: [fix: fstar: default trait](https://github.com/hacspec/hax/pull/891) | ||
| * #887: [Initial cleanup of binders-related code](https://github.com/hacspec/hax/pull/887) | ||
| * #885: [docs(book): depend on `hax-lib` only when using hax](https://github.com/hacspec/hax/pull/885) | ||
| * #884: [Fix incorrect line numbers in error messages](https://github.com/hacspec/hax/pull/884) | ||
| * #883: [Fix step boundaries in fold_range_step_by](https://github.com/hacspec/hax/pull/883) | ||
| * #882: [fix(fstar-core): add support for `Option::map`](https://github.com/hacspec/hax/pull/882) | ||
| * #880: [Support float literals](https://github.com/hacspec/hax/pull/880) | ||
| * #877: [Avoid recursing twice on the arguments.](https://github.com/hacspec/hax/pull/877) | ||
| * #876: [Translate additional unsafe MIR operations](https://github.com/hacspec/hax/pull/876) | ||
| * #873: [Small PR to fix circularity in Core.Fmt.fsti](https://github.com/hacspec/hax/pull/873) | ||
| * #872: [Pre post impl blocks](https://github.com/hacspec/hax/pull/872) | ||
| * #870: [count-ones post-condition](https://github.com/hacspec/hax/pull/870) | ||
| * #868: [engine: kill a few `exn` to get useful errors](https://github.com/hacspec/hax/pull/868) | ||
| * #867: [Backend: Import unsafe code as a gated feature](https://github.com/hacspec/hax/pull/867) | ||
| * #860: [fix(engine): make dep. analysis sensible to UID assoc. items](https://github.com/hacspec/hax/pull/860) | ||
| * #827: [Add infos impl](https://github.com/hacspec/hax/pull/827) | ||
| * #819: [Add Rust Core Fstar Definitions.](https://github.com/hacspec/hax/pull/819) | ||
|
|
||
| #### Contributors | ||
| - [Nadrieril](https://github.com/Nadrieril) | ||
| - [R1kM](https://github.com/R1kM) | ||
| - [ROMemories](https://github.com/ROMemories) | ||
| - [W95Psp](https://github.com/W95Psp) | ||
| - [franziskuskiefer](https://github.com/franziskuskiefer) | ||
| - [gaetan-sbt](https://github.com/gaetan-sbt) | ||
| - [karthikbhargavan](https://github.com/karthikbhargavan) | ||
| - [mamonet](https://github.com/mamonet) | ||
| - [maximebuyse](https://github.com/maximebuyse) | ||
| - [paulmure](https://github.com/paulmure) |