Merge branch 'main' into jonas/proverif-rename

.github/workflows/gh_pages.yml

@@ -1,12 +1,12 @@
-name: Deploy documentation to GH Pages
+name: Deploy to GH Pages
 
 on:
   workflow_dispatch:
   push:
     branches: [main]
 
 jobs:
-  build:
+  build-documentation:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v3
@@ -19,9 +19,9 @@ jobs:
 
   # deploys the result of `build`
   # this job is a copy paste from <https://github.com/actions/deploy-pages>
-  deploy:
+  deploy-documentation:
     # Add a dependency to the build job
-    needs: build
+    needs: build-documentation
 
     # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
     permissions:
@@ -39,3 +39,74 @@ jobs:
       - 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:[email protected]/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:[email protected]/hacspec/book
+        fi
+      env:
+        PUSH_HACSPEC_GITHUB_TOKEN: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}}
+        USERNAME: github-actions[bot]

.github/workflows/install_and_test.yml

@@ -14,6 +14,10 @@ jobs:
     steps:
     - uses: actions/checkout@v3
     - uses: DeterminateSystems/nix-installer-action@main
+    - uses: cachix/cachix-action@v15
+      with:
+        name: hax
+        skipPush: true
     - uses: DeterminateSystems/magic-nix-cache-action@main
     - name: Build
       run: nix build -L
@@ -47,7 +51,6 @@ jobs:
       env:
         CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
       run: |
-        nix profile install nixpkgs#cachix nixpkgs#jq
         nix build .# .#fstar --json \
           | jq -r '.[].outputs | to_entries[].value' \
           | cachix push hax

.github/workflows/kyber.yml → .github/workflows/mlkem.yml

@@ -1,4 +1,4 @@
-name: Extract and TC Kyber
+name: Extract and TC ML-Kem
 
 on:
   pull_request:
@@ -11,7 +11,7 @@ env:
   CARGO_TERM_COLOR: always
 
 jobs:
-  hax:
+  extract-mlkem:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
     runs-on: "ubuntu-latest"
 

.github/workflows/stale.yml

@@ -0,0 +1,22 @@
+name: 'Triage stale issues and PRs'
+on:
+  schedule:
+    - cron: '00 1 * * *'
+  workflow_dispatch:
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/stale@v9
+        with:
+          stale-issue-message: "This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days."
+          stale-pr-message: "This PR has been marked as stale due to a lack of activity for 60 days. If you believe this pull request is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days."
+          stale-issue-label: 'stale'
+          exempt-issue-labels: 'keep-open'
+          stale-pr-label: 'stale'
+          exempt-pr-labels: 'keep-open'
+          days-before-stale: 60
+          days-before-close: 7
+          close-issue-message: "This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment."
+          close-pr-message: "This PR has been closed due to a lack of activity since being marked as stale. If you believe this pull request is still relevant, please reopen it with an update or comment."

.github/workflows/test.yml

@@ -30,6 +30,9 @@ jobs:
       - name: Test
         run: cargo test --workspace --exclude hax-engine-names-extract --verbose
 
+      - name: Test `hax-frontend-exporter` with feature `rustc` off
+        run: cargo check -p hax-frontend-exporter --no-default-features --verbose
+
   no-std-lib:
     runs-on: ubuntu-latest
     steps:

.github/workflows/test_installs.yml

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

.utils/list-names.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+function pager() {
+    if command -v bat &> /dev/null; then
+        bat -l ml
+    else
+        less
+    fi
+}
+
+hax-engine-names-extract | sed '/include .val/,$d' | pager

.utils/rebuild.sh

@@ -23,7 +23,7 @@ YELLOW=43
 GREEN=42
 RED=41
 BLACK=40
-status () { echo -e "\e[1m[rebuild script] \e[30m\e[$1m$2\e[0m"; }
+status () { echo -e "\033[1m[rebuild script] \033[30m\033[$1m$2\033[0m"; }
 
 cd_rootwise () {
     cd $(git rev-parse --show-toplevel)/$1