fix(ci): audit-gates External-prover installs coq, not non-existent r… #1111

Workflow file for this run

	name: CI

	on:
	push:
	branches: [main]
	pull_request:
	branches: [main]

	env:
	CARGO_TERM_COLOR: always
	CARGO_INCREMENTAL: "0"
	RUST_BACKTRACE: "1"
	# rust-toolchain.toml pins nightly; honour it in CI.

	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: true

	jobs:
	# ---------------------------------------------------------------------------
	# Job 0: Verum-syntax gate. Pure Python, no build — the fastest merge blocker.
	# grammar/verum.ebnf knows only `.` for paths; `::` is a Rust porting artefact
	# the parser only tolerates as error-recovery. This keeps it out of .vr sources
	# (IPv6 / SQL-cast / URI / script DATA excluded). See the script's header.
	# ---------------------------------------------------------------------------
	vr-syntax:
	name: Verum syntax gate (no Rust `::`, op-byte doc truth)
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- name: No Rust-style `::` in .vr sources
	run: python3 vcs/scripts/check_no_double_colon.py --check
	# instruction.rs is the single source of truth for VBC op bytes; a .vr
	# doc comment that contradicts it is worse than no comment, because the
	# next author writes code against it (T0193 shipped a `3 = log` claim
	# where the enum says 4). Re-derives the enums on every run.
	- name: .vr op-byte doc comments match the instruction.rs enums
	run: python3 vcs/scripts/check_op_byte_docs.py --check

	# ---------------------------------------------------------------------------
	# Job 1: compile + unit tests on Linux (x86_64 + aarch64) and macOS.
	# Linux-arm64 matters because aarch64 uses a different kernel syscall
	# table from x86_64 — see sys/linux/arch.vr. Blocks merge.
	# ---------------------------------------------------------------------------
	unit:
	name: Unit tests (${{ matrix.os }})
	runs-on: ${{ matrix.os }}
	strategy:
	fail-fast: false
	matrix:
	os: [ubuntu-latest, ubuntu-24.04-arm, macos-14]
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain (pinned via rust-toolchain.toml)
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly
	components: rustfmt, clippy, rust-src

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: unit-${{ matrix.os }}
	cache-on-failure: true

	- name: Build workspace (rustc -D warnings, blocking)
	env:
	RUSTFLAGS: "-D warnings"
	run: cargo build --workspace --locked

	- name: Run unit tests (library + binaries)
	run: cargo test --workspace --lib --bins --locked

	# ---------------------------------------------------------------------------
	# Job 2: VCS L0 (2,963 specs, 100%) + L1 (499 specs, 100%). Blocks merge.
	# ---------------------------------------------------------------------------
	vcs-l0-l1:
	name: VCS L0 + L1 (100% gate)
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: vcs-runner

	- name: Build vtest runner
	run: cargo build -p vtest --release --locked

	- name: Run L0-critical (100% required)
	working-directory: vcs
	run: make test-l0 PARALLEL=4

	- name: Run L1-core (100% required)
	working-directory: vcs
	run: make test-l1 PARALLEL=4

	- name: Upload VCS reports
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: vcs-reports-l0-l1
	path: vcs/reports/

	# ---------------------------------------------------------------------------
	# Job 3: Differential (interpreter vs AOT, 204+ specs). Blocks merge.
	# ---------------------------------------------------------------------------
	differential:
	name: Differential (Tier 0 vs Tier 3)
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: vcs-runner

	- name: Build vtest runner + verum CLI
	run: cargo build -p vtest -p verum_cli --release --locked

	- name: Run differential specs
	working-directory: vcs
	run: make test-differential PARALLEL=4

	- name: Upload differential reports
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: vcs-reports-differential
	path: vcs/reports/

	# ---------------------------------------------------------------------------
	# Job 3b: STRICT-gate baseline (#45). AOT-compiles a stdlib-heavy smoke
	# program with VERUM_STRICT_MONO + VERUM_STRICT_SIGNATURES so the two
	# silent-degradation classes (mono fallback-to-unspecialized, arity-
	# collision / skip-body forward declarations) are VISIBLE in CI on every
	# push. Advisory (continue-on-error) until the drift backlog is zero —
	# then remove `continue-on-error` to make it blocking, same lifecycle as
	# the lint job below.
	# ---------------------------------------------------------------------------
	strict-gates:
	name: STRICT gates (mono + signatures, advisory)
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: vcs-runner

	- name: Build verum CLI
	run: cargo build -p verum_cli --release --locked

	- name: AOT smoke under STRICT gates
	continue-on-error: true
	env:
	VERUM_STRICT_MONO: "1"
	VERUM_STRICT_SIGNATURES: "1"
	VERUM_NO_OBJECT_CACHE: "1"
	run: \|
	cat > /tmp/strict_smoke.vr <<'EOF'
	fn main() {
	let xs: List<Int> = [3, 1, 2];
	let total = xs.iter().fold(0, fn(acc: Int, x: Int) -> Int { acc + x });
	let m: Maybe<Text> = Maybe.Some(f"total={total}");
	match m {
	Maybe.Some(s) => print(s),
	Maybe.None => print("none"),
	}
	}
	EOF
	./target/release/verum build /tmp/strict_smoke.vr

	# ---------------------------------------------------------------------------
	# Job 4: Lint + format. Both rustfmt and clippy run advisory (visible in UI,
	# non-blocking) until Phase 3 of the production-readiness push lands the
	# one-shot reformat and eliminates the warning backlog. At that point remove
	# `continue-on-error` on both steps.
	# ---------------------------------------------------------------------------
	lint:
	name: Lint & format
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly
	components: rustfmt, clippy

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: lint

	- name: rustfmt --check (advisory)
	continue-on-error: true
	run: cargo fmt --all -- --check

	- name: clippy (-D warnings, advisory)
	continue-on-error: true
	run: cargo clippy --workspace --all-targets --locked -- -D warnings

	# ---------------------------------------------------------------------------
	# Job 5: Architectural invariants (#80) — codify the no-libc and
	# target-triple discipline established under #91 perf roadmap so future
	# commits can't silently regress.
	# ---------------------------------------------------------------------------
	arch-guards:
	name: Architectural invariants (no-libc, no-host-cfg)
	runs-on: ${{ matrix.os }}
	strategy:
	fail-fast: false
	matrix:
	os: [ubuntu-latest, macos-14]
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@master
	with:
	toolchain: nightly

	- name: Fetch prebuilt LLVM
	uses: ./.github/actions/fetch-llvm

	- name: Cache cargo registry + target
	uses: Swatinem/rust-cache@v2
	with:
	shared-key: arch-guards-${{ matrix.os }}

	- name: Build verum CLI for smoke binary
	run: cargo build --bin verum --locked

	# No-host-#[cfg(target_os)] in codegen (#80).
	# Codegen MUST read module.get_triple() — never host-cfg.
	# The script enforces this; new violations block merge.
	- name: Check no host-#[cfg(target_os)] in codegen
	run: python3 scripts/ci/check_no_host_cfg.py --strict

	# No-libc dynamic linkage (#80).
	# Builds a smoke .vr program and verifies the produced binary
	# only links the platform's permitted system boundary
	# (libSystem.B.dylib on macOS; ld-linux on Linux; nothing else).
	- name: Check AOT binary doesn't link libc
	run: ./scripts/ci/check_no_libc_link.sh target/debug/verum

Navigation Menu

Uh oh!

fix(ci): audit-gates External-prover installs coq, not non-existent r… #1111

Workflow file

fix(ci): audit-gates External-prover installs coq, not non-existent r… #1111

Uh oh!

Workflow file for this run