Repository navigation
Conversation
Add an `open_statements: allowed|forbidden` policy to roadmap/README.md.
Absent or forbidden keeps the strict policy, where CI rejects every sorry;
the key on any other article, or any other value, is a validation issue.
Derived status now records can_state, can_prove, waiting_on and assumes.
Under the strict policy a statement also waits for its proof prerequisites
to be proved, matching what `work list` already enforced. Under the open
policy a statement waits only for its statement prerequisites, a proof for
every prerequisite to be stated, and a proof that rests on an open
statement gets the new violet `conditional` state ("conditionally proved"),
never fully proved.
The legend, the Next up card and article pages follow: conditional articles
carry an Assumes row naming the open statements they rest on. The runtime
projection takes readiness from the derived status and serializes assumes,
waiting_on and the policy. The work frontier reads blockers from the
derived status and names the policy and each item's assumptions in text
and JSON. The new `autoform work assumptions [target] [--json]` command
emits the autoform-assumptions/v1 contract that CI audits the Lean build
against. Strict-policy work text is unchanged.
Nothing pinned the reworded legend meanings for can_prove and can_state or the policy-neutral Next up explanations, so add a legend test and a landing-page test for both phases. The conditional article test now checks that the Assumes row sits after the Lean row and before Discussion, as spec A3 places it. Under the open policy, `work list` names the policy even when nothing is ready; a test covers that branch. Also restore the two blank lines after the conditional legend test.
`work assumptions` maps OSError and RuntimeError to a path-free message with exit 2 and leaves output errors to propagate, like `work list`, but only its validation errors were tested. Extend the existing error tests to pin both branches for the new command.
ClaimBoard gains acquire_many, renew_many, and release_many. Each reads every key with one ls-remote, applies the per-key checks of the single-key method, and changes all refs in one git push --atomic with a --force-with-lease per ref, so a batch never holds some claims and not others. A lost race or a held claim returns a ClaimBatchResult naming the blocking keys, read from the porcelain status lines or the remote's "cannot lock ref" error. A board that does not support atomic pushes raises ClaimTransportError instead of falling back to separate pushes. autoform claim acquire|renew|release now takes one or more nodes. One node keeps today's code path and output; several print one line per target on success, one error line naming the blockers on failure, and exit 2 on a duplicate target.
The B1 contract separates transport problems, which raise ClaimTransportError, from a lost race or a held or unverifiable claim, which return a failure that names the blocking keys. The batch methods raised MalformedLeaseError for an unverifiable lease, so the CLI printed a bare key-level error instead of the "no claim was <op>ed" line. acquire_many, renew_many and release_many now report such a key as blocking with the reason "malformed lease". When keys block for different reasons, every key is named in batch order and the reasons are joined with "or". The per-key checks and the single-key methods are unchanged, and nothing is pushed. Tests cover each batch method with a malformed key, a batch with mixed reasons, the multi-node CLI line for a malformed claim, and the renew failure line.
The Lean findings pass of audit gains lean-target-deprecated: an article's lean: declaration whose source carries the deprecated attribute in an @[...] list before its keyword, on the declaration line or on the contiguous attribute lines directly above it. Comments are blanked first and string literals inside attribute lists are ignored, so a commented-out attribute or a name such as deprecated_alias does not count.
autoform work impact SELECTOR --lean-root PATH reads every project-local constant from the built environment with a new Lean probe, run through skeleton.run_probe so the freshness check, time limit and output bound apply. The revised set is the article's lean: names or the repeatable --declaration names, each of which must be project-local. Statement impact is the reverse closure over meaning edges (types, the values of definitions and opaque constants, an inductive's constructors). Proof impact covers constants with a body whose value reaches that set directly or through internal details such as simp's _simp_1 companions and a definition's _proof_1. The report names the impacted articles, the helpers no article names with their location and owning article, impacted articles with no Markdown dependency path to the revised one, deprecated constants and their users, the claim targets, and whether the revision is contained. --json writes the autoform-impact/v1 schema. The probe imports the modules Lake builds: each library's globs (M, M.* and M.+; other forms fail closed), else its roots. LeanLibrary records the globs, and run_probe takes a label so its errors name the impact probe; skeleton behavior is unchanged.
Locate a private helper by its source name, and fall back to the module's file without a line when the index finds the name in another file. Refuse a roadmap that changes between work_context and the runtime graph, both when an article is rewritten and when the selected article vanishes. Check that the shadowed-Std probe failure names the impact probe too, and rename the contained-revision test after what it checks. Keep an earlier declaration's @[deprecated], on its own line or before an alias, from marking the theorem that follows it.
When roadmap/README.md sets open_statements: allowed, the verify workflow asks `autoform work assumptions` for the assumption contract and renders an open-statement probe instead of the strict one. The probe accepts sorry only as the direct proof of a theorem that an open article's lean: names, and accepts any other declaration that reaches such a theorem only when its article's Markdown dependencies reach it. It rejects sorry in a type, a helper, a where clause or a definition, sorry inherited from outside the root package, contract names that the build does not declare, and an open statement whose article records it as proved. Every article declaration is logged as an open statement, conditional, or sorry-free. The article table is embedded as one JSON string and parsed with Lean.Json, because a term with thousands of tuple entries exceeds the elaborator's and code generator's recursion limits. Without the opt-in, the helper renders the same strict probe as before. The real-Lean CI job now also runs tests/test_lake_artifact_audit.py, so the new probe scenarios and the existing Lake artifact checks run against the fixture toolchain.
Describe the open_statements policy, the conditional state, work assumptions, work impact, multi-key claims, the CI open-statement audit and its pin requirement, and the revision contract in the CLI reference, and point the Formalize, Roadmap, Human Review, and Agent Review skills at them.
Retracting a statement removes `statement` but keeps `lean:`, so the old declaration and its sorry stay in the build until Formalize restates the article. Status and the assumption contract skipped unstated articles, which made CI reject that sorry as undeclared and showed every proof resting on it as plainly proved. Under the open policy such a theorem now stays an open statement, and every article with declarations, stated or not, gets a contract entry.
A helper is repaired under its owner's claim, so the owner's claim target belongs in claim_targets. Owners were reported only by node id, which is not the key the owner's worker claims when the article has an article_id.
The Assumes row and the graph legend said a conditional proof rests on open statements whose Lean proofs are still sorry. A retracted theorem that keeps its lean: name counts as open even when its Lean proof is complete, and a sorry-free proof recorded with only its statement is open too, so both texts now say the open statement has no recorded Lean proof, which holds in every case.
Under the open policy derive let a definition's statement wait only on its statement prerequisites, so work list, work context and the site offered a definition whose body uses an unstated theorem with no Lean declaration. A definition cannot land open: writing it down is its proof, and a sorry in a def fails CI. It now also waits for every proof prerequisite to be stated (an open statement counts), and waiting_on names the missing ones. The strict policy is unchanged.
The text output printed a conditional: line for every contract entry with assumptions, so an unproved open statement appeared as both open: and conditional:, while the docs reserve conditional for a proof that rests on an open statement. An open entry now carries its assumptions on its open: line, and conditional: is printed only for entries that are not open. The JSON contract is unchanged.
An article with proof: formalized and no statement: formalized used to be skipped by assumption_contract, so its declarations escaped the CI open probe. Pin that it gets an entry that is not open and whose allowance is limited to the open statements it assumes, under both policies.
Retracting a definition's statement left its `lean:` declaration in the build, but status gave it no reach, so a proof using it showed as proved while the CI audit flagged it as resting on the open statements the definition's body uses. A retracted definition now passes on the union of its prerequisites' reaches, as a stated one does. It is not open itself: CI rejects a `sorry` in a definition, so it cannot stand for an unproved claim.
The open-statement probe defined its helpers inside namespace AutoformOpenStatementAudit and read the article table with an unqualified Json.parse. Inside a namespace Lean resolves a name to a constant under that namespace first, so a root module defining AutoformOpenStatementAudit.Json.parse replaced the parser, forged the table and let a sorry theorem recorded as proved pass the audit. The helpers now live at the top level under distinctive autoformOpenAudit* names, where a clashing root constant fails as already declared and one matching a library name makes the reference ambiguous, and the parser is spelled _root_.Lean.Json.parse. Real-Lean tests cover the namespaced hijack and a root-level Json.parse forgery.
The open probe's article loop printed sorry-free, conditional and sorry-free-open-statement info lines even when the same declaration had an error, from the roots loop (an unexpected axiom) or from the article loop itself (an open statement its Markdown does not reach), so the log showed a clean line right next to the error. Those lines are now logged only for a declaration that added no error; the verdict is unchanged.
Lean compiles a mutually or well-founded recursive proof into auxiliaries such as X._f and X._unary, so a sorry written directly in an open theorem's recursive body is reported on the auxiliary, and the error told the user to do what they had already done. The audit still rejects it; the message now says that a recursive open statement's proof must be exactly sorry.
run_probe takes a label, but its missing-manifest and stale-artifact messages always said to run `lake build` "before extracting skeletons", so `work impact` on a stale build talked about skeletons. Both messages now say "before running the impact probe" for the impact probe, while the skeleton probe keeps its exact wording.
…k impact Articles and --declaration name a private declaration as its source does, but probe records carry kernel names, so an article naming one dropped out of the report and `work impact` on it failed. The probe now emits each private constant's user-facing name; a name resolves to its exact record, else to the one private record with that user-facing name, and a name several private records share is refused. Helpers of a private declaration find their owner through it, and the source locator uses the same field instead of stripping the private prefix. A theorem whose value is exactly a constant, as Batteries' `alias` makes, copies its target's type without mentioning the target, so it landed in the proof set and its users went unreported. The probe now emits that constant as `alias_of`, and it counts as a meaning edge. A deprecated constant's own generated companions (`eq_1`, `_simp_1`) no longer count as its users, though real users of a companion still do. A deprecated constant that another article's lean: names lists that article and stays out of deprecated_unused. Helpers the revised article owns, such as a structure's generated constructor and recursor, are repaired under its claim and no longer make a revision non-contained.
A root constant named like one of the open probe's helpers made the helper's own definition fail as already declared, so the audit ran with the imported constant in its place. The job still failed on that error, but the log ended with the clean summary. The audit now refuses to start when any helper resolves to an imported constant. A declaration whose `where` clause or other auxiliary failed, or that used a failing helper, still printed a `conditional:` line when it also rested on a declared open statement, because only its own errors suppressed the line. It now gets no clean line when anything it reaches through the audit's edges failed.
work impact treated any theorem whose value is exactly another local constant as that constant's alias and put it in the statement-impacted set with its target. A hand-written theorem such as `theorem t : seed = 1 + 1 := seedEq` keeps its own statement when seedEq's changes; only its proof breaks. Require the theorem's type to be exactly the target's, instantiated at the value's universe levels, which is what Batteries' alias writes, so such a theorem is reported as proof-impacted instead.
Bring the README and the Formalize, Roadmap and Human Review skills in line with the code: a definition is ready to state only once its proof prerequisites are stated, a retracted theorem stays open while its lean: names the old declaration, the open audit logs at most one line per declaration and none that reads as passing after an error, and a recursive proof must be sorry as a whole. Describe how work impact names private declarations, what counts as an alias, and which derived declarations it does not report.
tests/test_impact.py builds a Lean project and runs the work impact probe against it, and honours AUTOFORM_REQUIRE_REAL_LEAN_TESTS like the skeleton suite, but no CI job ran it with Lean installed, so it was always skipped. Add it to the real-Lean job.
…mpact Lean adds a partial def to the kernel as an opaque constant whose value is only an Inhabited witness; the body it runs is the internal _unsafe_rec companion, which nothing else names. work impact therefore never reported an article whose lean: is a partial def that uses the revised set, so a revision could be judged contained while that definition stopped compiling. The probe now counts the companion as the opaque constant's value, as it counts an inductive's constructors.
Doctor sorts audit findings into its "audit" and "lean targets" checks by code, and its list predates lean-target-deprecated, so a deprecated target failed the roadmap audit check while "lean targets" still said every target resolves. List the code with the other Lean target findings.
…step The skeleton suite already uses most of its step's 25-minute timeout, so sharing that budget let a slow impact or audit test cut the skeleton suite short. Give the two suites a separate step with its own timeout, and leave the skeleton step as main has it.
The open-statements section said a retracted theorem stops being open once its statement is recorded again, but a restated theorem without a recorded proof is still an open statement: the audit keeps accepting its sorry and what rests on it stays conditional. Also say that the one-line limit per declaration covers the status lines, since errors are logged on their own.
meta-cla
Bot
added
the
CLA Signed
The test asserts the Lean row that the site shows for a declaration without a source link, but on GitHub Actions the renderer detects repository coordinates from GITHUB_REPOSITORY, GITHUB_SERVER_URL and GITHUB_SHA and links the source instead, so the row is absent and the test failed on CI only. Clear those variables and pass empty coordinates, as the stranded-links test already does.
main merged #92 and four later PRs. The one conflict is the stale-artifacts message in skeleton.py: main names the exact `lake build` targets, and this branch names the probe the build must precede. The resolution keeps both, so the impact probe's message now reads "run `lake build Demo` before running the impact probe", and its test expects the target.
A theorem with lean: but no statement: formalized used to count as an open statement, so a draft lean: name on a theorem that was never stated became an assumption its dependents could rest on, and CI accepted its sorry. Roadmap now records the retraction as statement: retracted, which the loader checks against lean:, proof: formalized and mathlib: true, and only stated or retracted theorems are open. The assumption contract also lists Mathlib articles that name lean: declarations, never open and allowed nothing, so CI can check those names exist and reach no open statement. Work items carry a revision flag that points Formalize at autoform work impact, and the assumptions text report calls an article conditional only when its derived state is, naming conditional articles without lean: too, and labels other listed articles that assume something as unproved.
… no article owns it A helper no article owns was listed in work impact but claimed by nobody, so two revisions that both had to repair it could proceed at once without contending. Each helper now carries claim_target: its owner's claim target, or a lean/ key derived from its name the way author claim keys are, and claim_targets includes every helper's. Revisions touching the same unowned helper therefore contend for one claim. The JSON helper objects gain claim_target and the text report prints it; contained is unchanged, since an unowned helper already made a revision not contained.
A Lean revision requested in Human Review was stranded: Roadmap only recorded the decision, so the article stayed proved and work list never offered it. Roadmap now retracts the article with statement: retracted, keeping lean:, so it returns to the frontier as a statement phase flagged as a revision. The README and skills now describe the marker and which articles are open statements, the mathlib articles in the assumptions contract, the revision flag on work items, and the lean/<slug>-<digest> claim key for unowned helpers. The revision contract defines a claim set per route, migrates proof-impacted articles off a sorry'd X under the expand route (otherwise X never becomes unused and R can never record its proof), re-runs work impact after the rebase, and warns that instance, attribute, and notation changes are invisible to it. Several statements that contradicted the code are corrected, and the audit's sorry-free hint now says to restate a retracted article before recording its proof.
This was referenced Oct 5, 2026
`work impact R --declaration X` skipped X when listing helpers, so when no article named X its claim set held only R's target. Two revisions of the same unowned helper from different articles then each claimed only their own article and could both edit X. A revised declaration no article names is now claimed under its owner's target, or under the `lean/<slug>-<digest>` key an unowned helper gets, and `contained` holds exactly when the revised article's target is the only one, so such a revision is never reported as safe to make in place under R's claim alone.
The expand route told proof-impacted articles to drop `proof: formalized` so they return to their proof phase while X is still `sorry`. A stated definition counts as proved whatever `proof:` says, so that did nothing for a proof-impacted definition, which kept resting on the deprecated X and kept it out of `deprecated_unused`. Such a definition is now migrated to X' in the same commit or, failing that, retracted like a statement-impacted article, and the claim set covers every article whose frontmatter or Lean changes. A project whose CI pins an older AUTOFORM_REF fails `autoform check` on `statement: retracted`, since older loaders accept only `formalized`. The README's assertion table and the Roadmap skill now say to move the pin first, and until then to retract by removing `statement` and `proof` and keeping `lean:`. Status treats every stated, unproved theorem as an open statement, with or without `lean:`, while the README defined one as having `lean:`. The README now matches the code and notes that CI audits an open statement only through the declarations its `lean:` names.
No test checked the audit's line for an open statement whose proof is sorry-free, which now tells the worker to restate a retracted article before recording the proof, and no real-Lean test fed the audit a contract entry in the `mathlib` state the assumptions contract writes. The open-probe fixture gains a sorry-free open theorem whose exact line is asserted, the outside-root declaration is audited as a `mathlib` article, and a `mathlib` article whose Lean reaches an undeclared open statement must fail.
Three readers interpret open statements: derive, the work list, and the assumptions contract CI audits Lean against. Each was pinned only by hand-written fixtures, so a change to one could drift from the others without any test noticing. tests/test_contract.py writes seeded random roadmaps of theorems and definitions under both policies and checks them against each other and against the stated semantics: fully proved rests on nothing open, conditional is exactly proved-but-assuming, the work list offers exactly the ready phases, the contract opens exactly the open statements and allows only what each article rests on, and the audit's validator accepts every contract. Invalid retractions are generated too and must fail to load. A real-Lean test builds a small open-policy project, runs the audit the way the verify workflow does, and checks that the site never claims more than the audit: every fully proved article is sorry-free, and every article resting on an open statement is conditional or open. It joins the real-Lean CI step, which took under 7 minutes locally on a heavily loaded machine.
Contributor
Author
|
Superseded by the reviewable stack #135 → #136 → #138. The split preserves the original work while separating atomic claim transport, Lean revision impact/deprecation, and the opt-in open-statement/kernel-audit policy. Each layer has its own focused validation and dependency boundary; continue review on those PRs. |
This was referenced Oct 5, 2026
Deicyde
added a commit
that referenced
this pull request
Oct 6, 2026
The impact probe follows names, so a Markdown statement dependent whose Lean inlines the revised definition's body instead of naming it was not impacted, and the revision left it fully proved under the old meaning. The report now lists unused_statement_dependencies: the stated articles that reach the revised article through Markdown statement edges, transitively, but are not statement-impacted. They join claim_targets and keep the revision from being contained, and the text report prints them on one line. The README describes the field and what contained now requires. How the revision contract treats such an article belongs with the contract, in the open-statements layer. Restored from closed #115 (d9f9e94) and adapted to this layer's plural helper owners and Lean source and build revision lines.
Deicyde
added a commit
that referenced
this pull request
Oct 6, 2026
A mathlib: true article counts as stated, so one whose Markdown statement depends on the revised article was reported in unused_statement_dependencies and claimed, although its statement is a Mathlib declaration that cannot use the revised one and the loader refuses to retract it. Restored from closed #115's review follow-ups (3bc24df).
This was referenced Oct 6, 2026
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Base
main. #92 has merged, and this branch mergedmainat7b65ebc(merge commit94e7772), so the diff is this PR's work only.Two additions to the Markdown formalize frontier. Open statements are opt-in. The revision contract adds commands, multi-target claims, report fields, a retraction marker, and one audit finding, and the skills now follow it. A project that does not opt in sees four changes: the readiness fix in the first bullet below, the
lean-target-deprecatedfinding, thestatement: retractedmarker, and the skills' revision procedure.The contract below states the promise this PR keeps between the wiki and the Lean, the gaps a contract audit found, and how each was closed. Reviewing that section against the code is a smaller job than reviewing the diff.
Open statements (opt-in)
open_statements: allowedinroadmap/README.mdlets a theorem's statement land with asorryproof; the key is valid only on that page and acceptsallowedorforbidden. Absent orforbiddenkeeps the strict policy: whatwork listreports as ready and the CI audit are unchanged, and "ready to state" on the site andcan_statein the runtime projection now agree withwork list, which already held a statement until its proof prerequisites were proved. The site's legend and article text now say a node's prerequisites are ready rather than stated or proved, since which applies depends on the policy.statement: retractedand is not proved. CI audits it only through the declarations itslean:names. A theorem that was never stated is not open even with alean:name, so a draft name never becomes an assumption and CI rejects itssorry. A retracted definition is not open, but what rests on it still assumes the open statements its body reaches.conditional, labelled "conditionally proved": violet on the site, never green and neverfully_proved, with anAssumesrow on the article page andassumesinwork list,work context, and the runtime projection. In JSON, all three also carry anopen_statementsflag, and each runtime node addswaiting_on. A conditional proof recordsproof: formalized; only the derivedfully_provedmeans complete andsorry-free.autoform work assumptions [--json]lists oneopen:line per open statement, oneconditional:line per conditional article, and oneunproved:line per other listed article that assumes open statements.--jsonwrites theautoform-assumptions/v1contract: every article whoselean:names a declaration,mathlib: trueones included withopenfalse and nothing allowed, so CI checks their names exist and reach no open statement.autoform-verify.ymlreads the policy withautoform_audit.py --policyand, underallowed, audits every root-package declaration in the built environment against that contract. It accepts asorryonly inside a declared open statement's own proof (the README asks for the whole proof to besorry, which the audit does not check), and a proof that reaches only the open statements its article's Markdown dependencies reach. It rejects asorryin a type, a helper, a definition, or a Lean-generated auxiliary; asorryinherited from outside the root package; a declaration that reaches an open statement its article's Markdown dependencies do not reach; alean:name missing from the build; and an open statement recorded as proved. Each article declaration gets at most one status line: one of threeopen statement (...)lines,conditional: NAME [ID] rests on open statement(s) A, B, orsorry-free. The sorry-free open statement line readsopen statement (proof is sorry-free; restate it if retracted, then record proof: formalized): NAME [ID]. Errors are logged on their own lines, and a declaration with an error gets no line that reads as passing. The summary line counts open statements and conditional declarations, so a conditional result never reads as sorry-free.Revising shared declarations
statement: retractedrecords a retraction. The article keepslean:, whichwork impactneeds, and returns to the frontier as a statement phase; Formalize restates it by replacing the marker withstatement: formalized. The loader rejects the marker withoutlean:, withproof: formalized, or withmathlib: true.work listandwork contextflag such an item as a revision:revisionis true in JSON, and the text adds arevision:(list) orRevision:(context) line saying to start fromautoform work impact.autoform work impact R . --lean-root . [--declaration NAME] [--timeout SECONDS] [--json]runs a Lean probe on the built project and reports what revising R's declarations affects: statement-impacted articles (whose meaning reaches the revised set through types, definition bodies, inductive constructors,partial defbodies, andalias-style theorems), proof-impacted articles, helpers no article names (each with its owning article when one exists, and itsclaim_target), impacted articles with no Markdown path to R, every deprecated project declaration with its replacement, its users, and the other articles whoselean:names it,deprecated_unused,claim_targets, andcontained. A helper no article owns is claimed under alean/<slug>-<digest>key derived from its name, so two revisions that touch it contend for one claim. A revised declaration that no article names is claimed the same way, under its owner's target or its own key.containedholds exactly when R's target is the only claim target.--jsonwritesautoform-impact/v1.autoform claim acquire,renew, andreleaseaccept several targets and change all of them or none in one atomic push. The README's claim contract adds a no-hold-and-wait rule for work that needs several claims.autoform audit --lean-rootreportslean-target-deprecatedfor an article whoselean:names a declaration withdeprecatedin its own@[...]attribute list, andautoform doctor --lean-rootlists it under its Lean targets check. The finding is an error, so both commands fail when alean:names a deprecated declaration, including, by design, while an expand route keeps a superseded declaration in R'slean:; the Formalize skill exempts that case. The generated CI runs neither command.contained, re-checking R's other declarations that use X, whichcontainedignores. Otherwise expand, migrate, contract: add X', deprecate X, point R'slean:at X', retract the statement-impacted articles withstatement: retracted, and, while X's proof is stillsorry, return the proof-impacted articles to their proof phase so they migrate to X' (otherwise X never becomes unused and R can never record its proof). In that case a proof-impacted definition, which counts as proved once stated, is migrated to X' in the same commit or retracted. Delete X oncedeprecated_unusedlists it. Revise in place, claiming everyclaim_targetsentry and landing one commit whose default build passes, only when X and X' cannot coexist, or when the change is to an instance's priority or scope, an attribute, or notation, whichwork impactcannot see; then every stated article whose Lean imports the changed module is treated as statement-impacted.work impactis re-run after acquiring and again after rebasing; a set that grew is acquired whole under the no-hold-and-wait rule. Roadmap edits only Markdown: it retracts the revised article with the marker, also for a Lean revision requested in Human Review, and the dependents whose text it rewrites; Formalize does the rest.The contract
The wiki says what is claimed, the Lean is the evidence, and the site,
work, and CI must never claim more than the Lean proves.sorry(strict) or only the declared open ones (open).roadmap/README.md, strict by default; the CLI and CI parsers agree or fail closed.work, the runtime JSON, and the site.work impact, one atomic multi-target claim, and one commit whose default build passes.work impactand claims; the rest is processstatement: formalizedmeans the Lean declaration says what the article says.tests/test_contract.pychecks the first four rows, apart from failing closed on a bad policy value. A seeded property test writes 30 random roadmaps under each policy, using the standard library only. It checks thatderive,work list, the runtime projection, and thework assumptionscontract agree with each other and with a model computed from the frontmatter alone. It also checks that the CLI and the audit script read the same policy, and that the loader refuses each invalid retraction with its own message. A real-Lean test builds a fixture project and runs the verify workflow's steps. It checks that every article the runtime projection shows fully proved is auditedsorry-free, and that every article the audit finds resting on an open statement is conditional or open. The last two rows rest on process and review.A contract audit (agents listing invariants from the code, a red team per area, an independent check of each attack) found ten gaps in this PR. All are closed here:
statement: retractedlean:counted as an open statementmathlib: truearticles were left out of the open contractrevisionsorry'd X, which therefore never became unusedwork impactcannot see instance, attribute, or notation changeswork impactafter the rebaselean/<slug>-<digest>work assumptionsmislabelled two casesopen:/conditional:/unproved:follow the derived stateA second review of those fixes found six more problems, also fixed here:
work impact --declaration Xskipped X when listing helpers, so when no article named X, two revisions from different articles could each claim only their own article and both edit X. Such an X is now claimed under its owner's target or its ownlean/key, andcontainedholds exactly when R's target is the only claim target.proof:says, so under the expand route a proof-impacted definition kept resting on thesorry'd X and kept X out ofdeprecated_unused. It is now migrated in the same commit or retracted.AUTOFORM_REFpin older than this branch makesautoform checkrejectstatement: retracted. The README and the Roadmap skill now say to move the pin, and until then to retract by removingstatementandproofand keepinglean:.lean:, while status treats every stated or retracted, unproved theorem as open. The README now matches the code.mathlibcontract entry. One now does, and amathlibarticle whose Lean reaches an undeclared open statement must fail.The audit also found seven gaps that already exist on
main(H1 to H7). Separate draft PRs stacked on this branch fix them, so this one stops growing:lean:name is in the build, checks alean:name outside the root package for unsafe declarations and unexpected axioms, and replays the root package through the kernel (H1, and the first halves of H4 and H6).autoform verifypassed, andcheck --lean-rootrefuses alean:name defined more than once (H3, and the second half of H4).statement_hashbindsstatement: formalizedto the statement text and the Lean meaning it was reviewed against, and CI checks it withautoform skeleton --check-statements(H5).proof: formalizedwithoutstatement: formalized, and either one without alean:declaration;work impactreportsunused_statement_dependencies(H2, H7).The second half of H6, build-time IO during
lake build, stays open. Closing it needs a separate audit job and the governance call below.Open decision, not changed here: the trust model. If workers are untrusted, opting in is a one-line edit to
roadmap/README.md, a file pull requests control, which argues for CODEOWNERS onroadmap/README.mdand.github/. That is a governance call for the maintainers.Validation
ruff check autoform_cli servers tests: clean.0237cd6: 1255 passed, 45 skipped, 4 failed. The 4 failures are thetests/test_scaffold.pypin tests. They fail only because my local clone has nooriginremote, soplugin_pin()finds no pin; they pass in a clone withoriginand in CI.AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), the new CI step's selection,tests/test_lake_artifact_audit.py tests/test_impact.py tests/test_contract.py: 136 passed, 1 skipped. The skip istest_helper_runs_on_python_310, because python3.10 is not installed on this machine.0237cd6, push run 37364104121: all four jobs pass, on the fourth attempt. Each earlier attempt lost some Linux jobs before they started, with "The job was not acquired by Runner of type hosted even after multiple attempts".tests/test_skill_examples.py:32.mainitself fails that test since e54e5ab removed the README sentence it checks, and the PR run tests the merge with currentmain. Align README test after removing execution-branch guidance #137 fixes it onmain; this branch's own push run passes test (3.10).0da3cac, before the second review's fixes, both runs passed.Known limits
sorry: recursion can move asorrycase into_for_unary, which the audit rejects as helpers, as it does awhereclause's auxiliary.work impactdoes not report a declaration derived throughto_additiveor its users, shows the directions of anIffalias only as proof-impacted, and cannot see a change to an instance's priority or scope, an attribute, or notation (all documented).lean-target-deprecatedis lexical: it misses a laterattribute [deprecated] X, which the deprecated list ofwork impactcatches.work, and the site derive conditional results from the Markdown dependencies and CI from what the Lean uses, so CI can printsorry-freefor an article the site shows as conditional (documented; never the reverse).lake build --wfailandwarningAsErrorcannot be combined with open statements.lean:makeswork impactrefuse to run for every article.AUTOFORM_REFpin,autoform-verify.yml, andautoform_audit.pyfrom this branch; an older pin, workflow, or audit script fails closed. The bundled example gets the new workflow and audit script but keeps its pin and does not opt in, so it stays strict.autoform checkalso rejectsstatement: retracted, even in a strict project. Until the pin moves, retract by removingstatementandproofand keepinglean:; the README and the Roadmap skill say so.