-
Notifications
You must be signed in to change notification settings - Fork 22
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 #1306 from cryspen/this-month-in-hax
init(docs/blog): this month in hax: January
- Loading branch information
Showing
1 changed file
with
79 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,79 @@ | ||
--- | ||
authors: | ||
- lucas | ||
title: "This Month in Hax: January 2025" | ||
date: 2025-02-10 | ||
--- | ||
|
||
|
||
This blog post continues our ongoing series introduced in the [previous blog of | ||
hax](https://hacspec.org/blog/tags/this-month-in-hax/), a monthly collection of | ||
highlights showcasing key developments in hax and its ecosystem. | ||
|
||
This month, we merged **31 pull requests** and celebrated a major milestone by | ||
releasing the first official version of hax: | ||
[v0.1.0](https://github.com/cryspen/hax/releases/tag/cargo-hax-v0.1.0). If you | ||
haven’t already, be sure to check out [our blog post](../announce-v0.1.md) for | ||
more details on this release! | ||
|
||
We tackled a variety of bug fixes and engine improvements. One significant | ||
achievement was resolving a long-standing issue related to the inconsistent | ||
preservation of declaration orders between Rust and the extractions. This | ||
problem [was finally fixed](https://github.com/cryspen/hax/pull/1247). 🎉 | ||
|
||
Additionally, we merged [a comprehensive | ||
overhaul](https://github.com/cryspen/hax/pull/1199) of how identifiers are | ||
treated and represented within the engine. This rework allowed us to fix nearly | ||
ten related issues, making the system more robust and efficient. | ||
|
||
In the F\* backend, we transitioned away from using | ||
[HACL\*](https://github.com/hacl-star/hacl-star) machine integers. Instead, we | ||
now rely on a [thin wrapper](https://github.com/cryspen/hax/pull/1238) over | ||
F\*'s native mathematical integers. Unlike HACL\*'s opaque machine integers, | ||
this new representation allows us to use F\*'s normalizer freely, offering a | ||
cleaner and more lightweight solution. | ||
|
||
Stay tuned for more updates in the coming months! | ||
|
||
### Full list of PRs | ||
|
||
* \#1278: [ci(gha): drop magic-nix-cache action because of EOL](https://github.com/cryspen/hax/pull/1278) | ||
* \#1277: [fix(mkdocs): use codemirror instead of ace, re-setup on page reload](https://github.com/cryspen/hax/pull/1277) | ||
* \#1275: [Create CODEOWNERS](https://github.com/cryspen/hax/pull/1275) | ||
* \#1273: [Various F* core lib additions.](https://github.com/cryspen/hax/pull/1273) | ||
* \#1267: [fix(hax-lib/macros): handle correctly `&mut Self` arguments in `ensures`](https://github.com/cryspen/hax/pull/1267) | ||
* \#1265: [Fix announce-v0.1.md](https://github.com/cryspen/hax/pull/1265) | ||
* \#1263: [updatge readme and docs](https://github.com/cryspen/hax/pull/1263) | ||
* \#1261: [Update website landing page](https://github.com/cryspen/hax/pull/1261) | ||
* \#1260: [chore(deps): bump hashbrown from 0.15.0 to 0.15.2](https://github.com/cryspen/hax/pull/1260) | ||
* \#1259: [changelog: initialize](https://github.com/cryspen/hax/pull/1259) | ||
* \#1258: [Delete frontend/exporter/json-visualizer directory](https://github.com/cryspen/hax/pull/1258) | ||
* \#1247: [Stable topological sort using original order.](https://github.com/cryspen/hax/pull/1247) | ||
* \#1245: [Release hax v0.1.0](https://github.com/cryspen/hax/pull/1245) | ||
* \#1241: [hax v0.1 blog post](https://github.com/cryspen/hax/pull/1241) | ||
* \#1238: [Transparent integers](https://github.com/cryspen/hax/pull/1238) | ||
* \#1237: [Fix order of `Call` trait clauses](https://github.com/cryspen/hax/pull/1237) | ||
* \#1236: [Add more info to `ImplExprAtom::Builtin`](https://github.com/cryspen/hax/pull/1236) | ||
* \#1230: [fix(engine) Propagate return rewrite to avoid crash in side_effect_utils](https://github.com/cryspen/hax/pull/1230) | ||
* \#1229: [fix(engine) Add type arguments for associated constants.](https://github.com/cryspen/hax/pull/1229) | ||
* \#1228: [fix(engine) Use ocamlgraph fork to fix missing rec bug.](https://github.com/cryspen/hax/pull/1228) | ||
* \#1225: [Hax home page using mkdocs](https://github.com/cryspen/hax/pull/1225) | ||
* \#1223: [fix(engine) Attempt to fix double return bug.](https://github.com/cryspen/hax/pull/1223) | ||
* \#1222: [Make predicate handling a bit more consistent](https://github.com/cryspen/hax/pull/1222) | ||
* \#1220: [Visit trait goals to rename impl expr they may contain.](https://github.com/cryspen/hax/pull/1220) | ||
* \#1216: [Update README.md: `unsafe` is OK to use](https://github.com/cryspen/hax/pull/1216) | ||
* \#1215: [Fix generics handling for function calls](https://github.com/cryspen/hax/pull/1215) | ||
* \#1212: [fix(CI) Update F* version to fix mlkem CI job ](https://github.com/cryspen/hax/pull/1212) | ||
* \#1206: [fix(engine) Make sub-parts of `Quote` visited by visitors](https://github.com/cryspen/hax/pull/1206) | ||
* \#1199: [Engine: rework global name representation](https://github.com/cryspen/hax/pull/1199) | ||
* \#1075: [Move trait methods in cyclic dependencies bundling.](https://github.com/cryspen/hax/pull/1075) | ||
* \#1066: [Add EBNF for AST to book](https://github.com/cryspen/hax/pull/1066) | ||
|
||
### Contributors | ||
* [@Nadrieril](https://github.com/Nadrieril) | ||
* [@W95Psp](https://github.com/W95Psp) | ||
* [@app/dependabot](https://github.com/app/dependabot) | ||
* [@cmester0](https://github.com/cmester0) | ||
* [@franziskuskiefer](https://github.com/franziskuskiefer) | ||
* [@karthikbhargavan](https://github.com/karthikbhargavan) | ||
* [@maximebuyse](https://github.com/maximebuyse) |