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, allowing for
better scaling and caching. We also improved the general ergonomics:
diagnostics can now be
output in JSON, we have improved error
messages… And we pushed
various bug fixes.
In the engine, we now resugar
asserts properly and
support dyn. 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 topic of libraries and helper macros, users can now add
requires and ensures
clauses directly on traits.
Merged Pull Requests
- #811: Add mli for phase_reconstruct_for_index_loops.
- #802: Add json format option
- #800: feat(engine/ocaml_of_json_schema): add
valto keyword list - #799: fix(bounded-ints): zero and one were inverted
- #797: Fix potentially looping predicate_id.
- #796: Add nicer error messages when rustc emits an error in detect_forking.
- #795: fix: precondition constraints should be of the shape
true => pred - #794: Resugar asserts
- #792: feat(frontend): Add option to control output directory
- #790: Allow
ensuresandrequireson traits - #788: Fix #296
- #779: Support let-else pattern.
- #777: Small typo fixes for hax book
- #776: feat(book): fix checkboxes
- #769: Extensions to the proof-libs for libcrux-ml-kem
- #765: fix(engine/lib): import associated item projection on generic bounds
- #764: feat(hax-lib): allow requires & ensures on
&mutinputs functions - #763: fix(hax-lib): refinements: various fixes
- #762: fix(hax-lib):
use super::*in refinement expansion - #759: fix(frontend): crashes on fn ptr
- #758: fix color printing in util script
- #756: fix(frontend): kill
crate_typeinHaxMeta - #753: exporter: make it need nightly only when feature
rustcis on - #751: Engine: propagate trait generics arguments
- #750: feat(exporter): thir: call: separate trait VS method generic args
- #744: doc(engine): ppx_functor_application
- #743: Refactor of the frontend
- #730: fix(frontend): make
path_tobreadth-first - #729: Move book from
hacspec/booktohacspec/hax - #727: fix(engine):
Concrete_ident_generated:name->t, derive more - #698: Generate visitors automatically