From 456f1d2011ed6ffbf62a23d6787e67f4841f0330 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 13 May 2024 08:34:32 +0200 Subject: [PATCH 1/4] feat(readme): add a header with all relevant links --- README.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/README.md b/README.md index 14abce4f2..4100dfc01 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,11 @@ +

+ 🌐 Website | + 📖 Book | + 📝 Blog | + 💬 Zulip | + 🛠️ Internal docs +

+ # Hax hax is a tool for high assurance translations that translates a large subset of From 60fc0ccce873e3599f224686c865c6ae046ac531 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 13 May 2024 08:35:27 +0200 Subject: [PATCH 2/4] feat(readme): add a `Learn more` section, move examples there --- README.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 4100dfc01..460303237 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,15 @@ standard library, to write succinct, executable, and verifiable specifications i Rust. These specifications can be translated into formal languages with hax. +## Learn more + +Here are some resources for learning more about hax: + - [Book](https://hacspec.org/book) (work in progress) + + [Quick start](https://hacspec.org/book/quick_start/intro.html) + + [Tutorial](https://hacspec.org/book/tutorial/index.html) + - [Examples](examples/): the [examples directory](examples/) contains + a set of examples that show what hax can do for you. + ## Usage Hax is a cargo subcommand. The command `cargo hax` accepts the following subcommands: @@ -99,11 +108,6 @@ Quicklinks: - [🔨 Rejected rust we want to support](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+-label%3Awontfix%2Cwontfix-v1); - [💭 Rejected rust we don't plan to support in v1](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1). -## Examples - -There's a set of examples that show what hax can do for you. -Please check out the [examples directory](examples/). - ## Hacking on Hax ### Edit the sources (Nix) From 96baa4ad782bf36a2272356fe4047f09e0fd5cb8 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 13 May 2024 08:35:42 +0200 Subject: [PATCH 3/4] feat(readme): add `pro-verif` --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 460303237..ea23a7118 100644 --- a/README.md +++ b/README.md @@ -36,8 +36,8 @@ The command `cargo hax` accepts the following subcommands: * **`json`** (`cargo hax json`): extract the typed AST of your crate as a JSON file. Note: - * `BACKEND` can be `fstar`, `coq` or `easycrypt`. `cargo hax into - --help` gives the full list of supported backends. + * `BACKEND` can be `fstar`, `coq`, `easycrypt` or `pro-verif`. `cargo hax into --help` + gives the full list of supported backends. * The subcommands `cargo hax`, `cargo hax into` and `cargo hax into ` takes options. For instance, you can `cargo hax into fstar --z3rlimit 100`. Use `--help` on those subcommands to list From e0b0f91c433c98fc0c8766a6eea4699114a03127 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 13 May 2024 08:36:21 +0200 Subject: [PATCH 4/4] feat(readme): hack on hax: "internal" docs link --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index ea23a7118..ea5591066 100644 --- a/README.md +++ b/README.md @@ -109,6 +109,9 @@ Quicklinks: - [💭 Rejected rust we don't plan to support in v1](https://github.com/hacspec/hax/issues?q=is%3Aissue+is%3Aopen+label%3Aunsupported-rust+label%3Awontfix%2Cwontfix-v1). ## Hacking on Hax +The documentation of the internal crate of hax and its engine can be +found [here](https://hacspec.org/hax/). + ### Edit the sources (Nix) Just clone & `cd` into the repo, then run `nix develop .`.