From bb3d4311e174a9cca48c92a392f90a89841c72df Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 18 Nov 2024 11:03:21 +0100 Subject: [PATCH 01/10] doc(book): architecture of hax --- book/src/SUMMARY.md | 2 +- book/src/contributing/architecture.md | 84 +++++++++++++++++++++++++++ book/src/contributing/structure.md | 0 3 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 book/src/contributing/architecture.md delete mode 100644 book/src/contributing/structure.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index e5f094882..1201418f5 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -19,7 +19,7 @@ - [Command line usage]() - [The include flag: which items should be extracted, and how?](faq/include-flags.md) - [Contributing]() - - [Structure]() + - [Architecture](contributing/architecture.md) - [Hax Cargo subcommand]() - [Frontend: the Rustc driver]() - [Frontend: the exporter]() diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md new file mode 100644 index 000000000..d6fcab013 --- /dev/null +++ b/book/src/contributing/architecture.md @@ -0,0 +1,84 @@ +# Architecture + +Hax is a software pipeline designed to transform Rust code into various formal verification backends such as **F\***, **Coq**, **ProVerif**, and **EasyCrypt**. It comprises two main components: + +1. **The Frontend** (written in Rust) +2. **The Engine** (written in OCaml) + +## The Frontend (Rust) + +The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). + +### `hax-frontend-exporter` Library + +This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes IDs indirections. + +**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. + +### `hax-driver` Binary + +`hax-driver` is a custom Rust compiler driver that behaves like `rustc` but performs additional tasks: + +1. **Item Enumeration:** Lists all items in a crate. +2. **AST Transformation:** Applies `sinto` on each item to generate the hax-ified AST. +3. **Output Generation:** Outputs the mirrored items into a `haxmeta` file within the `target` directory. + +### `cargo-hax` Binary + +`cargo-hax` provides a `hax` subcommand for Cargo, accessible via `cargo hax --help`. It serves as the command-line interface for hax, orchestrating both the frontend and the engine. + +**Workflow:** + +1. **Custom Build Execution:** Runs `cargo build`, instructing Cargo to use `hax-driver` instead of `rustc`. +2. **Multiple Compiler Invocations:** `cargo build` invokes `hax-driver` multiple times with various options. +3. **Inter-Process Communication:** `hax-driver` communicates with `cargo-hax` via `stderr` using JSON lines. +4. **Metadata Generation:** Produces `haxmeta` files containing the transformed ASTs. +5. **Engine Invocation (Optional):** If requested, runs the engine, passing options and `haxmeta` information via `stdin` serialized as JSON. +6. **Interactive Communication:** Engages in interactive communication with the engine. +7. **User Reporting:** Outputs results and diagnostics to the user. + +## The Engine (OCaml) + +The engine processes the transformed ASTs and options provided via JSON input from `stdin`. It performs several key functions to convert the hax-ified Rust code into the target backend language. + +### Importing and Simplifying ASTs + +- **AST Importation:** Imports the hax-ified Rust THIR AST. +- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. + +### Internal AST and Features + +The internal AST is defined using a **functor** that takes a list of type-level booleans, referred to as **features**, and produces the AST types accordingly. + +Features are for instances, mutation, loops, unsafe code. A full list is available in `engine/lib/features.ml`. + +**Feature Witnesses:** + +- On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. +- **Example:** In the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. + +### Transformation Phases + +The engine executes a sequence of **phases**, which are determined based on the target backend. Each phase: + +1. **Input:** Takes a list of items from an AST with specific feature constraints. +2. **Output:** Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes. + +The phases can be found in the `engin/lib/phases/` folder. + +### Backend Code Generation + +After completing the transformation phases: + +1. **Backend Printer Invocation:** Calls the printer associated with the selected backend to generate the target code. +2. **File Map Creation:** Produces a map from file names to their contents, representing the generated code. +3. **Output Serialization:** Outputs the file map and additional information (e.g., errors) as JSON to `stderr`. + +### Communication Protocol + +The engine communicates asynchronously with the frontend using a protocol defined in `hax_types::engine_api::protocol`. This communication includes: + +- **Diagnostic Data:** Sending error messages, warnings, and other diagnostics. +- **Profiling Information:** Providing performance metrics and profiling data. +- **Pretty-Printing Requests:** Requesting formatted versions of Rust source code or diagnostics for better readability. + diff --git a/book/src/contributing/structure.md b/book/src/contributing/structure.md deleted file mode 100644 index e69de29bb..000000000 From 04d7599c41668f1c2a7c593a1628c0e9fa4b8901 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 15:38:29 +0100 Subject: [PATCH 02/10] Update book/src/contributing/architecture.md Co-authored-by: Franziskus Kiefer --- book/src/contributing/architecture.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index d6fcab013..946a4976b 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -11,7 +11,7 @@ The frontend is responsible for extracting and exporting Rust code's abstract sy ### `hax-frontend-exporter` Library -This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes IDs indirections. +This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections. **`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. From 55b17d9b5540b495014d61fbfe174e7b357b2dc0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 16:00:44 +0100 Subject: [PATCH 03/10] feat(book): architecture: add links --- book/src/contributing/architecture.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 946a4976b..083f2c113 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -9,11 +9,11 @@ Hax is a software pipeline designed to transform Rust code into various formal v The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). -### `hax-frontend-exporter` Library +### [`hax-frontend-exporter` Library](https://hacspec.org/hax/frontend/hax_frontend_exporter/index.html) This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections. -**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the `SInto` trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. +**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the [`SInto`](https://hacspec.org/hax/frontend/hax_frontend_exporter/trait.SInto.html) trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process. ### `hax-driver` Binary @@ -37,20 +37,20 @@ This library mirrors the internal types of the Rust compiler (`rustc`) that cons 6. **Interactive Communication:** Engages in interactive communication with the engine. 7. **User Reporting:** Outputs results and diagnostics to the user. -## The Engine (OCaml) +## The Engine (OCaml - [documentation](https://hacspec.org/hax/engine/hax-engine/index.html)) The engine processes the transformed ASTs and options provided via JSON input from `stdin`. It performs several key functions to convert the hax-ified Rust code into the target backend language. ### Importing and Simplifying ASTs -- **AST Importation:** Imports the hax-ified Rust THIR AST. -- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. +- **AST Importation:** Imports the hax-ified Rust THIR AST. This is module [`Import_thir`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Import_thir/index.html). +- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. This is mostly the functor [`Ast.Make`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Ast/Make/index.html). ### Internal AST and Features The internal AST is defined using a **functor** that takes a list of type-level booleans, referred to as **features**, and produces the AST types accordingly. -Features are for instances, mutation, loops, unsafe code. A full list is available in `engine/lib/features.ml`. +Features are for instances, mutation, loops, unsafe code. The enumeration [`Features.Enumeration`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html) lists all those features. **Feature Witnesses:** @@ -76,7 +76,7 @@ After completing the transformation phases: ### Communication Protocol -The engine communicates asynchronously with the frontend using a protocol defined in `hax_types::engine_api::protocol`. This communication includes: +The engine communicates asynchronously with the frontend using a protocol defined in [`hax_types::engine_api::protocol`](https://hacspec.org/hax/frontend/hax_types/engine_api/protocol/index.html). This communication includes: - **Diagnostic Data:** Sending error messages, warnings, and other diagnostics. - **Profiling Information:** Providing performance metrics and profiling data. From fd4aefa4ab6d595d968dcc2ab48bf3f3f2d1e8ff Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 27 Nov 2024 16:02:35 +0100 Subject: [PATCH 04/10] book: simpliify paragraph, drop bullet poitns --- book/src/contributing/architecture.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 083f2c113..2fb766a27 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -52,10 +52,7 @@ The internal AST is defined using a **functor** that takes a list of type-level Features are for instances, mutation, loops, unsafe code. The enumeration [`Features.Enumeration`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html) lists all those features. -**Feature Witnesses:** - -- On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. -- **Example:** In the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. +**Feature Witnesses:** On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. For example, in the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported. ### Transformation Phases From afff4b381b6454b5d53521d4c03729ac007dd8c7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 28 Nov 2024 08:11:40 +0100 Subject: [PATCH 05/10] book(architecture): describe the relation between the frontend & engine in the intro --- book/src/contributing/architecture.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index 2fb766a27..fef0fb45f 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -5,6 +5,8 @@ Hax is a software pipeline designed to transform Rust code into various formal v 1. **The Frontend** (written in Rust) 2. **The Engine** (written in OCaml) +The frontend hooks into the Rust compiler, producing a abstract syntax tree for a given crate. The engine then takes this AST in input, applies various transformation, to reach in the end the language of the backend: F*, Coq... + ## The Frontend (Rust) The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools). From 65c586f64523d345a1eeeb77fad1e3bef02fa4e9 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 28 Nov 2024 08:50:11 +0100 Subject: [PATCH 06/10] doc(book): add more links --- book/src/contributing/architecture.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md index fef0fb45f..4877c97fd 100644 --- a/book/src/contributing/architecture.md +++ b/book/src/contributing/architecture.md @@ -63,7 +63,7 @@ The engine executes a sequence of **phases**, which are determined based on the 1. **Input:** Takes a list of items from an AST with specific feature constraints. 2. **Output:** Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes. -The phases can be found in the `engin/lib/phases/` folder. +The phases can be found in the [`Phases`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html) module. ### Backend Code Generation From 7d544d67eb2ebd2dd06d4cf84b97a8ce949a9856 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 7 Oct 2024 17:16:03 +0200 Subject: [PATCH 07/10] doc: release procedure --- Cargo.toml | 4 ++++ PUBLISHING.md | 28 +++++++++++++++++++--------- cli/subcommands/Cargo.toml | 3 +++ engine/names/Cargo.toml | 3 +++ engine/names/extract/Cargo.toml | 3 +++ hax-lib-protocol-macros/Cargo.toml | 3 +++ hax-lib-protocol/Cargo.toml | 3 +++ test-harness/Cargo.toml | 3 +++ 8 files changed, 41 insertions(+), 9 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 52243d79a..fe664a8ba 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -79,3 +79,7 @@ hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-alpha. hax-lib = { path = "hax-lib", version = "=0.1.0-alpha.1" } hax-engine-names = { path = "engine/names", version = "=0.1.0-alpha.1" } hax-types = { path = "hax-types", version = "=0.1.0-alpha.1" } + +[workspace.metadata.release] +owners = ["github:hacspec:crates"] + diff --git a/PUBLISHING.md b/PUBLISHING.md index ae1491466..779884788 100644 --- a/PUBLISHING.md +++ b/PUBLISHING.md @@ -1,4 +1,11 @@ -# Crates publishing +# Publishing + +## OCaml + +There is only the package `hax-engine`, that includes a binary and a +number of libraries. + +## Rust This repository is divided into several crates, some to be published, some not. All crates should start with the `hax-` prefix, but @@ -9,7 +16,7 @@ and `examples`): - `hax-test-harness` **(doesn't need to be published)** -## cargo-hax +### cargo-hax 1. `hax-frontend-exporter-options` (`frontend/exporter/options `) 2. `hax-adt-into` (`frontend/exporter/adt-into`) @@ -20,23 +27,26 @@ and `examples`): - `hax-export-json-schemas` - `hax-pretty-print-diagnostics` -- `hax-phase-debug-webapp` - `hax-driver` +### hax-lib -## hax-lib +We publish the following crates that are helper libraries to be used +for hax code: 1. `hax-lib-macros-types` 2. `hax-lib-macros` 3. `hax-lib` ---- - -- `hax-lint` - -## Supporting crates for the engine +### Supporting crates for the engine The crate listed below are used only by the OCaml build of the engine. Those should not be published on `crate.io`. 1. `cargo-hax-engine-names` 2. `cargo-hax-engine-names-extract` + +## Procedure + 1. Bump the version number with `cargo release LEVEL --no-publish --execute` (`cargo release --help` for more details on `LEVEL`). This will bump the version of every Rust crate, but also the version in `engine/dune-project`. This will also regenerate `engine/hax-engine.opam`. Note this will *not* publish the crate. + 2. PR the change + 3. when the PR is merged in main, checkout `main` and run `cargo release --execute` + diff --git a/cli/subcommands/Cargo.toml b/cli/subcommands/Cargo.toml index 91512f584..9ba434912 100644 --- a/cli/subcommands/Cargo.toml +++ b/cli/subcommands/Cargo.toml @@ -54,6 +54,9 @@ hax-lib-macros-types = {workspace = true, features = ["schemars"]} version_check = "0.9" toml = "0.8" +[package.metadata.release] +pre-release-hook = ["dune", "build", "--root", "../../engine", "hax-engine.opam"] + [[package.metadata.release.pre-release-replacements]] file = "../../engine/dune-project" search = "version [a-z0-9\\.-]+" diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml index efc92fca6..790bde85b 100644 --- a/engine/names/Cargo.toml +++ b/engine/names/Cargo.toml @@ -12,3 +12,6 @@ description = "Dummy crate containing all the Rust names the hax engine should b [dependencies] hax-lib-protocol = {path = "../../hax-lib-protocol"} hax-lib = {path = "../../hax-lib"} + +[package.metadata.release] +release = false \ No newline at end of file diff --git a/engine/names/extract/Cargo.toml b/engine/names/extract/Cargo.toml index 22604c874..df9d97479 100644 --- a/engine/names/extract/Cargo.toml +++ b/engine/names/extract/Cargo.toml @@ -23,3 +23,6 @@ extract_names_mode = [] [lints.rust] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(feature, values("rustc"))'] } + +[package.metadata.release] +release = false \ No newline at end of file diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml index de9561465..32de7ec54 100644 --- a/hax-lib-protocol-macros/Cargo.toml +++ b/hax-lib-protocol-macros/Cargo.toml @@ -21,3 +21,6 @@ syn = { version = "2.0", features = [ "extra-traits", "parsing", ] } + +[package.metadata.release] +release = false \ No newline at end of file diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml index 0dee6ef9e..0b2dc5e28 100644 --- a/hax-lib-protocol/Cargo.toml +++ b/hax-lib-protocol/Cargo.toml @@ -10,3 +10,6 @@ readme.workspace = true [dependencies] libcrux = "0.0.2-pre.2" + +[package.metadata.release] +release = false \ No newline at end of file diff --git a/test-harness/Cargo.toml b/test-harness/Cargo.toml index e0dbfe4ca..bc32eec70 100644 --- a/test-harness/Cargo.toml +++ b/test-harness/Cargo.toml @@ -25,3 +25,6 @@ insta = {version = "1.29.0", features = ["filters", "toml"]} serde = { version = "1.0", features = ["derive"] } regex = "1" hax-types.workspace = true + +[package.metadata.release] +release = false \ No newline at end of file From 508536d42d20a4243bda82576c9c271644f95d9a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 10 Oct 2024 17:06:34 +0200 Subject: [PATCH 08/10] fix: missing newlines Co-authored-by: Franziskus Kiefer --- engine/names/Cargo.toml | 2 +- engine/names/extract/Cargo.toml | 2 +- hax-lib-protocol-macros/Cargo.toml | 2 +- hax-lib-protocol/Cargo.toml | 2 +- test-harness/Cargo.toml | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml index 790bde85b..58ebcb0d2 100644 --- a/engine/names/Cargo.toml +++ b/engine/names/Cargo.toml @@ -14,4 +14,4 @@ hax-lib-protocol = {path = "../../hax-lib-protocol"} hax-lib = {path = "../../hax-lib"} [package.metadata.release] -release = false \ No newline at end of file +release = false diff --git a/engine/names/extract/Cargo.toml b/engine/names/extract/Cargo.toml index df9d97479..ed24a9d3d 100644 --- a/engine/names/extract/Cargo.toml +++ b/engine/names/extract/Cargo.toml @@ -25,4 +25,4 @@ extract_names_mode = [] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(feature, values("rustc"))'] } [package.metadata.release] -release = false \ No newline at end of file +release = false diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml index 32de7ec54..739fd467f 100644 --- a/hax-lib-protocol-macros/Cargo.toml +++ b/hax-lib-protocol-macros/Cargo.toml @@ -23,4 +23,4 @@ syn = { version = "2.0", features = [ ] } [package.metadata.release] -release = false \ No newline at end of file +release = false diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml index 0b2dc5e28..e442033b1 100644 --- a/hax-lib-protocol/Cargo.toml +++ b/hax-lib-protocol/Cargo.toml @@ -12,4 +12,4 @@ readme.workspace = true libcrux = "0.0.2-pre.2" [package.metadata.release] -release = false \ No newline at end of file +release = false diff --git a/test-harness/Cargo.toml b/test-harness/Cargo.toml index bc32eec70..a11bb3e9d 100644 --- a/test-harness/Cargo.toml +++ b/test-harness/Cargo.toml @@ -27,4 +27,4 @@ regex = "1" hax-types.workspace = true [package.metadata.release] -release = false \ No newline at end of file +release = false From f62bff4ef97a1df03d9cba2fc5c1307613f5f8ed Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 10 Oct 2024 17:13:00 +0200 Subject: [PATCH 09/10] fix(publishing): note about opam --- PUBLISHING.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/PUBLISHING.md b/PUBLISHING.md index 779884788..cfb04a098 100644 --- a/PUBLISHING.md +++ b/PUBLISHING.md @@ -50,3 +50,8 @@ engine. Those should not be published on `crate.io`. 2. PR the change 3. when the PR is merged in main, checkout `main` and run `cargo release --execute` +Note: for now, we are not publishing to Opam. Instead, let's just advertise the following for installation: +```bash +opam pin hax-engine https://github.com/hacspec/hax.git#the-release-tag +opam install hax-engine +``` From d4698af0d2a0f375046f6f90d1e2a668163d08d3 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 2 Dec 2024 13:57:20 +0100 Subject: [PATCH 10/10] doc(publishing): clarification about the engine --- PUBLISHING.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/PUBLISHING.md b/PUBLISHING.md index cfb04a098..e671dbe78 100644 --- a/PUBLISHING.md +++ b/PUBLISHING.md @@ -5,6 +5,9 @@ There is only the package `hax-engine`, that includes a binary and a number of libraries. +We have no particular release procedure for the engine: we don't plan +on publishing it to opam. + ## Rust This repository is divided into several crates, some to be published,