Merge branch 'main' into new-sandwich-core-changes

.github/workflows/gh_pages.yml

@@ -6,24 +6,23 @@ on:
     branches: [main]
 
 jobs:
-  build-documentation:
+  # Build job
+  build:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
-    - uses: DeterminateSystems/nix-installer-action@main
-    - uses: DeterminateSystems/magic-nix-cache-action@main
-    - name: Build docs
-      run: nix build .#hax.docs --out-link ./_site
-    - name: Upload Pages artifact
-      uses: actions/upload-pages-artifact@v2
-
-  # deploys the result of `build`
-  # this job is a copy paste from <https://github.com/actions/deploy-pages>
-  deploy-documentation:
-    # Add a dependency to the build job
-    needs: build-documentation
-
-    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+      - uses: actions/checkout@v4
+      - uses: DeterminateSystems/nix-installer-action@main
+      - uses: DeterminateSystems/magic-nix-cache-action@main
+      - name: Build documentation
+        run: nix build .#docs
+      - name: Upload static files as artifact
+        id: deployment
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: result/
+  # Deploy job
+  deploy:
+    needs: build
     permissions:
       pages: write      # to deploy to Pages
       id-token: write   # to verify the deployment originates from an appropriate source
@@ -38,75 +37,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v2 # or the latest "vX.X.X" version tag for this action
-
-  # Builds and deploy "external" GH pages: pushes to the repos
-  # `hacspec/hacspec.github.io` and `hacspec/book`
-  build-and-deploy-external-gh-pages:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        path: hax
-    - uses: actions/checkout@v4
-      with:
-        repository: "hacspec/hacspec.github.io"
-        path: hacspec.github.io
-        token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
-    - uses: actions/checkout@v4
-      with:
-        repository: "hacspec/book"
-        path: book
-        token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
-
-    - uses: DeterminateSystems/nix-installer-action@main
-
-    - name: Configure git
-      run: |
-        git config --global user.name "github-actions[bot]"
-        git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com"
-
-    - name: Patch and push `README.md` in `hacspec.github.io`
-      run: |
-        (
-          README_ORIGINAL="https://github.com/hacspec/hax/blob/main/README.md"
-          echo "<!-- WARNING: a GitHub action periodically replaces this file with ${README_ORIGINAL}. Do not make any modification to this file, instead make a PR to ${README_ORIGINAL} -->"
-          echo ""
-          cat hax/README.md
-        ) > hacspec.github.io/README.md
-        cd hacspec.github.io
-
-        # Replace the `🌐 Website` link to a GitHub link
-        sed -i 's#.*🌐 Website.*#  <a href="https://github.com/hacspec/hax">🔗 GitHub</a> |#' README.md
-
-        # Replace relative links to absolute links
-        sed -i 's|(\./|(https://github.com/hacspec/hax/tree/main/|g' README.md
-
-        git add -A
-        if git commit -m "Readme update"; then
-          git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/hacspec.github.io
-        fi
-
-    - name: Regenerate and push the book
-      run: |
-        nix build ./hax#hax-book -o result-hax-book
-        HAX_COMMIT=$(git -C ./hax rev-parse --short HEAD)
-
-        mkdir hax-book
-        rsync -rq --no-perms --chown=$(id -un):$(id -gn) "$(realpath result-hax-book)/" hax-book
-        mv book/.git hax-book/.git
-        cd hax-book
-
-        {
-          echo "# Warning: this repository only contains generated files"
-          echo "The sources of the book are in https://github.com/hacspec/hax/tree/main/book"
-          echo "Please file issues, and push PRs to https://github.com/hacspec/hax."
-        } > README.md
-
-        git add -A
-        if git commit -m "Book update (generated from hacspec/hax@$HAX_COMMIT)"; then
-          git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/book
-        fi
-      env:
-        PUSH_HACSPEC_GITHUB_TOKEN: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
-        USERNAME: github-actions[bot]
+        uses: actions/deploy-pages@v4 # or specific "vX.X.X" version tag for this action

.github/workflows/mlkem.yml

@@ -33,7 +33,7 @@ jobs:
           nix profile install ./hax
 
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.01.13
+        run: nix profile install github:FStarLang/FStar/v2024.12.03
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4

.github/workflows/stale.yml

@@ -1,7 +1,7 @@
 name: 'Triage stale issues and PRs'
 on:
   schedule:
-    - cron: '00 1 * * *'
+    - cron: '00 00 * * 4'
   workflow_dispatch:
 
 jobs:

.github/workflows/test_installs.yml

@@ -22,7 +22,7 @@ jobs:
           - ubuntu-latest
           - ubuntu-20.04
           - macos-latest
-          - macos-12
+          - macos-13
     runs-on: ${{ matrix.os }}
     steps:
     - uses: actions/checkout@v3

CHANGELOG.md

@@ -0,0 +1,11 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
+and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
+
+## [Unreleased]
+
+## 0.4.0 (2024-01-20)
+ - Initial release

CONTRIBUTING.md

@@ -50,6 +50,12 @@ window of 2 days, otherwise the PR will be reverted.
  - Try to avoid exceptions, if possible.
  - Never use `==`, which is the physical equality, and almost never what you want.
 
+### Changelog
+Our changelog format is based on https://keepachangelog.com/.
+Please add an entry in a subsection (`Added`, `Changed`, `Deprecated`, `Removed`, `Fixed` -- see https://keepachangelog.com/en/1.0.0/#how) for each notable change.
+
+Please prefix with `engine:`, `frontend:` or similar.
+
 ## Styleguides
 
 ### Git Commit Messages

Cargo.toml

@@ -32,7 +32,7 @@ default-members = [
 resolver = "2"
 
 [workspace.package]
-version = "0.1.0-rc.1"
+version = "0.1.0"
 authors = ["hax Authors"]
 license = "Apache-2.0"
 homepage = "https://github.com/hacspec/hax"
@@ -71,14 +71,14 @@ colored = "2"
 annotate-snippets = "0.11"
 
 # Crates in this repository
-hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-rc.1", default-features = false }
-hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-rc.1" }
-hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-rc.1" }
-hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-rc.1" }
-hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-rc.1" }
-hax-lib = { path = "hax-lib", version = "=0.1.0-rc.1" }
-hax-engine-names = { path = "engine/names", version = "=0.1.0-rc.1" }
-hax-types = { path = "hax-types", version = "=0.1.0-rc.1" }
+hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0", default-features = false }
+hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0" }
+hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0" }
+hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0" }
+hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0" }
+hax-lib = { path = "hax-lib", version = "=0.1.0" }
+hax-engine-names = { path = "engine/names", version = "=0.1.0" }
+hax-types = { path = "hax-types", version = "=0.1.0" }
 
 [workspace.metadata.release]
-owners = ["github:hacspec:crates"]
+owners = ["github:hacspec:crates"]

PUBLISHING.md

@@ -49,12 +49,19 @@ engine. Those should not be published on `crate.io`.
 2. `cargo-hax-engine-names-extract`
 
 ## Procedure
- 1. Bump the version number with `cargo release LEVEL --no-publish --no-tag --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`
+ 1. Move the contents of `CHANGELOG.md` under the `[Unreleased]` section to a new section named following the target version
+ 2. Bump the version number with `cargo release LEVEL --no-publish --no-tag --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.
+ 3. PR the change
+ 4. 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
 ```
+
+## Notes
+`cargo release` reads the `Cargo.toml` of each crates of the workspace.
+Some creates are excluded from releasing: in their `Cargo.toml` manifest, they have `package.metadata.release.release` set to `false`.
+
+Also, `cli/subcommands/Cargo.toml` specifies pre-release replacements for the engine: the version of the engine is bumped automatically by `cargo release`.