-
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 #12 from hacspec/this-month-in-hax-10-2024
This month in hax October 2024.
- Loading branch information
Showing
1 changed file
with
103 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,103 @@ | ||
| --- | ||
| author: "Maxime Buyse" | ||
| title: "This month in hax: October 2024" | ||
| date: "2024-11-04" | ||
| tags: ["this-month-in-hax"] | ||
| ShowToc: false | ||
| ShowBreadCrumbs: false | ||
| --- | ||
|
|
||
| In October, we merged 70 PRs! 🎉 | ||
|
|
||
| Thanks to a huge work from [Nadrieril](https://github.com/Nadrieril) on trait resolution, the goal of handling all valid Rust code with hax frontend is now almost achieved. With these improvements and some bugfixes from [W95Psp](https://github.com/W95Psp), we now produce JSON without errors for more than 99% of Rust's top 800 crates! | ||
|
|
||
| [W95Psp](https://github.com/W95Psp) worked on a new data representation for communication between the frontend and the engine. This removes redundancy and gives great performance gains. | ||
|
|
||
| A new generic printer has been developed by [W95Psp](https://github.com/W95Psp) and is now available for backend development. The coq backend is the first to use it thanks to the migration work from [cmester0](https://github.com/cmester0). | ||
|
|
||
| I have worked on eliminating circular dependencies between the modules we generate. And also on allowing control flow (`return`, `break` and `continue`) inside loops. | ||
|
|
||
| Last but not least, the effort to release v0.1.0 is almost finished. This comes with documentation and tooling improvements. For example, [jschneider-bensch](https://github.com/jschneider-bensch) added a simple PSK based protocol as an example for the ProVerif backend. | ||
|
|
||
| # Merged Pull Requests | ||
| * #1087: [Fix two query panics](https://github.com/hacspec/hax/pull/1087) | ||
| * #1084: [fix(engine/simplify_question_marks): fix type arguments on `from`](https://github.com/hacspec/hax/pull/1084) | ||
| * #1079: [Include defaulted items in `FullDefKind::TraitImpl`](https://github.com/hacspec/hax/pull/1079) | ||
| * #1077: [fix(engine) Keep late_skip attributes in bundles](https://github.com/hacspec/hax/pull/1077) | ||
| * #1074: [feat(engine): profile each phase (mem usage, time, number of items)](https://github.com/hacspec/hax/pull/1074) | ||
| * #1071: [count_ones and bool->int](https://github.com/hacspec/hax/pull/1071) | ||
| * #1069: [Add `ImplExpr` information to associated types in an impl block](https://github.com/hacspec/hax/pull/1069) | ||
| * #1067: [feat(book): allow F* extraction + TC from within the book](https://github.com/hacspec/hax/pull/1067) | ||
| * #1063: [Add module information to `FullDef`](https://github.com/hacspec/hax/pull/1063) | ||
| * #1062: [fix(engine) Remove attributes on bundle aliases and filter out NotImplementedYet.](https://github.com/hacspec/hax/pull/1062) | ||
| * #1061: [feat(frontend/consts): float lits: use strings not bits, more support](https://github.com/hacspec/hax/pull/1061) | ||
| * #1057: [fix(exporter/constants): support usize casted to raw pointers constants](https://github.com/hacspec/hax/pull/1057) | ||
| * #1056: [fix(engine) Avoid wrapping return in a tuple.](https://github.com/hacspec/hax/pull/1056) | ||
| * #1055: [Include bodies in `FullDef`](https://github.com/hacspec/hax/pull/1055) | ||
| * #1054: [Intern `DefId`s](https://github.com/hacspec/hax/pull/1054) | ||
| * #1053: [Avoid a panic in `FullDef`](https://github.com/hacspec/hax/pull/1053) | ||
| * #1052: [fix(exporter/thir): fix #1048](https://github.com/hacspec/hax/pull/1052) | ||
| * #1050: [Fix #1042](https://github.com/hacspec/hax/pull/1050) | ||
| * #1049: [fix(engine) Move variant constructors in recursive bundling.](https://github.com/hacspec/hax/pull/1049) | ||
| * #1041: [fix: rustc_private](https://github.com/hacspec/hax/pull/1041) | ||
| * #1039: [Fix 914](https://github.com/hacspec/hax/pull/1039) | ||
| * #1037: [Machine int constructors and conversions](https://github.com/hacspec/hax/pull/1037) | ||
| * #1036: [Upgrade rustc](https://github.com/hacspec/hax/pull/1036) | ||
| * #1035: [feat: check licenses](https://github.com/hacspec/hax/pull/1035) | ||
| * #1031: [Improve trait resolution](https://github.com/hacspec/hax/pull/1031) | ||
| * #1030: [Avoid bundling use items.](https://github.com/hacspec/hax/pull/1030) | ||
| * #1029: [feat: deduplicate types in haxmeta and JSON](https://github.com/hacspec/hax/pull/1029) | ||
| * #1027: [fix(frontend): this was reverted by mistake](https://github.com/hacspec/hax/pull/1027) | ||
| * #1024: [Reorganize `frontend/exporter/types`](https://github.com/hacspec/hax/pull/1024) | ||
| * #1023: [PV backend example: Simple PSK based protocol](https://github.com/hacspec/hax/pull/1023) | ||
| * #1022: [some fixes for iterators.f_next and update_at_usize](https://github.com/hacspec/hax/pull/1022) | ||
| * #1020: [Quote items track replace](https://github.com/hacspec/hax/pull/1020) | ||
| * #1018: [fix(engine/import_thir): never drop bodies of constants](https://github.com/hacspec/hax/pull/1018) | ||
| * #1015: [fix(frontend): issue #1014](https://github.com/hacspec/hax/pull/1015) | ||
| * #1012: [fix: justfile](https://github.com/hacspec/hax/pull/1012) | ||
| * #1011: [fix(engine): also rename concrete idents within a projector.](https://github.com/hacspec/hax/pull/1011) | ||
| * #1008: [Support `impl Trait` in trait resolution](https://github.com/hacspec/hax/pull/1008) | ||
| * #1007: [feat(cli): better version information](https://github.com/hacspec/hax/pull/1007) | ||
| * #1006: [Support more features](https://github.com/hacspec/hax/pull/1006) | ||
| * #1002: [Fix bug with recursive bundles depending on items from original modules.](https://github.com/hacspec/hax/pull/1002) | ||
| * #1000: [Cache `FullDef` translation and add more information to it](https://github.com/hacspec/hax/pull/1000) | ||
| * #999: [Exporter get variant information works on unions](https://github.com/hacspec/hax/pull/999) | ||
| * #996: [Cache many things](https://github.com/hacspec/hax/pull/996) | ||
| * #994: [fix: DEV.md debug engine](https://github.com/hacspec/hax/pull/994) | ||
| * #990: [Remove workaround in trait resolution for associated items](https://github.com/hacspec/hax/pull/990) | ||
| * #989: [fix(engine): make consts fun. calls of arity 0 when there is an impl expr](https://github.com/hacspec/hax/pull/989) | ||
| * #988: [feat(engine) Rewrite control flow inside loops.](https://github.com/hacspec/hax/pull/988) | ||
| * #987: [Coq generic printer](https://github.com/hacspec/hax/pull/987) | ||
| * #984: [feat: just use `just`](https://github.com/hacspec/hax/pull/984) | ||
| * #981: [Make options extensible](https://github.com/hacspec/hax/pull/981) | ||
| * #977: [More improvements to trait resolution](https://github.com/hacspec/hax/pull/977) | ||
| * #970: [Rework trait resolution to support GATs](https://github.com/hacspec/hax/pull/970) | ||
| * #969: [Release `0.1.0-alpha.1`](https://github.com/hacspec/hax/pull/969) | ||
| * #964: [feat(contributing): add a `regressions` section](https://github.com/hacspec/hax/pull/964) | ||
| * #961: [Update README.md](https://github.com/hacspec/hax/pull/961) | ||
| * #960: [feat(engine): add `ast_destruct` module](https://github.com/hacspec/hax/pull/960) | ||
| * #959: [Prefer `try_normalize_erasing_regions`](https://github.com/hacspec/hax/pull/959) | ||
| * #958: [feat(engine): add module `ast_builder`](https://github.com/hacspec/hax/pull/958) | ||
| * #957: [Ignore structs in variants renaming for bundling.](https://github.com/hacspec/hax/pull/957) | ||
| * #956: [Run `cargo clippy --fix`](https://github.com/hacspec/hax/pull/956) | ||
| * #955: [feat(frontend): collect regular comments](https://github.com/hacspec/hax/pull/955) | ||
| * #952: [feat(doc): add `CONTRIBUTING.md`](https://github.com/hacspec/hax/pull/952) | ||
| * #950: [feat(nix/utils): intro. `check-unimlemented-issue-coherency`](https://github.com/hacspec/hax/pull/950) | ||
| * #949: [fix(engine): change issue id](https://github.com/hacspec/hax/pull/949) | ||
| * #948: [fix(engine/f*): convert an unimplemented to an assertion failure](https://github.com/hacspec/hax/pull/948) | ||
| * #947: [fix(exporter+engine): drop default parameters on traits](https://github.com/hacspec/hax/pull/947) | ||
| * #945: [feat(engine/f*): allow unsafe code](https://github.com/hacspec/hax/pull/945) | ||
| * #935: [Handle cyclic module dependencies](https://github.com/hacspec/hax/pull/935) | ||
| * #851: [fix(engine): expose type of local_ident.id](https://github.com/hacspec/hax/pull/851) | ||
| * #533: [more principled generic printer](https://github.com/hacspec/hax/pull/533) | ||
|
|
||
| ### 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) |