Skip to content

Commit

Permalink
fix(ci): remove specs tests
Browse files Browse the repository at this point in the history
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 #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
hacspec/specs#13.
  • Loading branch information
W95Psp committed May 7, 2024
1 parent 248b70b commit 9634d97
Showing 1 changed file with 0 additions and 27 deletions.
27 changes: 0 additions & 27 deletions .github/workflows/install_and_test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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' }}
Expand Down

0 comments on commit 9634d97

Please sign in to comment.