diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml index fd9fff0..38d0b27 100644 --- a/.github/workflows/amd64-linux.yml +++ b/.github/workflows/amd64-linux.yml @@ -112,4 +112,20 @@ jobs: - name: return error run: make -C proof/ CI=1 err + # proof (using runtest) + proof-runtest: + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + - name: preprocess + run: make -j$JOBS -C src/ CI=1 preprocess-inplace + + - name: run proof + run: make -j$JOBS -C proof/ all-runtest + - name: print report + run: make -C proof/ CI=1 reporter + - name: return error + run: make -C proof/ CI=1 err + diff --git a/proof/Makefile b/proof/Makefile index cb82935..3eedd38 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -127,6 +127,12 @@ all-no-report: $(MAKE) check-extracted $(MAKE) check-all +all-runtest: CI=1 +all-runtest: + $(MAKE) distclean + $(MAKE) -C $(SRC) extract-to-easycrypt + (cd $(PROOF)/crypto_scalarmult/curve25519 && $(EASYCRYPT) runtest tests.config curve25519) + # ----------------------------------------------------------------------------- # clean rules