fix(ci): drop invalid timeout-minutes from reusable-workflow calls (p… #678
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: MPL-2.0 | ||
| # Architecture Enforcement: Idris2 ONLY for logic, Zig for FFI, bindings for wrappers | ||
| name: Architecture Enforcement | ||
| env: | ||
| FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true | ||
| on: | ||
| pull_request: | ||
| push: | ||
| branches: [main, develop] | ||
| permissions: | ||
| contents: read | ||
| # Cancel superseded runs on the same ref so a rapid sequence of pushes | ||
| # to a feature branch does not pile up jobs against the Pro-plan 40-job | ||
| # concurrent ceiling. Each new push to a ref supersedes its predecessor. | ||
| concurrency: | ||
| group: ${{ github.workflow }}-${{ github.ref }} | ||
| cancel-in-progress: true | ||
| jobs: | ||
| enforce-idris-only: | ||
| runs-on: ubuntu-latest | ||
| # Fast grep checks; if this exceeds 5 minutes something is wrong. | ||
| timeout-minutes: 5 | ||
| steps: | ||
| - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 | ||
| - name: Block unsafe patterns in Rust safe_*.rs wrappers | ||
| run: | | ||
| # safe_*.rs files are legitimate FFI wrappers around Proven.Safe.* | ||
| # Idris modules (see bindings/rust/README.md). The filename itself | ||
| # is not the violation; the violation is reimplemented logic, which | ||
| # surfaces as panic-prone Rust idioms in the wrapper body. | ||
| # | ||
| # This step asserts the body-shape rule from ADR-008: wrappers may | ||
| # only call FFI / compose other safe wrappers, never panic. | ||
| shopt -s nullglob | ||
| violations=0 | ||
| for f in bindings/rust/src/safe_*.rs; do | ||
| if grep -nE '\.unwrap\(\)|\.expect\(|panic!\(|unreachable!\(|todo!\(|unimplemented!\(' "$f"; then | ||
| echo "❌ $f contains panic-prone idioms forbidden in FFI wrappers" | ||
| violations=$((violations + 1)) | ||
| fi | ||
| done | ||
| if [ "$violations" -gt 0 ]; then | ||
| echo "" | ||
| echo "SOLUTION: FFI wrappers must propagate errors, not panic." | ||
| echo "Logic that needs unwrap/expect/panic belongs in src/Proven/*.idr," | ||
| echo "with the binding returning the Result via FFI." | ||
| exit 1 | ||
| fi | ||
| echo "✅ Rust safe_*.rs wrappers contain no panic-prone idioms" | ||
| - name: Block non-FFI Zig code | ||
| run: | | ||
| # Zig is allowed in three places only: | ||
| # 1. ffi/zig/ — the FFI bridge layer | ||
| # 2. bindings/zig/ — the Zig language binding (necessarily Zig) | ||
| # 3. bindings/ephapax/ — the ephapax FFI bridge (Zig adapter layer) | ||
| # Anywhere else under bindings/*/src is a violation. | ||
| STRAY=$(find bindings/*/src -name "*.zig" -type f 2>/dev/null \ | ||
| | grep -vE '^bindings/(zig|ephapax)/' \ | ||
| || true) | ||
| if [ -n "$STRAY" ]; then | ||
| echo "❌ ERROR: Zig files found outside ffi/zig/, bindings/zig/, bindings/ephapax/" | ||
| echo "Zig is restricted to the FFI bridge, the Zig binding, and the ephapax adapter." | ||
| echo "$STRAY" | ||
| exit 1 | ||
| fi | ||
| echo "✅ Zig code correctly limited to ffi/zig/, bindings/zig/, bindings/ephapax/" | ||
| - name: Verify Idris modules exist for claimed features | ||
| run: | | ||
| # Check that bindings don't claim features without Idris backing | ||
| # This is a placeholder - actual check would parse binding manifests | ||
| echo "✅ Idris module verification (manual review required)" | ||
| - name: Block unwrap/getExn/panic in bindings | ||
| run: | | ||
| # Scan all language bindings for unsafe patterns | ||
| echo "Scanning for unsafe patterns in bindings..." | ||
| # Rust: unwrap, expect, panic | ||
| if grep -r "\.unwrap()" bindings/rust/src/ 2>/dev/null | grep -v "/tests/"; then | ||
| echo "❌ Found unwrap() in Rust bindings (outside tests)" | ||
| exit 1 | ||
| fi | ||
| # AffineScript: previously this checked bindings/rescript/src/ for | ||
| # ReScript-specific panic idioms (getExn, Obj.magic). ReScript was | ||
| # banned 2026-04-30 (estate-wide migration to AffineScript) and | ||
| # the binding was ported to bindings/affinescript/src/ with .afs | ||
| # files using the Zig FFI directly (no JS-FFI ReScript scaffolding). | ||
| # The remaining panic-prone-pattern catches are handled by the | ||
| # cross-binding "No panic-prone patterns in bindings" step in | ||
| # e2e.yml (Aspect — Safety Invariants). | ||
| echo "✅ No unsafe patterns found in bindings" | ||
| # The legacy `hypatia-scan` job that bootstrapped its own checkout of | ||
| # hyperpolymath/hypatia and built the Elixir scanner has been removed — | ||
| # see `.github/workflows/hypatia-scan.yml`, which is the canonical wrapper | ||
| # around hyperpolymath/standards's `hypatia-scan-reusable.yml`. The legacy | ||
| # job broke after hypatia's `elixir-scanner/` directory was relocated, and | ||
| # maintaining two parallel scanner invocations created drift; the reusable | ||
| # is the single source of truth. | ||
| verify-idris-build: | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 15 | ||
| # Docker pull (snazzybucket/idris2) + Idris2 totality check across all | ||
| # Proven.Safe.* modules. Local oracle runs in ~8 minutes; 20-minute | ||
| # budget covers cold cache and the occasional Docker Hub slowdown. | ||
| timeout-minutes: 20 | ||
| steps: | ||
| - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 | ||
| - name: Build Idris2 modules (via container) | ||
| run: | | ||
| # Use the snazzybucket/idris2 container so we don't pay a 10-minute | ||
| # bootstrap on every job. The container is the same one used locally | ||
| # to verify proven#9 before merge. | ||
| docker run --rm \ | ||
| -v "$PWD:/proj" \ | ||
| -w /proj \ | ||
| snazzybucket/idris2:latest \ | ||
| sh -c 'idris2 --build proven.ipkg' || { | ||
| echo "❌ Idris2 build failed - proofs are broken" | ||
| exit 1 | ||
| } | ||
| echo "✅ Idris2 modules build successfully with totality checking" | ||
