Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

this month in hax: 2024-07 #9

Merged
merged 6 commits into from
Aug 12, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions content/posts/this-month-in-hax/2024-07.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
---
author: "Lucas Franceschino"
title: "This month in hax: July 2024"
date: "2024-08-12"
tags: ["this-month-in-hax"]
ShowToc: false
ShowBreadCrumbs: false
---

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](https://github.com/hacspec/hax/pull/743), allowing for
better scaling and caching. We also improved the general ergonomics:
diagnostics can [now](https://github.com/hacspec/hax/pull/802) be
output in JSON, we have [improved error
messages](https://github.com/hacspec/hax/pull/796)... And we pushed
various bug fixes.

In the engine, we now [resugar
asserts](https://github.com/hacspec/hax/pull/794) properly and
[support `dyn`](https://github.com/hacspec/hax/pull/788). 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](https://github.com/hacspec/hax/pull/790) directly on traits.

# Merged Pull Requests
* #811: [Add mli for phase_reconstruct_for_index_loops.](https://github.com/hacspec/hax/pull/811)
* #802: [Add json format option](https://github.com/hacspec/hax/pull/802)
* #800: [feat(engine/ocaml_of_json_schema): add `val` to keyword list](https://github.com/hacspec/hax/pull/800)
* #799: [fix(bounded-ints): zero and one were inverted](https://github.com/hacspec/hax/pull/799)
* #797: [Fix potentially looping predicate_id.](https://github.com/hacspec/hax/pull/797)
* #796: [Add nicer error messages when rustc emits an error in detect_forking.](https://github.com/hacspec/hax/pull/796)
* #795: [fix: precondition constraints should be of the shape `true => pred`](https://github.com/hacspec/hax/pull/795)
* #794: [Resugar asserts](https://github.com/hacspec/hax/pull/794)
* #792: [feat(frontend): Add option to control output directory](https://github.com/hacspec/hax/pull/792)
* #790: [Allow `ensures` and `requires` on traits](https://github.com/hacspec/hax/pull/790)
* #788: [Fix #296](https://github.com/hacspec/hax/pull/788)
* #779: [Support let-else pattern.](https://github.com/hacspec/hax/pull/779)
* #777: [Small typo fixes for hax book](https://github.com/hacspec/hax/pull/777)
* #776: [feat(book): fix checkboxes](https://github.com/hacspec/hax/pull/776)
* #769: [Extensions to the proof-libs for libcrux-ml-kem](https://github.com/hacspec/hax/pull/769)
* #765: [fix(engine/lib): import associated item projection on generic bounds](https://github.com/hacspec/hax/pull/765)
* #764: [feat(hax-lib): allow requires & ensures on `&mut` inputs functions](https://github.com/hacspec/hax/pull/764)
* #763: [fix(hax-lib): refinements: various fixes](https://github.com/hacspec/hax/pull/763)
* #762: [fix(hax-lib): `use super::*` in refinement expansion](https://github.com/hacspec/hax/pull/762)
* #759: [fix(frontend): crashes on fn ptr](https://github.com/hacspec/hax/pull/759)
* #758: [fix color printing in util script](https://github.com/hacspec/hax/pull/758)
* #756: [fix(frontend): kill `crate_type` in `HaxMeta`](https://github.com/hacspec/hax/pull/756)
* #753: [ exporter: make it need nightly only when feature `rustc` is on](https://github.com/hacspec/hax/pull/753)
* #751: [Engine: propagate trait generics arguments](https://github.com/hacspec/hax/pull/751)
* #750: [feat(exporter): thir: call: separate trait VS method generic args](https://github.com/hacspec/hax/pull/750)
* #744: [doc(engine): ppx_functor_application](https://github.com/hacspec/hax/pull/744)
* #743: [Refactor of the frontend](https://github.com/hacspec/hax/pull/743)
* #730: [fix(frontend): make `path_to` breadth-first](https://github.com/hacspec/hax/pull/730)
* #729: [Move book from `hacspec/book` to `hacspec/hax`](https://github.com/hacspec/hax/pull/729)
* #727: [fix(engine): `Concrete_ident_generated`: `name` -> `t`, derive more](https://github.com/hacspec/hax/pull/727)
* #698: [Generate visitors automatically](https://github.com/hacspec/hax/pull/698)

# Contributors
- [paulmure](https://github.com/paulmure)
- [maximebuyse](https://github.com/maximebuyse)
- [karthikbhargavan](https://github.com/karthikbhargavan)
- [W95Psp](https://github.com/W95Psp)
Loading