From ce1a066a26286fc3b810bd8bdd486c0089f698bb Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 7 May 2024 08:36:54 +0200
Subject: [PATCH 1/2] fix(ci): remove `specs` tests

The https://github.com/hacspec/specs repository contains
specifications written in hacspec, mainly at the time of hacspec v1.

Since hacspec v1 is deprecated and archived, its library is deprecated
as well.

The hacspec lib (https://github.com/hacspec/hacspec/tree/master/lib)
doesn't typecheck any longer with `num-bigint` version `0.4.5`.

The hacspec lib dependents on `num-bigint` version `0.4`, not
specifying the minor version. The `specs` repository has no
`Cargo.lock`, and thus, from a clean `git clone`, `cargo build` pins
`num-bigint` to version `0.4.5`, breaking the hacspec library.

This broke https://github.com/hacspec/hax/pull/653 recently, and we
had the same kind of errors a couple times before in the past.

Two options were considered:
 - remove the tests related to the specs in the CI of hax;
 - commit a `Cargo.lock`.

The choose the first one: we need to update those specifications to
hax anyway: this will add motivation to
https://github.com/hacspec/specs/issues/13.
---
 .github/workflows/install_and_test.yml | 27 --------------------------
 1 file changed, 27 deletions(-)

diff --git a/.github/workflows/install_and_test.yml b/.github/workflows/install_and_test.yml
index 2a044548a..153175e83 100644
--- a/.github/workflows/install_and_test.yml
+++ b/.github/workflows/install_and_test.yml
@@ -41,33 +41,6 @@ jobs:
       with:
         repository: 'hacspec/specs'
         path: specs
-        
-    - name: Extract specifications
-      working-directory: specs
-      run: |
-        paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
-        for cratePath in $paths; do
-          crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml")
-          for backend in fstar coq; do
-            for skip in $SKIPLIST; do
-              if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then
-                echo "⛔ $crate [$backend] (skipping)"
-                continue 2
-              fi
-            done
-            echo "::group::$crate [$backend]"
-            cargo hax -C -p "$crate" \; into "$backend"
-            echo "::endgroup::"
-          done
-        done
-      env:
-        SKIPLIST: |
-          tls_cryptolib
-          hacspec-merlin
-          hacspec-halo2-coq
-          hacspec-halo2-fstar
-          hacspec-weierstrass-coq
-          hacspec-weierstrass-fstar
 
     - name: Push to Cachix
       if: ${{ github.event_name == 'workflow_dispatch'  || github.event_name == 'merge_group'  }}

From e8fdd4f8b9fea60c052ddf9381628bc3a78c18c8 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 7 May 2024 09:14:24 +0200
Subject: [PATCH 2/2] fix(ci): test local `chacha20`, not `specs` one

---
 .github/workflows/test_installs.yml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/test_installs.yml b/.github/workflows/test_installs.yml
index 5ed2a6640..f0de760ea 100644
--- a/.github/workflows/test_installs.yml
+++ b/.github/workflows/test_installs.yml
@@ -40,12 +40,10 @@ jobs:
         ./setup.sh
     - run: cargo hax --version
     - name: Test an extraction
-      uses: actions/checkout@v3
-      with:
-        repository: 'hacspec/specs'
-    - run: |
+      run: |
+        cd examples/chacha20
         eval $(opam env)
-        cargo hax -C -p hacspec-chacha20 \; -i '**' into fstar
+        cargo hax into fstar
   setup_sh_status:
     if: |
       always() &&