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.
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”
- #1147: Engine: F*: fix
\0
- #1146: Improve
setup.sh
- #1140: fix(engine): item ordering
- #1123: Engine: source maps: fix bugs, add features, enable for Coq
- #1122: Various tweaks
- #1121: fix typos in the book
- #1118: doc(book/include-flags): improve
- #1117: Upstream fstar core changes from cryspen-sandwich.
- #1116: feat(frontend/cli): improve options
- #1115: Cryspen green.
- #1114: feat(engine) Extract vals for trait impls in interface only mode.
- #1111: chore(engine): ocamlformat: update: 0.24.1 -> 0.26.2
- #1102: fix(engine) Fix deprecated attribute for compatibility with ocaml 5.2.
- #1101: fix(engine) Drop return/break/continue inside closures.
- #1100: Fix spans in error reporting with unicode characters.
- #1094: Fix ml-kem ci job.
- #1092: feat(ci): test rust by examples (extract to F*)
- #1091: Add example for Coq
- #1090: feat(engine/f*): add dummy support for floats
- #1080: feat(engine): keep track of parent items in spans
- #1064: Move to annotated core lib
- #1004: Restore neg_equiv_lemma
- #983: feat(hax-lib): intro.
hax
feature