Count what was proved, not what was claimed #92

Workflow file for this run

	name: CI

	# One workflow, not two. The artifact scan used to live in its own file, and a
	# guard in tests/unit/repo-guards.rs had to learn to read every file under
	# .github/workflows before it could see that a whole gate ran there: exactly the
	# failure it exists to prevent, one file over. One file is one place to look.
	on:
	push:
	# Work lands on dev, so dev needs the full lane too. The pull_request
	# trigger filters on the base branch, which a dev to main pull request
	# already matches, so it needs no entry of its own.
	branches: [main, dev]
	pull_request:
	branches: [main]

	# There is no paths-ignore, and that is deliberate. The old one skipped every
	# job on a push touching only markdown, which skipped cargo test --test unit,
	# which is the target holding documented_gate_list_covers_ci,
	# tool_router_matches_the_documented_surface and
	# incomplete_codes_match_their_documentation. So the filter turned off precisely
	# the gates that read the files being changed, and scripts/check-artifacts.sh
	# reads README.md and docs/ as well. A documentation-only push pays the full
	# lane now; that is cheaper than a documentation gate that cannot fail.

	# A push to a branch with a pull request open fires both triggers: one run on
	# the branch head, one on the merge ref, each paying a Frama-C install and a
	# fourteen minute suite. Keying on the head ref puts them in one group, so the
	# later run cancels the earlier.
	#
	# The repository is in the key as well as the branch, because the branch name
	# alone is not unique across forks: two pull requests from two forks whose
	# branches are both called "dev" shared a group, and cancel-in-progress then
	# had one contributor's checks killed by the other's push. The fallbacks are
	# what keep the pair above in one group, since a push event carries neither
	# field and answers with this repository and the bare branch, which is exactly
	# what a pull request from this repository resolves to.
	#
	# Except on main, where a run may be holding the release window below open with
	# the previous release already deleted. Cancelling that leaves no release at
	# all, so pushes to main queue rather than replace each other.
	concurrency:
	group: >-
	${{ github.workflow }}-${{ github.event.pull_request.head.repo.full_name \|\| github.repository }}-${{ github.event.pull_request.head.ref \|\| github.ref_name }}
	cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}

	# The floor, raised per job by the two that need more: the release job takes
	# contents: write to publish, and artifact-scans takes checks: write because the
	# advisory action reports by creating a check run. Nothing else writes anything.
	permissions:
	contents: read

	# Runner images are pinned to a release rather than "-latest", so an image
	# rollover is a deliberate bump in this file instead of a surprise on a Monday.
	#
	# Actions are named by major version only, "@v7" rather than "@v7.0.1" or a
	# commit. A major tag tracks its own patches, so a fix upstream arrives without
	# a commit here, and .github/dependabot.yml opens the pull request when the
	# major itself moves. Write the short form when adding one.
	#
	# Every job carries timeout-minutes. The default is 360, and the Frama-C lane
	# drives real processes over Unix sockets and can hang rather than fail, which
	# is six wasted runner hours before anyone notices.
	jobs:
	# Fast lane: builds + pure unit tests. No Frama-C needed.
	#
	# macOS is in this matrix because the build job below ships a macOS binary,
	# and a released artifact whose test suite has never run on the target is a
	# promise nobody checked. It is also where this server differs: process spawn,
	# socket paths and signal handling are all platform behavior, and
	# test-mcp-stdio already counts differently there, since
	# e_acsl_catches_a_runtime_violation skips where e-acsl-gcc cannot run.
	# Compiling for a platform is not the same as running on it.
	rust-quick:
	name: Rust unit / build (${{ matrix.os }})
	runs-on: ${{ matrix.os }}
	timeout-minutes: 30
	strategy:
	fail-fast: false
	matrix:
	os: [ubuntu-24.04, macos-15]
	steps:
	- uses: actions/checkout@v7
	with:
	persist-credentials: false

	- name: Shell formatting (shfmt, .editorconfig)
	if: runner.os == 'Linux'
	run: .ci/check-shell-formatting.sh

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@stable

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

	# Was local-only, in scripts/run-gates.sh and nowhere else, so the one
	# gate that would catch a lint regression could not fail a push. The
	# denial level lives in Cargo.toml, not in a -D here, so this command and
	# the one a person types before pushing mean the same thing.
	- name: Clippy
	run: cargo clippy --all-targets

	- name: Unit tests (no Frama-C)
	run: cargo test --test unit

	# --tests, matching the release gate in scripts/run-gates.sh. Without it
	# the test targets are never compiled in release mode here, so a release
	# only compile error in a test passes this lane and surfaces an hour
	# later in the suite that spawns the binary from disk.
	- name: Release build
	run: cargo build --release --tests

	# No toolchain and no build. Kept a separate job rather than a step of the
	# fast lane because its finding is about the documents, and a person reading a
	# red run should see which of the two it was without opening a log. The
	# advisory scan is a step here rather than a job of its own so it reuses this
	# checkout, which is also why this job is no longer only reading the tree: it
	# fetches a cargo-audit binary and queries the advisory database.
	artifact-scans:
	name: Artifact scans
	runs-on: ubuntu-24.04
	timeout-minutes: 10
	# Raised for this job alone, the way the release job raises contents. The
	# advisory action reports by creating a check run, so the workflow-wide
	# contents: read leaves it unable to publish the only thing it produces.
	permissions:
	contents: read
	checks: write
	steps:
	- uses: actions/checkout@v7
	with:
	persist-credentials: false
	- run: scripts/check-artifacts.sh

	# Not in scripts/run-gates.sh, and deliberately so. Every gate the runner
	# holds is reproducible from the commit, which is the whole reason
	# Cargo.lock is tracked; this one answers from an advisory database that
	# moves on its own, so it is the one check whose verdict is not a function
	# of the tree. There is no schedule here either, so this catches a
	# vulnerable dependency arriving rather than one discovered later; the
	# discovered-later half is what Dependabot alerts are for.
	#
	# Skipped on pull requests from forks, where GitHub caps GITHUB_TOKEN at
	# read-only whatever the permissions block says, so the action cannot
	# create the check run it reports through and fails on a clean tree. This
	# repository takes fork pull requests, so that is a real run and not a
	# hypothetical one. A dependency arriving that way is still scanned, on
	# the push that merges it.
	- name: RustSec advisories against the tracked lockfile
	if: ${{ github.event_name == 'push' \|\| github.event.pull_request.head.repo.full_name == github.repository }}
	uses: rustsec/audit-check@v2
	with:
	token: ${{ secrets.GITHUB_TOKEN }}

	# Full lane: Frama-C + WP provers + the ast-utils plugin, then the
	# integration / MCP-stdio suites that drive a real Frama-C server.
	integration:
	name: ast-utils plugin + Frama-C ${{ matrix.frama-c-version }}
	runs-on: ubuntu-24.04
	timeout-minutes: 60
	strategy:
	fail-fast: false
	matrix:
	frama-c-version: ["33.0"]
	steps:
	- uses: actions/checkout@v7
	with:
	persist-credentials: false

	- name: Install WP provers (z3, cvc5)
	timeout-minutes: 5
	run: \|
	sudo apt-get update -y
	sudo apt-get install -y z3 cvc5

	- name: Setup OCaml
	uses: ocaml/setup-ocaml@v3
	with:
	ocaml-compiler: "4.14.2"

	- name: Validate Frama-C matrix version
	run: .ci/check-frama-c-matrix-version.sh '${{ matrix.frama-c-version }}'

	# Cache the whole opam state keyed by frama-c + compiler + OS: frama-c is
	# not declared as a project dependency, so without this the ~10 min install
	# repeats every run. setup-ocaml uses a project-local switch in ./_opam
	# (OPAMROOT at ~/.opam holds global metadata + download cache), and frama-c
	# binaries land in _opam/bin, so both paths must be cached.
	- name: Cache opam state (~/.opam + _opam)
	id: cache-opam
	uses: actions/cache@v6
	with:
	path: \|
	~/.opam
	_opam
	key: ${{ runner.os }}-opam-ocaml-4.14.2-frama-c-${{ matrix.frama-c-version }}-alt-ergo-2.6.3-v2

	# alt-ergo is named explicitly because it is an OPTIONAL dependency of
	# frama-c, not a hard one. This step used to say "alt-ergo + why3 pulled
	# as deps" and install frama-c alone: why3 did come along, alt-ergo did
	# not, and "why3 config detect" then found something it could not put a
	# version on ("Prover Alt-Ergo version is not recognized"). WP ran it
	# anyway, proved 24 of 33 goals where the baseline is 33, and the corpus
	# gate reported eleven confusing count mismatches for one missing package.
	#
	# The version is pinned rather than left to the solver because
	# scripts/check-tutorial-corpus.sh keys its per-fixture proved-goal counts
	# to the prover, not to the Frama-C version, and every row in it was
	# measured under 2.6.3. Moving this means re-measuring that table.
	- name: Install Frama-C ${{ matrix.frama-c-version }} and Alt-Ergo 2.6.3
	if: steps.cache-opam.outputs.cache-hit != 'true'
	run: opam install -y frama-c.${{ matrix.frama-c-version }} alt-ergo.2.6.3

	# Unconditional, unlike the Frama-C install above. cppo is the plug-in's
	# preprocessor, it builds in seconds, and it is a no-op on a warm switch.
	# Folding it into the cached step instead would mean a new cache key, and
	# that discards a whole Frama-C switch, about ten minutes of from-source
	# build, to add a package that takes one.
	- name: Install cppo
	run: opam install -y cppo

	- name: Check installed Frama-C and Alt-Ergo versions
	run: .ci/check-installed-versions.sh '${{ matrix.frama-c-version }}'

	# why3 keeps its prover registry in ~/.why3.conf (outside ~/.opam), so this
	# must run even on a cache hit, otherwise WP finds no prover and every goal
	# comes back NORESULT.
	- name: Configure why3 (detect z3, cvc5, alt-ergo)
	run: opam exec -- why3 config detect

	# Every step below needs frama-c and the provers on PATH, and each one
	# used to prepend the switch itself. Written once here it applies to the
	# whole job, and it also stops hiding a failure: prepending inside an
	# export makes the status that of the export rather than of the command
	# substitution, so an opam that could not answer set an empty prefix and
	# the step carried on to fail somewhere less obvious. This form fails
	# where the problem is. It is the six SC2155 warnings shellcheck
	# reported, and the reason they were worth listening to.
	- name: Put the opam switch on PATH
	run: opam var bin >> "$GITHUB_PATH"

	- name: ast-utils, build & install plugin
	working-directory: ast-utils
	run: \|
	opam exec -- dune build
	opam exec -- dune install
	opam exec -- dune runtest

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@stable

	- name: Cache cargo registry & target
	uses: Swatinem/rust-cache@v2

	- name: Frama-C version smoke tests
	run: .ci/frama-c-smoke-tests.sh

	- name: Tutorial corpus WP shape gate
	run: scripts/check-tutorial-corpus.sh

	- name: Abs-int false-OK guard
	run: scripts/check-abs-int-fixtures.sh

	- name: WP model and encoding fixture gate
	run: scripts/check-wp-model-fixtures.sh

	- name: Integration tests (live Frama-C server)
	run: cargo test --test test-integration -- --test-threads=1

	# Must stay after the release build in .ci/frama-c-smoke-tests.sh:
	# test-process-lifecycle spawns target/release/frama-c-mcp from disk
	# rather than the harness binary cargo just built, so moving this earlier
	# tests a stale binary or no binary at all.
	- name: Process lifecycle, reload and conclusion tests
	run: \|
	cargo test --test test-process-lifecycle -- --test-threads=1
	cargo test --test test-reload-project-regression -- --test-threads=1
	cargo test --test test-store-conclusion -- --test-threads=1
	cargo test --test test-transport-poison-recovery -- --test-threads=1

	- name: MCP stdio E2E tests
	id: stdio
	# Parallel, unlike the gates above: every test in this suite owns its
	# server, its frama-c and its state directory. See scripts/run-gates.sh
	# for the measurement. libtest's default is available parallelism, so
	# this follows the runner rather than pinning a count.
	env:
	# A bind/listen race the retry absorbs is reported as a tracing warn,
	# and the default EnvFilter admits ERROR only, so without this the one
	# signal that the flake is coming back is dropped before it reaches
	# the log the next step scans.
	RUST_LOG: frama_c_mcp=warn
	run: \|
	set -o pipefail
	cargo test --test test-mcp-stdio --release 2>&1 \| tee "$RUNNER_TEMP/mcp-stdio.log"

	# Not success(): a refusal is one of the things that fails the suite, so
	# the scan has to happen on exactly the runs where the step above went
	# red. !cancelled() alone would not be enough, because it differs from
	# always() only on cancellation, so an earlier failed step in this job
	# skips the suite and still reaches here to scan a log nobody wrote. The
	# outcome check is what excludes that, and it is what lets the script
	# treat a missing log as a failure instead of tolerating one. A tolerated
	# missing log is a gate that passes by not running.
	- name: Detect an unqualified stdio connection refusal
	if: ${{ !cancelled() && (steps.stdio.outcome == 'success' \|\| steps.stdio.outcome == 'failure') }}
	env:
	STDIO_LOG: ${{ runner.temp }}/mcp-stdio.log
	run: scripts/check-stdio-refusal.sh

	# The supported floor, compiled but not measured. The three shell gates in
	# the lane above pin proved-goal counts to Frama-C 33.0 and Alt-Ergo 2.6.3,
	# so they cannot answer here, and widening their version cases to admit 32.1
	# would compare this lane's proofs against numbers measured somewhere else.
	# What the floor actually claims is narrower: that the plug-in still compiles
	# against the oldest Frama-C the opam constraint allows, and that its own
	# OCaml regressions still pass there. That is what this lane checks, and
	# until it existed nothing did: the version conditionals in ast-utils/src
	# have one arm no other job ever reaches.
	#
	# The version is pinned in ci_builds_the_plugin_on_the_supported_floor
	# against selfcheck::MIN_FRAMA_C_VERSION, so moving the floor without moving
	# this fails the unit lane rather than going quiet.
	plugin-floor:
	name: ast-utils plugin on the supported floor
	runs-on: ubuntu-24.04
	timeout-minutes: 45
	steps:
	- uses: actions/checkout@v7
	with:
	persist-credentials: false

	- name: Setup OCaml
	uses: ocaml/setup-ocaml@v3
	with:
	ocaml-compiler: "4.14.2"

	- name: Cache opam state (~/.opam + _opam)
	id: cache-opam
	uses: actions/cache@v6
	with:
	path: \|
	~/.opam
	_opam
	key: ${{ runner.os }}-opam-ocaml-4.14.2-frama-c-32.1-cppo-v1

	- name: Install Frama-C 32.1 and cppo
	if: steps.cache-opam.outputs.cache-hit != 'true'
	run: opam install -y frama-c.32.1 cppo

	- name: Check installed Frama-C version
	run: opam exec -- frama-c -version

	- name: ast-utils, build & install plugin
	working-directory: ast-utils
	run: \|
	opam exec -- dune build
	opam exec -- dune install
	opam exec -- dune runtest

	# The MCP server half of the product, prebuilt. The ast-utils plugin is not
	# here and cannot be: a .cmxs is tied to the exact OCaml and Frama-C the
	# switch holds, so a downloaded one either refuses to load or loads against a
	# different AST. README says so where it says how to download this.
	#
	# No Windows row. src/frama-c/transport.rs speaks tokio UnixStream, and
	# Frama-C does not target Windows either.
	build:
	name: Binary ${{ matrix.name }}
	strategy:
	fail-fast: false
	matrix:
	include:
	- name: Linux x86_64
	os: ubuntu-24.04
	target: x86_64-unknown-linux-gnu
	- name: macOS arm64
	os: macos-15
	target: aarch64-apple-darwin
	runs-on: ${{ matrix.os }}
	timeout-minutes: 30
	steps:
	- uses: actions/checkout@v7
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@stable
	with:
	targets: ${{ matrix.target }}
	- uses: Swatinem/rust-cache@v2
	with:
	key: ${{ matrix.target }}
	- run: cargo build --release --locked --target ${{ matrix.target }}
	# A binary that ships having never been executed is a promise nobody
	# checked. Both rows build natively, so the runner can run what it just
	# produced. --help is enough to prove it links and starts: Frama-C is
	# spawned lazily on the first project operation and is not installed in
	# this job, so nothing further would run here anyway.
	- name: Smoke-run the binary this job ships
	run: ./target/${{ matrix.target }}/release/frama-c-mcp --help > /dev/null
	# A tarball rather than a bare binary, because it carries the executable
	# bit and HTTPS does not.
	- name: Package
	run: \|
	tar czf frama-c-mcp-${{ matrix.target }}.tar.gz \
	-C target/${{ matrix.target }}/release frama-c-mcp
	- uses: actions/upload-artifact@v7
	with:
	name: frama-c-mcp-${{ matrix.target }}
	path: frama-c-mcp-${{ matrix.target }}.tar.gz

	# A rolling "latest" release, so the newest main build is one download away
	# instead of behind a login wall with a 90-day expiry, which is all the
	# artifacts above are. It needs every other job, not only "build": shipping a
	# binary whose suite went red is worse than shipping nothing. A matrix leg
	# that fails still fails its job, so a broken macOS row skips this even under
	# fail-fast: false.
	#
	# Delete and recreate rather than upload --clobber: the "latest" tag has to
	# move to the commit that produced these binaries, and no gh invocation
	# repoints an existing tag. That leaves a window where the release is gone and
	# its replacement does not exist yet, which drives the care below. The assets
	# are staged and named before anything is deleted, so a missing artifact fails
	# while the old release is still up, and cancel-in-progress is off for main so
	# nothing kills this job mid-window.
	release:
	needs: [rust-quick, artifact-scans, integration, plugin-floor, build]
	if: github.event_name == 'push' && github.ref == 'refs/heads/main'
	runs-on: ubuntu-24.04
	timeout-minutes: 15
	permissions:
	contents: write
	concurrency:
	group: release-latest
	cancel-in-progress: false
	env:
	GH_TOKEN: ${{ github.token }}
	GH_REPO: ${{ github.repository }}
	steps:
	# Needed since the shell below moved into .ci/: this job runs two scripts
	# out of the tree and would otherwise fail on the first push to main with
	# no such file. It is first so that checkout's workspace clean cannot wipe
	# the artifacts the next step downloads.
	#
	# persist-credentials matters more here than in the jobs above, not less:
	# this is the one job with contents: write, so the default would write a
	# token that can push to the repository into .git/config. Nothing here
	# uses git; gh reads GH_TOKEN from the environment.
	- uses: actions/checkout@v7
	with:
	persist-credentials: false
	- uses: actions/download-artifact@v8
	with:
	# Without a pattern this collects every artifact in the run, so an
	# artifact added to another job later would silently ship as a release
	# asset.
	pattern: frama-c-mcp-*
	path: dist
	merge-multiple: true
	- name: Stage assets
	run: .ci/stage-release-assets.sh
	- name: Replace the latest release
	run: .ci/publish-latest-release.sh

Navigation Menu

Uh oh!

Count what was proved, not what was claimed #92

Workflow file

Count what was proved, not what was claimed #92

Uh oh!

Workflow file for this run