-
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 #13 from hacspec/this-month-in-hax-11-24
This month in hax: 2024-11
- Loading branch information
Showing
2 changed files
with
76 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,76 @@ | ||
| --- | ||
| author: "Lucas Franceschino" | ||
| title: "This month in hax: November 2024" | ||
| date: "2024-12-03" | ||
| tags: ["this-month-in-hax"] | ||
| ShowToc: false | ||
| ShowBreadCrumbs: false | ||
| --- | ||
|
|
||
| Despite some team members attending an offsite work week event, we | ||
| merged 24 PRs this month. Here's an overview of the work of the month. | ||
|
|
||
| The frontend remained stable this month, with only a few pull requests | ||
| focused on small improvements and bug fixes. Our CI now tests the | ||
| extraction of [Rust by | ||
| Example](https://doc.rust-lang.org/rust-by-example/). | ||
|
|
||
| [cmester0](https://github.com/cmester0) is working on an annotated core | ||
| library, which is extractable via hax to multiple backends. The Coq | ||
| backend now uses this generated core library, and ships with an | ||
| example. | ||
|
|
||
| I want to add source maps to hax for a long time. A source map is a | ||
| file that maps transformed code to its original source code. This | ||
| mapping is particularly useful in debugging, allowing developers to | ||
| see the original source code when errors occur or when stepping | ||
| through code in a debugger. | ||
|
|
||
| Support for source maps was added previously, but was not really | ||
| usable. Source maps are now being automatically for the backends using | ||
| the generic printer (currently only Coq does so). Here is a preview: | ||
|
|
||
|  | ||
|
|
||
| Lastly, we fixed a several issues and enhanced the engine. For | ||
| instance, control is now rewritten correctly within closures. | ||
|
|
||
| Get involved with Hax! Submit issues, suggest improvements, or upvote | ||
| the ones you care about on GitHub. Every contribution counts! ☀️ | ||
|
|
||
| # Merged Pull Requests | ||
| * #1149: [Revert "fix(engine): item ordering"](https://github.com/hacspec/hax/pull/1149) | ||
| * #1147: [Engine: F*: fix `\0`](https://github.com/hacspec/hax/pull/1147) | ||
| * #1146: [Improve `setup.sh`](https://github.com/hacspec/hax/pull/1146) | ||
| * #1140: [fix(engine): item ordering](https://github.com/hacspec/hax/pull/1140) | ||
| * #1123: [Engine: source maps: fix bugs, add features, enable for Coq](https://github.com/hacspec/hax/pull/1123) | ||
| * #1122: [Various tweaks](https://github.com/hacspec/hax/pull/1122) | ||
| * #1121: [fix typos in the book](https://github.com/hacspec/hax/pull/1121) | ||
| * #1118: [doc(book/include-flags): improve](https://github.com/hacspec/hax/pull/1118) | ||
| * #1117: [Upstream fstar core changes from cryspen-sandwich.](https://github.com/hacspec/hax/pull/1117) | ||
| * #1116: [feat(frontend/cli): improve options](https://github.com/hacspec/hax/pull/1116) | ||
| * #1115: [Cryspen green.](https://github.com/hacspec/hax/pull/1115) | ||
| * #1114: [feat(engine) Extract vals for trait impls in interface only mode.](https://github.com/hacspec/hax/pull/1114) | ||
| * #1111: [chore(engine): ocamlformat: update: 0.24.1 -> 0.26.2](https://github.com/hacspec/hax/pull/1111) | ||
| * #1102: [fix(engine) Fix deprecated attribute for compatibility with ocaml 5.2.](https://github.com/hacspec/hax/pull/1102) | ||
| * #1101: [fix(engine) Drop return/break/continue inside closures.](https://github.com/hacspec/hax/pull/1101) | ||
| * #1100: [Fix spans in error reporting with unicode characters.](https://github.com/hacspec/hax/pull/1100) | ||
| * #1094: [Fix ml-kem ci job.](https://github.com/hacspec/hax/pull/1094) | ||
| * #1092: [feat(ci): test rust by examples (extract to F*)](https://github.com/hacspec/hax/pull/1092) | ||
| * #1091: [Add example for Coq](https://github.com/hacspec/hax/pull/1091) | ||
| * #1090: [feat(engine/f*): add dummy support for floats](https://github.com/hacspec/hax/pull/1090) | ||
| * #1080: [feat(engine): keep track of parent items in spans](https://github.com/hacspec/hax/pull/1080) | ||
| * #1064: [Move to annotated core lib](https://github.com/hacspec/hax/pull/1064) | ||
| * #1004: [Restore neg_equiv_lemma](https://github.com/hacspec/hax/pull/1004) | ||
| * #983: [feat(hax-lib): intro. `hax` feature](https://github.com/hacspec/hax/pull/983) | ||
|
|
||
| ### Contributors | ||
| * [@cmester0](https://github.com/cmester0) | ||
| * [@W95Psp](https://github.com/W95Psp) | ||
| * [@jschneider-bensch](https://github.com/jschneider-bensch) | ||
| * [@spitters](https://github.com/spitters) | ||
| * [@franziskuskiefer](https://github.com/franziskuskiefer) | ||
| * [@Nadrieril](https://github.com/Nadrieril) | ||
| * [@karthikbhargavan](https://github.com/karthikbhargavan) | ||
| * [@maximebuyse](https://github.com/maximebuyse) | ||
| * [@paulmure](https://github.com/paulmure) |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.