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

feat: this-month-in-hax: first post #7

Merged
merged 1 commit into from
Jul 3, 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
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)
Loading