From 3f6c9539d1b7528a98b3d4a83b56e37656bda424 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Fri, 29 May 2026 09:49:41 +0800 Subject: [PATCH] CI: Switch HOL-Light proofs to free Github runners Our Github runner costs have been through the roof recently due to the HOL-Light proofs. This commit switches those proofs to the free Github runners. Signed-off-by: Matthias J. Kannwischer --- .github/workflows/hol_light.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/hol_light.yml b/.github/workflows/hol_light.yml index 6c0ed93c1..d8e6add86 100644 --- a/.github/workflows/hol_light.yml +++ b/.github/workflows/hol_light.yml @@ -48,7 +48,7 @@ jobs: # if the byte code needs updating. hol_light_bytecode: name: AArch64 HOL-Light bytecode check - runs-on: pqcp-arm64 + runs-on: ubuntu-24.04-arm if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -62,7 +62,7 @@ jobs: autogen --update-hol-light-bytecode --dry-run hol_light_interactive: name: AArch64 HOL-Light interactive shell test - runs-on: pqcp-arm64 + runs-on: ubuntu-24.04-arm needs: [ hol_light_bytecode ] if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: @@ -124,7 +124,7 @@ jobs: - name: rej_uniform_aarch64_asm needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_table.ml"] name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S - runs-on: pqcp-arm64 + runs-on: ubuntu-24.04-arm if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -166,7 +166,7 @@ jobs: # x86_64 proofs hol_light_bytecode_x86_64: name: x86_64 HOL-Light bytecode check - runs-on: pqcp-x64 + runs-on: ubuntu-latest if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -180,7 +180,7 @@ jobs: autogen --update-hol-light-bytecode --dry-run hol_light_interactive_x86_64: name: x86_64 HOL-Light interactive shell test - runs-on: pqcp-x64 + runs-on: ubuntu-latest needs: [ hol_light_bytecode_x86_64 ] if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: @@ -222,7 +222,7 @@ jobs: - name: keccak_f1600_x4_avx2_asm needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"] name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S - runs-on: pqcp-x64 + runs-on: ubuntu-latest if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2