From 8514fc1b8fe31a422522d2e97f98912cd7ed6ac7 Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Fri, 29 May 2026 11:29:43 +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.

- Ports https://github.com/pq-code-package/mldsa-native/pull/1134

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 .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 74860405d..a065077eb 100644
--- a/.github/workflows/hol_light.yml
+++ b/.github/workflows/hol_light.yml
@@ -44,7 +44,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
@@ -58,7 +58,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:
@@ -110,7 +110,7 @@ jobs:
           - name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
             needs: ["keccak_specs.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
@@ -152,7 +152,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
@@ -166,7 +166,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:
@@ -230,7 +230,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