Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
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
1 change: 1 addition & 0 deletions .github/workflows/agda-meta-checker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
verify-proofs:
name: Type-check Agda proofs
runs-on: ubuntu-latest
timeout-minutes: 15
steps:
- name: Checkout
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/boj-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ concurrency:
jobs:
trigger-boj:
runs-on: ubuntu-latest
timeout-minutes: 5
steps:
- name: Checkout
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cargo-audit.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ jobs:
audit:
name: Dependency audit
runs-on: ubuntu-latest
timeout-minutes: 10

steps:
- name: Checkout repository
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cflite_batch.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ permissions:
jobs:
BatchFuzzing:
runs-on: ubuntu-latest
timeout-minutes: 45
strategy:
fail-fast: false
matrix:
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cflite_pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ permissions:
jobs:
PR:
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down
66 changes: 44 additions & 22 deletions .github/workflows/chapel-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,17 @@ concurrency:

permissions: read-all

# Pinned Chapel deb (Ubuntu 22.04 amd64; installs cleanly on the
# ubuntu24 runner). SHA-256 verified against the GitHub Releases asset;
# mismatch fails the install step. Bumped 2.3.0 -> 2.8.0 (issue #181)
# to track sibling estate repos proven (#141) and panic-attack (#85),
# both of which validated this URL+SHA combo against the same
# `ubuntu-latest` runner image we use here.
env:
CHAPEL_VERSION: '2.8.0'
CHAPEL_DEB_URL: 'https://github.com/chapel-lang/chapel/releases/download/2.8.0/chapel-2.8.0-1.ubuntu22.amd64.deb'
CHAPEL_DEB_SHA256: '944a454b8a791f344312fcd261b562871159b74f5ef41d81e11833eb21d85f60'

jobs:
# Job 1: Compile Chapel .chpl files into a static library.
#
Expand All @@ -35,30 +46,36 @@ jobs:
# compiling, the workflow fails.
#
# Why --static and not --dynamic:
# The official apt deb (chapel-2.3.0-1.ubuntu24.amd64.deb) ships only
# the CHPL_LIB_PIC=none runtime variant. Building a shared library
# requires CHPL_LIB_PIC=pic runtime objects which are not in the
# package; the linker rejects the non-PIC `libchpl.a` with
# The official apt deb (chapel-${CHAPEL_VERSION}-1.ubuntu22.amd64.deb)
# ships only the CHPL_LIB_PIC=none runtime variant. Building a shared
# library requires CHPL_LIB_PIC=pic runtime objects which are not in
# the package; the linker rejects the non-PIC `libchpl.a` with
# `relocation R_X86_64_TPOFF32 ... can not be used when making a
# shared object`. Until the CI image ships a PIC-enabled runtime
# (or we adopt a from-source Chapel build), the metalayer is
# (or we adopt a from-source Chapel build via the
# `chapel-pic-from-source` Justfile recipe), the metalayer is
# distributed as `libechidna_chapel.a` and the Zig FFI links it
# statically.
chapel-build:
name: Compile Chapel Metalayer
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 30
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

- name: Install Chapel
- name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
run: |
# Install Chapel from official apt repository.
# SHA256 of the deb is pinned for supply-chain integrity; bump
# alongside the version tag when upgrading.
curl -fsSL --max-time 300 \
https://github.com/chapel-lang/chapel/releases/download/2.3.0/chapel-2.3.0-1.ubuntu24.amd64.deb \
-o /tmp/chapel.deb
sudo dpkg -i /tmp/chapel.deb || sudo apt-get install -f -y
set -euo pipefail
# libunwind-dev is a runtime link-time dep for chpl-built binaries
# on the ubuntu .deb path; sibling estate repo panic-attack (#85)
# established this preinstall as the working pattern, reused by
# proven (#141). Without it the chapel-build smoke link fails with
# `error while loading shared libraries: libunwind.so.8`.
sudo apt-get update -qq
sudo apt-get install -y libunwind-dev
curl -fsSL --max-time 300 --retry 3 -o /tmp/chapel.deb "$CHAPEL_DEB_URL"
echo "$CHAPEL_DEB_SHA256 /tmp/chapel.deb" | sha256sum --check
sudo apt-get install -y /tmp/chapel.deb
chpl --version

- name: Compile Chapel proof search library (static)
Expand Down Expand Up @@ -93,7 +110,8 @@ jobs:
# `src/zig_ffi/build.zig`.
zig-ffi:
name: Build & Test Zig FFI Bridge
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 20
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

Expand Down Expand Up @@ -121,7 +139,8 @@ jobs:
# Re-enable strict gating once #133's Chapel + FFI rehabilitation lands.
rust-chapel-feature:
name: Rust Build with Chapel Feature
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 20
needs: zig-ffi
continue-on-error: true
steps:
Expand Down Expand Up @@ -159,18 +178,21 @@ jobs:
# and flip this job to strict.
rust-chapel-real:
name: Rust Build β€” Real Chapel Library (allow-fail, L2.3+ gate)
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 30
needs: [chapel-build, zig-ffi]
continue-on-error: true
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

- name: Install Chapel
- name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
run: |
curl -fsSL --max-time 300 \
https://github.com/chapel-lang/chapel/releases/download/2.3.0/chapel-2.3.0-1.ubuntu24.amd64.deb \
-o /tmp/chapel.deb
sudo dpkg -i /tmp/chapel.deb || sudo apt-get install -f -y
set -euo pipefail
sudo apt-get update -qq
sudo apt-get install -y libunwind-dev
curl -fsSL --max-time 300 --retry 3 -o /tmp/chapel.deb "$CHAPEL_DEB_URL"
echo "$CHAPEL_DEB_SHA256 /tmp/chapel.deb" | sha256sum --check
sudo apt-get install -y /tmp/chapel.deb
chpl --version

- name: Install Zig
Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/codeql.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,15 @@ jobs:
permissions:
contents: read
security-events: write
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
include:
- language: javascript-typescript
build-mode: none
- language: cpp
build-mode: none

steps:
- name: Checkout
Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/container-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ jobs:
container-build:
name: Build & verify container image
runs-on: ubuntu-latest
timeout-minutes: 90

steps:
- name: Checkout
Expand Down Expand Up @@ -110,6 +111,7 @@ jobs:
tier3-container:
name: Tier-3 / ${{ matrix.prover }}
runs-on: ubuntu-latest
timeout-minutes: 90
# Run on schedule or when the .containerization tree changes on main.
# Not a merge gate β€” these are informational weekly builds.
if: >-
Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/dogfood-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
a2ml-validate:
name: Validate A2ML manifests
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -72,6 +73,7 @@ jobs:
k9-validate:
name: Validate K9 contracts
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -121,6 +123,7 @@ jobs:
empty-lint:
name: Empty-linter (invisible characters)
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -185,6 +188,7 @@ jobs:
groove-check:
name: Groove manifest check
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -243,6 +247,7 @@ jobs:
eclexiaiser-validate:
name: Validate eclexiaiser manifest
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -312,6 +317,7 @@ jobs:
dogfood-summary:
name: Dogfooding compliance summary
runs-on: ubuntu-latest
timeout-minutes: 5
needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
if: always()

Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/formal-verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ jobs:
stable-tests:
name: Trust-pipeline invariant tests (stable)
runs-on: ubuntu-latest
timeout-minutes: 15

steps:
- name: Checkout repository
Expand All @@ -67,6 +68,7 @@ jobs:
creusot-verify:
name: Creusot formal verification
runs-on: ubuntu-latest
timeout-minutes: 15
# No continue-on-error β€” this is a hard merge gate as of Stage 8c-M3.
# The outer-loop invariant for compute is now live; all obligations
# (PO-1..P8, PO-A1..A12) must discharge under Why3+Z3.
Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/generator-generic-ossf-slsa3-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ on:
jobs:
build:
runs-on: ubuntu-latest
timeout-minutes: 10
outputs:
digests: ${{ steps.hash.outputs.digests }}

Expand Down Expand Up @@ -60,6 +61,7 @@ jobs:

provenance:
needs: [build]
timeout-minutes: 10
permissions:
actions: read # To read the workflow path.
id-token: write # To sign the provenance.
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/ghcr-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ env:
jobs:
build-and-push:
runs-on: ubuntu-latest
timeout-minutes: 10
permissions:
contents: read
packages: write
Expand Down
3 changes: 2 additions & 1 deletion .github/workflows/governance.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,5 @@ permissions:

jobs:
governance:
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@3f34549c03274ec7a74683068f03a492b0fa805f # main 2026-06-01 (R5 generic β€” standards#330; consumes .github/canonical-references/)
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613
timeout-minutes: 10
1 change: 1 addition & 0 deletions .github/workflows/hypatia-scan.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,4 +26,5 @@ permissions:
jobs:
hypatia:
uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89
timeout-minutes: 10
secrets: inherit
1 change: 1 addition & 0 deletions .github/workflows/idris2-abi-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ jobs:
idris2-typecheck:
name: Type-check Idris2 ABI definitions
runs-on: ubuntu-latest
timeout-minutes: 30
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

Expand Down
1 change: 1 addition & 0 deletions .github/workflows/instant-sync.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ permissions:
jobs:
dispatch:
runs-on: ubuntu-latest
timeout-minutes: 10
steps:
- name: Trigger Propagation
uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3
Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/live-provers.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ jobs:
name: T1 / ${{ matrix.backend }}
if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down Expand Up @@ -126,6 +127,7 @@ jobs:
name: T1 Guix manifest check
if: github.event_name != 'schedule'
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
steps:
- name: Checkout
Expand All @@ -147,6 +149,7 @@ jobs:
name: T2 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 3 * * *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '2' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down Expand Up @@ -294,6 +297,7 @@ jobs:
name: T3 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
strategy:
fail-fast: false
Expand Down Expand Up @@ -408,6 +412,7 @@ jobs:
name: T4 niche provers
if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
steps:
- name: Checkout
Expand All @@ -427,6 +432,7 @@ jobs:
name: T4 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
strategy:
fail-fast: false
Expand Down
9 changes: 9 additions & 0 deletions .github/workflows/mirror.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,19 @@ on:
branches: [main]
workflow_dispatch:

# Estate guardrail: cancel superseded runs so re-pushes / rebased PR
# updates do not pile up queued runs against the shared account-wide
# Actions concurrency pool. Applied only to read-only check workflows
# (no publish/mutation), so cancelling a superseded run is always safe.
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

permissions:
contents: read

jobs:
mirror:
uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@e6b2884722350515934d443daf23442f2195796f
timeout-minutes: 10
secrets: inherit
1 change: 1 addition & 0 deletions .github/workflows/mvp-smoke.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ jobs:
mvp-smoke:
name: MVP Smoke
runs-on: ubuntu-latest
timeout-minutes: 15
permissions:
contents: read
steps:
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/rust-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ permissions:
jobs:
rust-ci:
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@cc5a372af1af1b202c17f1b21efd954e6c038bef
timeout-minutes: 30
with:
enable_audit: true
enable_coverage: true
Loading
Loading