feat(ci): verify extraction-edited F* code

cryspen · Jan 9, 2024 · 51be769 · 51be769
1 parent 7658d96
commit 51be769
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -73,6 +73,14 @@ jobs:
               PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
               ./hax-driver.py --verify-extraction
 
+      - name: 🏃 Verify Kyber `extraction-edited` F* code
+        run: |
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              make -C proofs/fstar/extraction-edited
+
       - name: 🏃 Extract the Kyber specification
         run: |
           eval $(opam env)