File tree Expand file tree Collapse file tree 1 file changed +16
-16
lines changed Expand file tree Collapse file tree 1 file changed +16
-16
lines changed Original file line number Diff line number Diff line change @@ -165,22 +165,22 @@ jobs:
165165 script : |
166166 autogen --update-hol-light-bytecode --dry-run
167167 # TODO: fix the interactive mode to work for both x86 and arm.
168- # hol_light_interactive_x86_64:
169- # name: HOL-Light interactive shell test
170- # runs-on: pqcp-x64
171- # needs: [ hol_light_bytecode_x86_64 ]
172- # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
173- # steps:
174- # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
175- # with:
176- # fetch-depth: 0
177- # - uses: ./.github/actions/setup-shell
178- # with:
179- # gh_token: ${{ secrets.GITHUB_TOKEN }}
180- # nix-shell: 'hol_light'
181- # script: |
182- # make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
183- # echo 'needs "proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
168+ hol_light_interactive_x86_64 :
169+ name : HOL-Light interactive shell test
170+ runs-on : pqcp-x64
171+ needs : [ hol_light_bytecode_x86_64 ]
172+ if : github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
173+ steps :
174+ - uses : actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
175+ with :
176+ fetch-depth : 0
177+ - uses : ./.github/actions/setup-shell
178+ with :
179+ gh_token : ${{ secrets.GITHUB_TOKEN }}
180+ nix-shell : ' hol_light'
181+ script : |
182+ make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
183+ echo 'needs "proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
184184 hol_light_proofs_x86_64 :
185185 needs : [ hol_light_bytecode_x86_64 ]
186186 strategy :
You can’t perform that action at this time.
0 commit comments