Skip to content

CI: Switch HOL-Light proofs to free Github runners #1710

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mkannwischer merged 1 commit into from
May 29, 2026
Merged

CI: Switch HOL-Light proofs to free Github runners #1710

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/hol_light.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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:
Expand Down Expand Up @@ -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
Expand Down
Loading