Skip to content

Commit

Permalink
feat(ci/hax): make sure snapshots are up-to-date separately
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Feb 5, 2024
1 parent 47eaa39 commit fdbe548
Showing 1 changed file with 8 additions and 6 deletions.
14 changes: 8 additions & 6 deletions .github/workflows/hax.yml
Original file line number Diff line number Diff line change
Expand Up @@ -62,25 +62,27 @@ jobs:
sudo apt-get install --yes nodejs
./setup.sh
- name: πŸƒ Make sure the extracted Kyber snapshot is up-to-date
- name: πŸƒ Extract the Kyber reference code
run: |
eval $(opam env)
(cd proofs/fstar/extraction/ && ./clean.sh)
rm -f sys/platform/proofs/fstar/extraction/*.fst*
./hax-driver.py --kyber-reference
git diff --exit-code
- name: πŸƒ Extract and verify the Kyber reference code
- name: πŸƒ Regenerate `extraction-*` folders
run: ./proofs/fstar/patches.sh apply

- name: πŸƒ Make sure snapshots are up-to-date
run: git diff --exit-code

- name: πŸƒ Verify the Kyber reference 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" \
./hax-driver.py --verify-extraction
- name: πŸƒ Regenerate `extraction-*` folders
run: ./proofs/fstar/patches.sh apply

- name: πŸƒ Verify Kyber `extraction-edited` F* code
run: |
env FSTAR_HOME=${{ github.workspace }}/fstar \
Expand Down

0 comments on commit fdbe548

Please sign in to comment.