Skip to content

Commit

Permalink
feat: this-month-in-hax: first post
Browse files Browse the repository at this point in the history
  • Loading branch information
Lucas Franceschino committed Jul 2, 2024
1 parent 23dc965 commit 3091874
Showing 1 changed file with 57 additions and 0 deletions.
57 changes: 57 additions & 0 deletions content/posts/this-month-in-hax/2024-06.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
---
author: "Lucas Franceschino"
title: "This month in hax: June 2024"
date: "2024-07-02"
tags: ["this-month-in-hax"]
ShowToc: false
ShowBreadCrumbs: false
---

This first blog post inaugurates our series named "This Month in hax":
a series of short highlights of what happened in the development of
hax and it's ecosystem in the month.

In June, 30 PRs have been merged 🎉! The detail is available below.

On the Rust side, we have updated the Rust compiler to a very recent
nightly thanks to [@Nadrieril](https://github.com/Nadrieril)! We also
added support for more Rust features in the frontend ([`dyn
Trait`]((https://github.com/hacspec/hax/pull/741)), (more disciminant
informations on ADTs)[https://github.com/hacspec/hax/pull/693]), fixed
various bugs, and improved the general experience of using hax.

We pushed many fixes for the F* backend in the engine and improved the
F* proof library. We also improved the bounded integer library and
it's F* integration.

# Merge Pull Requests
- [Translate `dyn Trait` information](https://github.com/hacspec/hax/pull/741)
- [fix(engine/fstar): use `Base.String.hash` instead of `String.hash`](https://github.com/hacspec/hax/pull/740)
- [feat: add LICENSE](https://github.com/hacspec/hax/pull/736)
- [Update rustc all at once](https://github.com/hacspec/hax/pull/735)
- [refactor(engine/fstar-ast): get rid of `zarith` and GMP](https://github.com/hacspec/hax/pull/734)
- [Update rustc](https://github.com/hacspec/hax/pull/733)
- [fix(engine/fstar): fix implicit discrepancies in traits](https://github.com/hacspec/hax/pull/726)
- [feat(nix): reduce closure size for hax-engine](https://github.com/hacspec/hax/pull/724)
- [Generalize bounded ints](https://github.com/hacspec/hax/pull/723)
- [Don't use strings to represent paths](https://github.com/hacspec/hax/pull/722)
- [Update rustc](https://github.com/hacspec/hax/pull/721)
- [Update intro.md: use latest version of gist for makefile](https://github.com/hacspec/hax/pull/19)
- [fix(backends/fstar): no `__marker_trait` if parent bounds](https://github.com/hacspec/hax/pull/712)
- [feat(proof-libs): add `t_Default`](https://github.com/hacspec/hax/pull/711)
- [Fix typo in intro.md](https://github.com/hacspec/hax/pull/18)
- [feat(hax): logging: enable tracing in release, add trait-related logs](https://github.com/hacspec/hax/pull/710)
- [fix(exporter): disable impl expr resolution under type aliases](https://github.com/hacspec/hax/pull/709)
- [fix: rename action for extracting ml-kem](https://github.com/hacspec/hax/pull/704)
- [feat: isolate `DefId`: faster build times](https://github.com/hacspec/hax/pull/703)
- [fix(README): always begin relative path with `./`, rewrite in action](https://github.com/hacspec/hax/pull/702)
- [fix(ci): newer version of `ppx_deriving` (6.0.2) loops indefinitely](https://github.com/hacspec/hax/pull/697)
- [Update to OCaml 5](https://github.com/hacspec/hax/pull/694)
- [Export discriminant values in `AdtDef`](https://github.com/hacspec/hax/pull/693)
- [Update README.md](https://github.com/hacspec/hax/pull/691)
- [Bump rustc version](https://github.com/hacspec/hax/pull/690)
- [Bump rustc version](https://github.com/hacspec/hax/pull/687)
- [refactor(exporter): always use `State::param_env`](https://github.com/hacspec/hax/pull/685)
- [fix(exporter): fixes #680](https://github.com/hacspec/hax/pull/681)
- [Engine: F*: fix #677 by always extracting implicit types](https://github.com/hacspec/hax/pull/679)
- [Engine: F*: open modules providing trait impls](https://github.com/hacspec/hax/pull/676)

0 comments on commit 3091874

Please sign in to comment.