Makefile

Rama main · réplica de lectura del repositorio original.

# Convenience targets. The conformance matrix in docs/conformance.md is generated, never
# authored: `make matrix` regenerates it, and CI fails if the committed block
# drifts from a fresh generation (see .github/workflows/ci.yml).

.PHONY: matrix matrix-check matrix-execute docs-gen docs-check demo demo-flagship demo-escape pre-merge pre-merge-affected formal roadmap-check roadmap-issue-state workflow-permissions runtime-seams vision-check

# roadmap item 327: the required gate before a change reaches main. Mirrors the
# FAST half of every per-backend CI job locally (emit/golden suites, the
# generated-artifact gates, lint) so the drift that `pytest tests/` alone misses
# — a stale per-backend suite that reds CI unnoticed — is caught before pushing.
# Steps that need a heavy/absent toolchain skip LOUDLY (never a false green); the
# target exits non-zero if any step that ran failed. See tools/pre_merge.sh and
# CONTRIBUTING.md "The pre-merge gate".
pre-merge:
	sh tools/pre_merge.sh

# FAST inner-loop gate: run ONLY the pre-merge targets that tools/affected_tests.py
# selects for the current diff (base = merge-base with origin/main). A sound
# conservative superset: any core/compile-reachable or unmapped change selects
# FULL and stops with the selector receipt; run `make pre-merge` to explicitly
# escalate. NOT a replacement for `make pre-merge`, which remains the release/CI
# gate. Override the base with: make pre-merge-affected BASE=<ref>
pre-merge-affected:
	sh tools/pre_merge.sh --affected $(if $(BASE),--base=$(BASE),)

# The roadmap's in-progress markers, checked against git. The roadmap is the
# state-of-record and its state is PROSE, so it rots silently: a marker reading
# "FIXING on `fix/x`" for a branch that merged hours ago costs the next agent a
# full re-investigation. Same contract as matrix-check: a claim that can be
# checked mechanically must be. See tools/check_roadmap_markers.py for what it
# can and cannot know, and CONTRIBUTING.md "Tracking work" for the discipline.
# --require-issue is on (roadmap item 452): the issue migration is finished, so
# every open or partial item cites its issue, or its private security advisory
# for a security item that must not be a public issue on this public repo.
# --check-tier-parity is on too (issue #1572), so this target is the lint job.
# --audit-successors (issue #2100) is on as well: it prints every top-level row
# that carries an in-progress glyph, the issue it cites and whether it names a
# successor. It is REPORT ONLY and needs no network, so it cannot redden this
# target; the gate that can fail a row on live issue state is the
# `roadmap-issue-state` target below, which is deliberately not wired here.
roadmap-check:
	python3 tools/check_roadmap_markers.py --check-contradiction --check-delegation --check-duplicate-headers --check-orphan --require-issue --check-tier-parity --audit-successors

# The same tool with all five prose checks on: self-contradiction, dangling
# delegation, orphaned findings, single-tier fixes for language-wide
# guarantees, and duplicate item headers. A, B, C, D and E are green on main
# and run in CI (the `roadmap-check` target above mirrors that line).
# D (--check-tier-parity) was red for a while with two real findings (items 421
# F6 and 422 F6); issue #1572 turned the check on once both were answered, and
# this target now exits 0. Roadmap item 523 kept claiming otherwise until issue
# #2100 corrected it.
roadmap-check-all:
	python3 tools/check_roadmap_markers.py --check-all

# Issue #2100: the one gate in tools/ that reads GitHub ISSUE STATE. A row that
# carries an in-progress glyph, cites a CLOSED issue and names no successor is
# a red here -- the marker says work is still going and the tracker says the
# issue it points at was shut. `--require-issue` (above) asks only that a row
# CITE an issue; it never asked whether the issue was still open.
#
# Needs `gh` on PATH with auth, and the network. FAIL-CLOSED: no `gh`, no auth,
# a rate limit, a timeout or a 404 leaves that issue UNKNOWN, which is never
# read as CLOSED -- so a broken lookup can neither invent a finding nor pass
# silently. If NO issue could be read at all the tool exits 2, "the environment
# cannot answer", never 0. That is why this is not in `roadmap-check`/CI: the
# lint job must not gain a network dependency, and on main today it reports
# real findings (rows whose cited issue closed with a residual still in the
# tree) that issue #2100's list exists to adjudicate one by one.
roadmap-issue-state:
	python3 tools/check_roadmap_markers.py --require-successor --issue-state

# The roadmap's CITATIONS, resolved against the working tree. The gate above
# asks git whether a marker contradicts a branch; this one asks the tree
# whether a cited test, symbol, path or scoped absence claim still holds. The
# six findings it reported on 2026-09-15 were paid down in #1110 and CI's
# `lint` job runs the `--check` line below; this target is the advisory read.
# Issue #1233 widened the path rule from 75 of the roadmap's 508 backticked
# path citations to 489 of them, which is where most of its citations live.
# This target also prints the claim ratchet, the citations that are stale and
# recorded as debt rather than fixed. See the tool's docstring for the two
# rules that were measured and thrown away, and why.
roadmap-claims:
	python3 tools/check_roadmap_claims.py

roadmap-claims-check:
	python3 tools/check_roadmap_claims.py --check

# issue #1204: the same question asked of docs/vision.md, which no tool read.
# Resolves its commands, links and backticked paths against the tree and
# re-checks the generated six-tier block against docs/conformance.md's per-tier
# totals. `--self-test` plants a rename per rule and requires each to be
# reported. Both lines run in the `lint` job. It resolves the commands and does
# not run them: CI's per-backend jobs are what run them.
vision-check:
	python3 tools/check_vision_claims.py --self-test
	python3 tools/check_vision_claims.py --check

# issue #191: the workflow permission gate. A job-level `permissions` block
# REPLACES the workflow-level one rather than merging into it, and the release
# path is the one place where getting that wrong is invisible until a tag is
# already pushed. `--self-test` reintroduces the original bug into a synthetic
# workflow and asserts the gate catches it; `--strict` also fails a job with no
# block at any level. Both run in the `lint` job and in tools/pre_pr.sh.
workflow-permissions:
	uv run --no-project --with pyyaml==6.0.2 python3 tools/check_workflow_permissions.py --self-test
	uv run --no-project --with pyyaml==6.0.2 python3 tools/check_workflow_permissions.py --strict

# issue #292: each fail-silent `revl_*` runtime seam (read through a getattr
# string literal in backends/python/replay.py and src/revl/run.py) is defined
# exactly once with the arity its caller uses. The merge_group trigger in
# ci.yml closes the merge-interaction class by construction; this is the static
# half that catches the one of the three defects a linter could -- a
# cross-module duplicate/incompatible-signature definition, which F811 and
# every type checker walk past because the seam is resolved by string name.
# `--self-test` reds the gate against the issue-#292 collision itself. Both run
# in the `lint` job and in tools/pre_pr.sh. Stdlib-only, so no uv wrapper.
runtime-seams:
	python3 tools/check_runtime_seams.py --self-test
	python3 tools/check_runtime_seams.py

# Regenerate the docs/conformance.md conformance + performance matrix in place.
matrix:
	python3 tools/conformance.py --write-readme

# The staleness gate CI runs: exit non-zero if the committed block is stale.
matrix-check:
	python3 tools/conformance.py --check-readme

# The matrix's third question (issue #244): RUN the cases that have an answer
# and check every tier computes the same one. `--validate` stops at compile
# depth and cannot see a tier that compiles and then means something else.
# A tier whose runtime is absent here reports `-`, never agreement.
matrix-execute:
	python3 tools/conformance.py --execute

# issue #255: the source-derived blocks in DESIGN.md and the five docs that
# carry them. `docs-gen` regenerates them in place; `docs-check` is the gate the
# frontend CI job runs. Run docs-gen after editing anything under docs/ (the
# DOC-STATUS inventory is a function of every docs/*.md) or after adding a CLI
# subcommand, an MCP verb or a diagnostic guarantee.
docs-gen:
	python3 tools/docgen.py --write

docs-check:
	python3 tools/docgen.py --check

# v3.0 gate E3: the live-systems demo (swap / why / apply) from a clean
# checkout. Ensures the cordis-py runtime is set up, then runs the scripted
# demo under it (demo/live_systems/run_demo.py). REVL_DEMO_REQUIRE=1 makes a
# missing runtime fatal rather than a silent skip.
demo:
	@[ -x backends/python/.venv/bin/python ] || sh backends/python/setup.sh
	REVL_DEMO_REQUIRE=1 backends/python/.venv/bin/python demo/live_systems/run_demo.py

# Roadmap item 525: the flagship integrated demo. One legacy-enterprise agent
# across the typed API, a peer service and the computer-use family, with the
# guarantee each leg discharges named beside the artifact that shows it. Needs
# the compiler and nothing else, so there is no runtime to set up first.
demo-flagship:
	python3 demo/legacy_enterprise/run_demo.py

# Issue #2691: three components that exceed what they declared, each refused,
# explained and repaired, then audited. Compiler only: no runtime, no network.
demo-escape:
	python3 demo/escape/run_demo.py

# formal/ — the machine-checked backbone (formal/STATUS.md). run_gate.sh:
# the import-layering and non-vacuity gates (both toolchain-free, so they
# always run), then lake build, then the axioms gate (no theorem may
# depend on sorryAx, an unfinished proof, or on any project-defined axiom;
# the machine-checked form of "a claim gets a command or it gets
# softened") over both CheckAxioms.lean and harness/Oracle.lean's own
# print block — the oracle file is outside the RevL library root, so it
# needs its own pass — then the harness census. The non-vacuity gate is roadmap
# item 418 step 8: `#print axioms` is as clean on a theorem whose
# hypotheses cannot all hold as on a load-bearing one, so every registered
# theorem carries a row in formal/scripts/nonvacuity.tsv naming its
# evidence. A missing elan/lake skips LOUDLY (never a false green),
# matching the pre-merge discipline. The logic lives in a script, not
# recipe lines: each recipe line is its own shell, so an in-Makefile
# skip-guard cannot stop the target. The script exits 77 for that skip so
# tools/pre_merge.sh can report it as SKIPPED; here it stays a success, since
# the SKIP line above it already says what was not checked.
formal:
	sh formal/scripts/run_gate.sh || [ $$? -eq 77 ]