Repository navigation
Conversation
The count before parsing took only delimiter rows with a hyphen, and ended a table at a line of ">". Python-Markdown takes any delimiter row of pipes, colons, hyphens, and spaces, a row of pipes alone included, and outside a block quote a line of ">" is one more row. Such tables reached millions of cells and were refused only by the rendered-size backstop, after seconds of rendering. Every line of those characters with a pipe now counts as a delimiter row, its header's cells as its columns, and a table runs to the next whitespace-only line.
GitHub reads card files with cmark-gfm, not markdown-it, and marks formulas by its own rules. Read testimony with cmark-gfm, find the formulas GitHub marks as its Markdown API was seen to, and compare what that reading shows with the site's rendering, element by element. Refuse a difference with the line where the two part and a rewrite both read alike, and refuse a formula GitHub was not seen to read as emulated.
MathJax reads no text of a card outside the formulas the renderer marked, and GitHub's Markdown API was seen to read no formula in \begin, \ref, \eqref, \(, or a lone dollar sign in text, so refusing them there kept out quoted LaTeX for no reason a reader could see. Where GitHub does read a formula, the comparison with its reading still refuses it. Delimiters inside a formula are still refused, with advice that fits them.
The renderer kept \$ escaped on the premise that MathJax shows it as a dollar sign, but MathJax reads no text of a card outside the formulas the renderer marked, so the site showed the backslash where GitHub shows none. Let \$ come out as a bare $, and say how to keep dollar signs typed where GitHub pairs an escaped one into a formula.
extract_skeletons and _translate_lakefile opened their temporary directory outside any signal guard, so the guard of the first command inside was the outermost one. On SIGTERM or SIGHUP that guard restored the default handler and re-delivered the signal as it exited, which ended the process before the enclosing TemporaryDirectory ran its cleanup, leaving an autoform-skeleton-* directory behind. Both now enter _signal_guard() before the directory. Guards nest by reuse, so the helper build, the probe pool, and each probe share the outer guard, and the signal is re-delivered only after the scratch is removed and every process group is terminated. The new test runs an extraction in a child against a fake lake that stalls while translating lakefile.lean, while building the helper, or during a probe, sends SIGTERM or SIGHUP, and checks that no process and no autoform-skeleton-* entry survives.
The lexical index keeps the first file that declares a name and records the rest in index.elsewhere, but only the module-mismatch reason used that record. A name declared in two files resolved silently to the first by path order, so which statement was reviewed depended on file names, and when the first declared it private the probe reported "not in the built environment; run `lake build`" against a complete build without naming the other file. The index cannot tell which declaration Lean binds, so a target name that more than one indexed file declares is now unresolved before any probe, with a reason that names every file in sorted order. A broken source passage on the same article keeps its own reason and appends the same list, so every reason given for such a name names the files. The index counts private declarations like public ones, so a public target that another file also declares private is refused too; the README states this. The elsewhere suffix on the module-mismatch reason is removed, since no name with several files reaches that branch. The new test declares Skel.dup privately in one file and publicly in two others, with and without a broken passage, and checks that no probe runs and the reason lists all three files.
Three probe nits: - signatureOf and rawSignatureOf printed at a fixed width of 100, so a signature between 101 and 120 columns wrapped where `#check`, which prints at the format.width option (120 by default), keeps it on one line. Both now print at the option's value. - A project module that declares a constant the helper also declares (all of them are in the AutoformSkeleton namespace) makes the probe's import of «autoform-skeleton-helper» fail with "environment already contains". The reason told the user to run `lake build`, which cannot fix a name collision. It now names the module and the constant and says the namespace is reserved by the probe's helper; the README documents the reserved namespace beside the reserved module name. - run_probe stabilized Lean's stderr with its own scratch directory only. The helper directory is the extraction's scratch and is on the probe's LEAN_PATH, so a search-path error carried a path that changed on every run. It is now passed to _stable_detail as well. Hash rotation: signature and raw signature text feed blind_text, so every DeclarationSkeleton.evidence_hash, NodeSkeleton.evidence_hash, and NodeSkeleton.review_hash rotates for a packet whose own or trusted signature has a line that wraps differently at 120 columns than at 100. The meaning hashes (DeclarationSkeleton.hash, NodeSkeleton.hash) are computed from kernel material, not printed text, and do not move. The autoform-skeleton/v5 schema is unreleased, so no released record is invalidated. Tests: a real-Lean signature of 115 columns prints on one line; a real module declaring AutoformSkeleton.main gets the collision reason without the `lake build` hint; a fake lake whose probe lists its search path yields a reason that shows the helper directory as <scratch>. All three fail on the parent commit.
The probe located a source's comments by parsing it with the root environment's token table, and withheld a source holding a known token shaped like part of a comment opener. Whether text is a comment depends on the token table Lean used when it compiled the file, which that environment does not match: a token declared later in the module, or in a module the file does not import, is in it, and a token such as `++"` or `++r` moves a string's quotes without any comment-like shape, so code read as a comment leaked author text into the blind packet. Adding token shapes cannot close that, and the shapes also withheld realistic sources whose tokens are harmless. A source is now shown only when the probe can prove it lexes the source as Lean did, `local` syntax aside. Lean does not record the table, so the probe reconstructs what the final environment proves of it, once per module and cached across declarations: - the table at a module's first line is exactly the builtin tokens and the global tokens of its import closure; - a token of a module outside that closure is absent; - a scoped token of the closure, or a token the module itself declares, may be present, unless the parser that declares it provably starts after the declaration's source ends. `ParserAttribute.add` records a parser's tokens just before its node kinds and the parser itself, so a token is placed at that parser's declaration only when the parser's definition spells it. Lexing depends only on the tokens that occur in the text, so the probe parses the source under the imported table extended by each subset of the uncertain tokens occurring in it (at most eight, or 256 tables), and removes comments only when every table under which it parses agrees on them. The true table is among those, so agreement proves the comment ranges. A statement is recovered the same way. This replaces substring rules against the root table (approach A) with a reconstruction of the compile-time table (approach B): A can only guess which tokens matter, while B decides lexing with Lean's own parser under every table the environment leaves possible. Sources of trusted declarations from modules with fewer imports than the root now parse with their own module's tokens, so notation the root imports no longer withholds them or changes their comments. Tokens declared after a source are proved absent and no longer withhold it; the same text under tokens that may be active is withheld. On the Adv fixtures trusted sources go from 15 shown, 3 withheld (LeakQ and LeakR leaking their comment) to 17 shown, 1 withheld, with no leak; statements stay 17 of 17. Residual: `local` syntax is recorded nowhere, and the probe's grammar is the root module's, so a `local` token, or a `local` or later-declared parser that reads raw characters after an existing token, can still change what Lean read as a comment.
The formatter escapes an identifier that spells a token as «», reading the token table from the environment. The probe's environment also holds the helper's imports, whose tokens include `throwError` and `register_option`, so a binder with such a name printed escaped in a module that imports only Init, unlike `#check` in a file importing only that module. Signatures now print with the token table the probe reconstructs for the root's module: the builtin tokens, the global tokens of its imports, and its own global tokens. A signature that changes rotates the evidence and review hashes of its declaration and node; the kernel-material hashes do not change.
To compile a file in the module system, Lean loads its imports and, through each loaded module, only what that module imports `public`ly, unless a chain of `import all` reaches it; `importModulesCore` applies those rules from v4.27 through v4.34. A private import of an import is not loaded, so its tokens are not in the file's table. The probe is a file outside the module system, which loads every module, and it took the tokens of the whole import closure as present, so text that Lean read as a comment in such a file could be parsed as code and shown with its comment. The closure the probe treats as certain now follows the same rules: every module imported directly or not for a file outside the module system, and the loaded set for one inside it. Signatures still print with the table of a file outside the module system whose only import is the root's module, which has the global tokens of everything it imports.
… to name headings check and render read different texts. An indented first statement line passed check as code, but render stripped the statement before boxing it, so the published page held it as raw HTML. A form feed, U+2028, or another line break Python reads but Python-Markdown does not hid HTML or a TeX definition inside a code line that the site later wrote out on a line of its own, and the "key: value" lines MkDocs takes off the top of a page (or YAML after a byte order mark, closed by "...") changed what the rest of the page parsed as. publishable_article now normalizes line breaks, returns that text for render to publish, and checks every piece the site can publish, as markdown.published_markdown gives it: each MkDocs reading of the page and the statement and notes inside the exact boxes render writes. The split, the box markup, and the fence walker moved from render.py to markdown.py, so both sides use one function, and the statement is no longer dedented. check and render both call render.publication_issues. attr_list stays configured for the site, but in articles it may only give a heading an id. publishable_article records every attribute list the site's converter applies, on the same parse it checks, and refuses any class, style, event handler, or other key=value, and an id on anything but a heading, naming the line. A heading id must match a conservative pattern, may not start with a prefix the site's own ids use, and may not be an id the site gives one of its own elements on the article's page (statement anchors and the "Additional formalization targets" heading). Testimony already renders without attr_list and the card body is raw HTML on the page; the attribute-list test now also converts a card inside its statement box with the site's converter and checks only the card's own classes appear.
render writes stylesheets/blueprint.css, javascripts/blueprint-mermaid.js, javascripts/mathjax.js, and assets/autoform.svg over the vault's copies. A directory at one of those paths was copied into the site and then crashed the write with IsADirectoryError; a file named javascripts crashed the mkdir; a FIFO would have hung the copy. check said nothing about any of them. A directory at tex-macros.json was silently ignored, and a symlink there was followed by check. in_the_way (mathjax.py) names the first path on the way to a regular file that is not a directory, or the file itself when it is not a regular file. publication_issues, which check reports and render refuses on, runs it for each asset render writes, and _tex_macros for tex-macros.json, so check names the path and render refuses before it copies anything. mathjax_script reads a kept configuration only when it is a regular file. Finding: config-7.
MathJax expands a macro by splicing strings: the body with each argument
in place of its #n, then the rest of the formula. A body or default that
ends in a single backslash joins whatever follows into one command, so
{"bs": "\\"} turned `\bs label{x}` into \label{x}, and
{"L": ["#1label", 1, "\\"]} turned `\L` into \label, past both the macro
check and the article check.
Where string splicing and token expansion differ: addArgs puts a space
between a command name and a following letter, so a name never runs on
into the letters after it, and neither the text before a #n (\# is a
character) nor an argument an article writes (the backslash takes the
next character) can end in a single backslash. That leaves a body or a
default ending in an odd run of backslashes, which _tex_macros now
refuses with a message naming the macro.
The node test runs the rendered script against MathJax 3.2.2: macros
that splice a command name or a #n before letters, or end in \\, do not
spell \DeclareMathOperator out of what follows them, and the refused
forms, written past check, do.
Finding: iso-tex-1.
MathJax reads its configuration from window.MathJax when it starts. A project script listed after javascripts/mathjax.js could assign its own there first, such as the snippet Material's documentation gives, and MathJax then started with it: ready() never ran, and one TeX input read every formula on the page, cards and all. A check at load() was too late for a project scaffolded with the bundle in mkdocs.yml, which starts before DOMContentLoaded. window.MathJax is now an accessor the script defines. It returns the site's configuration until MathJax starts, accepts exactly one assignment, MathJax itself holding that configuration, and ignores any other with an error in the console. The replacement never takes effect, so the page goes on to typeset as render wrote it; refusing to typeset would leave readers with raw TeX and keep nothing more apart. If window.MathJax cannot be defined (a script before this one made it unconfigurable), the script logs an error and loads nothing. The node harness gains a mode that assigns Material's snippet after the script is evaluated, for both the current and the old scaffold: the error is logged and each card is still typeset alone. Finding: iso-script-later-config-override.
render() typesets the articles and each read-back card as documents of their own, each with a TeX input that has read nothing else. MathJax's menu handler gives each document a menu of its own, so a menu action changed only the document that owned the clicked formula: switching the renderer from a card left the rest of the page in CHTML, and turning off assistive MathML or turning on the explorer from an article never reached the cards. Each document's menu now shares, with the menu of the document MathJax starts with, the renderers it has loaded and the defaults that first menu took before it read the saved settings, so a renderer loaded once is reused and a saved setting is told apart from a default the same way everywhere. When a setting changes, the menu saves it as before; once the change in hand is done and what it loads has loaded, the same setting is made in the menu of every other document of the pass. Settings are shared, inputs are not: each document keeps its own TeX input, and each formula is redrawn with the input that first read it. Details that the shared settings depend on: - The document MathJax starts with now has an input that finds nothing. Its menu renders it when it applies a saved setting, which typeset every formula on the page with one input before the first pass. - No document is made while a menu is loading a component. A menu that asks for a component already loading is never told it has loaded (MathJax drops the second callback), so documents wait for the menus' loads. The script waits on MathJax's map of loads rather than on a menu's loadingPromise, since asking for that promise makes a menu that loads an accessibility component skip redrawing. - MathJax.startup.output follows the renderer the reader chose, so the next pass, and a menu that remakes its document, use it. - Loading an accessibility component (the explorer, collapsible math) remakes only the loading menu's document with the extended handler. The other documents are now remade the same way, with the TeX input and formulas they had, so the explorer works on every formula. - A menu redraws its document at once and stops partway, with the formulas gone, when what it uses is not ready, such as the speech engine the explorer needs; stock MathJax leaves those formulas missing. After syncing, each document is rendered again with handleRetriesFor, and a retry thrown by one menu's setting no longer stops the others. - Each pass reset the renderer with clearCache, which only CHTML has, so after a reader chose SVG every page shown by instant navigation failed with "startup.output.clearCache is not a function" and was left as typed. The pass now calls reset(), which every renderer has. Not fixed, because stock MathJax 3.2.2 does the same on a page with one document: "Reset to defaults" logs "ContextMenu Error: Command of variable scale failed." (resetDefaults raises Menu.loading by hand, so setScale's redraw throws a retry), and the explorer's first redraw logs a MathJax retry from the loader. The node harness gives every document a menu with the interface the script uses, loads the real SVG renderer, and simulates the explorer load as MathJax's menu does it. Tests: a change from the articles or from either card applies to all documents, which share renderers and defaults, are remade by the current handler, keep their own inputs and formulas, and show every formula; the next pass starts in SVG; the startup document holds no formula; no document is made while a menu is loading. Checked in Chrome with the shipped template: renderer, assistive MathML, scale, explorer and collapsible from any formula reach all five containers, reload applies the saved settings to all, reset reverts all, and with navigation.instant the next page starts in SVG with the explorer on. Finding: iso-script-menu-per-document.
layout-mmltoken-color: base TeX's \mmlToken gives a symbol whatever attributes the formula writes. The site's ui/safe filter, with allow "none", drops the class, style, id, and href it could set, but it does not filter mathcolor or mathbackground, so an article could color a symbol like the site's status marks. Neutralizing only the color would mean a second filter beside MathJax's own, kept in step with every attribute MathML grows; refusing the command is one rule check already knows how to apply. So check refuses \mmlToken wherever the page's MathJax reads it, with the article and line, and tex-macros.json may not use it in a body or default. Cards already refuse it through the testimony allowlist. config-5: tests now fail when the safe filter's settings are loosened. A node test typesets an article and a card that each give a symbol a style, class, id, and href through \mmlToken, and asserts both outputs are a bare <mi>x</mi>; dropping safeOptions, or setting styles, URLs, classes, or cssIDs to "safe", fails it. config-6 (part): a test that \mathtoolsset is refused in an article. The README's validation section names \mmlToken with the other refused commands. Mutations: emptying ATTRIBUTE_TEX fails 4 tests; removing \mathtoolsset from STATEFUL_TEX fails 1; each safe setting changed to "safe", and the safeOptions line removed, fail the node pin test.
config-6: four guards in javascripts/mathjax.js survived their removal because the node harness never reached them. The harness gains a mode for each, and each has a test that fails without its guard: - Sequencing. The page's document now stops once on a retry, as a document does while a component loads, and meanwhile a reader picks another renderer, which the menu loads. Only the page's document may exist when that load ends. Replacing the reduce chain with Promise.all(steps.map(render)), or the wait on settled(), fails it. - The page step's processHtmlClass. A document made outside MathJax's startup reads an element of class mathjax_process wherever it is, inside a card too; the test puts one in a card and expects neither input to read it. Dropping processHtmlClass from the page step fails. - The output reset. A spy records one reset a pass, before the pass's first document; dropping startup.output.reset() fails. - The started-before guard. node-main starts a MathJax before the script runs; the test expects the "loaded before" error, no subscription to document$, and nothing typeset. Replacing the guard's condition with false fails. The comment on typeset() said an input registers what it can define under names every input looks up, the newest winning, and that this was why each document is finished before the next input is made. MathJax 3.2.2 does not do that: in node, a \DeclareMathOperator made through an input created before another stays in its own input, in either order of rendering, and with the page's document stopped until both cards' inputs existed, the articles still got their packages, macros, and operator. The order matters for the reason the harness now tests, the menu loads, and the comment says so. The \mathtoolsset refusal case, the fifth part of config-6, is in 8baadcb.
iso-tex-2: the page's TeX input read every text node outside the cards,
while check judged an article through its Markdown rendering. Text the
site prints as typed reached MathJax without check reading it as TeX:
a statement's title in its heading, the tree, the book navigation, and
the next-up link; a discussion: value; the hero lead; and a table of
contents and the navigation. A title such as
# Top `$\DeclareMathOperator{\leq}{>}$`
passes check, since the backticks make it code there, but the site
prints the title with html.escape, the backticks as characters, and the
page's input read the declaration and changed every \leq in the
articles on the page.
The fix makes one set of formulas the thing both sides read: the
elements pymdownx.arithmatex marks. markdown.FORMULA_CLASS names the
class. The page step's document gets those elements outside the cards
as its elements, instead of the whole page, and _RenderedText passes
check only the text inside them, which is what MathJax reads in them.
Any other text on the page is not TeX to either side.
What a reader sees changes in two places, both shown as typed now:
- TeX in a title or a discussion: value, wherever the site prints it
as HTML. This was never documented or tested, and no example vault
uses it.
- TeX in a heading as the table of contents and the navigation show
it. Material strips a heading's tags there, and its own recommended
MathJax setup does not typeset those either. The heading in the
article is typeset as before.
An escaped delimiter, \\( in the source, is text and not a formula, so
the refusal cases that used it now use a real \( and the escaped form
is an accepted case.
Tests: a page with TeX in a nav, a sidebar, a hero lead, a title, and a
Mermaid block has only its one marked formula read; a rendered vault
whose title and discussion carry a declaration passes check and keeps
\leq on the page; prose after a formula that names \newcommand is
accepted. Mutations that read the whole page again, drop the card
filter, judge all text, never end a formula, or rename the class each
fail a test.
layout-attr-list-imitation, a gap a74f66c left: superfences reads a
fence header in braces as an attribute list of its own, outside the
attr_list treeprocessor check watches. Every class after the language,
an id, and any other attribute land on the code block's element, so an
article passed check with
```{.text .bp-readback .bp-readback-current}
Approved.
```
which the site publishes as a div of class bp-readback, styled as a
card; with a style that covers the page; or with class mermaid, whose
text the site's diagram script draws with Mermaid's loose security
(iso-script-mermaid-loose-click).
_rendered_article now wraps the fence preprocessor's handle_attrs, the
one place braces are read, and records a header that leaves a class,
an id, or an attribute after the language. check names its line and
says to keep only the language. A header that only names the language,
as ```{.lean} does, and the options title, linenums, and hl_lines are
accepted, since they set no attribute.
Tests cover a card's classes, an id with a data attribute, a style, a
fence in a list and in a blockquote, and the accepted headers.
Mutations that unhook the wrapper, drop any of the three conditions,
or skip the fence message each fail a test.
iso-script-mermaid-loose-click: the site's diagram script drew every div.mermaid with securityLevel "loose", which its graphs' click links need. Loose mode also runs a diagram's `click X call fn(...)` as script and draws its labels as HTML, so a ```mermaid fence in an article, which superfences turns into that div, could run script on the site and draw nodes in the status palette. Render's graphs now carry a marker only render can produce: each is written as raw HTML, <div class="mermaid bp-graph">, and the script draws div.bp-graph and nothing else. No article can make that element, since raw HTML, attribute lists, and fence braces that set more than a language are all refused (a74f66c, f6bb94d). An article's own Mermaid is refused by check rather than drawn in strict mode. Strict mode would still let an article draw boxes in the colors the site uses for status, it rests on Mermaid's sanitizer, and a diagram in an article is testimony nobody can read back the way a card reads. check finds it in the renderer's own output (a div of the mermaid fence class), names each fence's line, and says to show the source in a ```text fence. Mermaid shown as code is accepted. Labels could carry HTML into the loose render: a node's title is the raw H1 text, code spans included, and Mermaid draws labels as HTML, so `<b style="position:fixed">` in a title reached the page. Titles in labels and tooltips are now written with Mermaid's entity codes (#quot;, #96;, #amp;, #lt;, #gt;), which it shows as typed. Links could carry script too. A click's href is made from file and folder names: a node file named `t";click n0 call alert(7);click n0 "op.md` ended the string and added a call, and a chapter folder named `javascript:alert(7)` made a sibling chapter's link a javascript: URL, which loose mode opens as is. Hrefs are now percent-encoded, so each stays one string and a relative path to the same page. Tests: check and render refuse a diagram in an article (fenced with backticks, tildes, braces, in a list, in a blockquote), and one that imitates render's graph class; code shown as text passes; render writes each graph marked, and the site converter keeps its click lines; a node harness runs the shipped script against a fake DOM and Mermaid and sees it draw only the marked graph, in loose mode; titles and links are escaped in the project view and the vault copy. Mutations that drop the marker, widen the selector, unwrap any of the three graph sites, drop any label escape or the href encoding, or weaken the check's detection or line search each fail a test.
A formula's containment came from a CHTML-only, Material-only selector and from contain: paint. With the SVG renderer the MathJax menu offers, or under another theme, nothing held an article formula: it could paint over a card, a status mark, or the lines around it (layout-svg-renderer-uncontained, config-2). Where it did apply, contain: paint cut off the ink that \rlap, \llap, and the mathtools laps put beside a formula's box, and every glyph that rose above it (layout-lap-clipping). Now every mjx-container, whatever its renderer, clips only vertically, to its own box plus the slack its glyphs need, which a negative margin gives back; inline formulas become inline blocks so they have a box to clip, and each formula is the containing block of what it positions. Across, ink stops at the edge of the paragraph, heading, list, or table cell that holds an article formula, so a lap keeps its ink inside its block and nothing reaches the navigation beside the text. A display scrolls inside its own block. The display selector outranks MathJax's own sheets, which are added after ours. A card too wide for the page, or a formula in it, scrolls, and a shade at an edge now shows there is more that way: shades fixed at the edges, under covers in the review panel's color that scroll with the content (layout-card-scroll-no-hint). The covers use Material's panel color, since in the dark scheme the panel is not the page's color. A card's approval label wraps on a narrow screen instead of running past it, where a hash was cut off at 360 px (layout-summary-clip-360). Checked in Chrome 151 at 360 and 1280 px with CHTML and SVG, under Material and the mkdocs theme: no article formula paints outside its band or block, laps keep their ink, the label shows every character, and the wide card's shades appear at the edges it can scroll toward.
Material caps every svg on a page at its container's width. With the SVG renderer the MathJax menu offers, that shrank any display or card formula wider than the column until it could not be read, instead of letting it scroll: the wide card formula in the test site was drawn 627 px wide and 8 px tall at 1280 px, and 267 by 3 px at 360 px. On a phone, where Material makes a display's box as narrow as its content can be, every display without a tag shrank to 1 px and vanished. This is stock Material with MathJax's SVG output and does not depend on the containment rules; it turned up while checking them in Chrome. A formula's svg now ignores the cap, so it keeps the size TeX set and scrolls, or is cut at its block's edge, as a CHTML formula does.
Main brings PR #52 (skeleton golf, its compatibility fixes, the legacy v1 tree replacement) and the pyjwt/urllib3 lock bumps. The merge keeps #52's structure and re-expresses the stack's behavior on top of it. skeleton.py: #52's DeclarationSkeleton inheritance, _report_entry and _report_value readers, and canonical to_json round-trip in load_skeleton_report replace the field-by-field loader. The stack's schema family message, module-keyed trusted and semantics tables, and SkeletonReport coherence checks stay; hand-rolled count, hash and unreferenced-entry checks are now covered by the round-trip ("not a canonical ... report"). _run_registered_command uses #52's check_output poll loop with the stack's pool cancellation raised inside it, so #52's teardown path handles it. _stage_output takes #52's (destination, content) form plus the stack's stages registry, registering each stage before it is created and retrying name collisions; OutputTransaction drives write_packets and write_skeleton_report through #52's _output_path and manifest loop. declaration_filename keeps its suffix validation with #52's quote() encoding. The stack's public atomic_rename supersedes #52's _rename_no_replace body. _validate_managed_output is #52's single test, plus the exact-schema parameter and the refusal of a symlinked manifest. source_passage stays in graph.py; #52's copy in skeleton.py is dropped. #52's fixes are kept: the rollback restore past a swapped symlink, the missing-fragment SkeletonError, legacy v1 tree replacement, and the restored compatibility APIs. skeleton_probe.lean: the stack's helper module, token tables and per-root error records, with #52's golfs: leafJson, a SemanticCache holding the output handle, merged defn/opaque arms, signatureOf with a raw flag, and emitShared marking an entry only after it is written. lean.py: #52's form, plus the stack's scan cut-off, stage pruning, REVIEW_PACKET_SCHEMA export, ignored output schemas and SourceIndex.elsewhere. Tests: every test from both sides is kept and adapted (_fake_default_probe for the per-module runner, the probe fixture plus the helper olean, _assert_load_rejects, nested shared tables). The probe-record test expects the helper's `finally out.flush`, and test_readback builds its __slots__ copies with dataclasses.replace, since the slots of DeclarationSkeleton no longer list the inherited fields. The stack's test_extraction_rejects_lake_configuration_changed_during_probe is removed: it is exactly the lake-configuration case of #52's parametrized test_default_extraction_rejects_input_changed_during_probe.
The merge of main into the stack left five blank lines that neither parent has (findings N1 and G3): one inside SkeletonReport._incoherence after the selection-mode check, and four in the probe (after the defnInfo/opaqueInfo arm of meaningConstants, a second blank after emitShared, one at the top of the boundary-module emitShared block, and a second blank before `end AutoformSkeleton`). They came from conflict hunks resolved by hand. Delete them so each hunk matches the parent it came from. No behavior changes.
Main's skeleton golf (#52) made _stage_output allocate its stage in one attempt: the name carries a 64-bit random token, so a collision is not a case worth a retry loop. The merge kept the stack's 100-try FileExistsError loop and its "cannot allocate a stage" error around #52's unified directory-or-file body (finding G2), so the loop came back as dead code. Allocate once, as #52 does. The stack's hardening stays: the stage is registered in `stages` before it is created, so its owner removes it however a later step ends, and a FileExistsError takes it back out of `stages` before propagating, so a name collision never removes a foreign path. The mode inspection keeps its SkeletonError. Behavior is unchanged for every non-colliding name; a collision now raises FileExistsError, as on main, instead of retrying.
test_shared_probe_tables_keep_every_hash failed with the real Lean toolchain on the stack and on the merge (finding G1): it pinned 3db5dbb9...6238, the digest main and the merge base produce, while the stack produces 9dad08e8...020a. The CI job that runs tests/test_skeleton.py against the fixture toolchain would fail on it. Root cause: 5859e05 ("Print signatures at format.width ...") prints signatures at the format.width option (120) instead of a fixed 100 and documents that every evidence and review hash of a packet whose signature wraps differently rotates, while meaning hashes do not. It did not refresh this golden, whose comment says it records intentional changes to the packet evidence. Dumping the hash table on main and on the merge shows exactly that rotation and nothing else: only the evidence_hash of Skel.Kinds.usesWf, Skel.heavy_of_notation and Skel.heavy_of_weight (their signatures now print on one line) and the Skel node's evidence_hash and review_hash differ; every meaning hash and the whole Skel.Semantics run match. Pin the stack's digest.
markdown-table-cell-bound-bypass: _testimony_limit_errors split the testimony on "\n" alone, while Python-Markdown's NormalizeWhitespace turns "\r" and "\r\n" into line ends. A 9 KB testimony whose table rows ended in "\r" met every pre-parse limit, so the write path rendered its million cells and refused it only at the rendered-size backstop, after 3.4 s and 317 MB. The line limit was open to the same separator. The table bound itself came from a hand regex that mirrored TableProcessor.test, a copy that could drift from the library. The limits now read the lines the renderer's own normalize_whitespace preprocessor produces, so the line and nesting limits see "\r" and tabs as the renderer does. Tables are found by the testimony converter's preprocessors and block parser, with a TableProcessor subclass that counts each row's cells at the header's width instead of building them. The block parser reads no inline markup and runs only within the byte, line and nesting limits, which bound it. The hand regex is gone. The before-parsing test now forbids Markdown.convert rather than constructing a converter, forbids the block parser for the byte, line and nesting limits, and bounds CPU time and traced memory; it gains the "\r", "\r\n" and pipe-only table variants and the "\r" line-limit variants.
The round 4 audit found the MathJax differential guards for \\* and \limits in a group skipping under the standard runner. tests/test_testimony_mathjax.py wanted AUTOFORM_MATHJAX_DIR to name the es5 directory, while tests/test_site_math.py joined "es5" onto the same variable, so no one setting ran both, and suite.sh, which sets the package root, reported the revert guards as skipped. Each file read the variable on its own, and the skip reasons did not say which half was missing. tests/mathjax_package.py is now the one place that reads the variable. It accepts the package root only, the directory holding package.json and es5/, since the tests check the release against package.json and a second accepted form is how the two conventions came apart. It skips, naming what is missing, without Node.js or the variable, and fails when the variable names the es5 directory (pointing at its parent), something other than a MathJax package, or another release, so a run meant to check MathJax cannot pass by skipping. Both test files take the package root and Node.js from it, and the site harness gets the resolved root in its environment rather than reading the variable itself.
Five review CLI tests spelled out the same prepare and record argv. _prepare_and_record runs them with the same flags, still asserts that prepare succeeds, and each test keeps its own assertions on the record.
Eight sites added or replaced review_approved by hand, by str.replace or re.sub. _approve does either edit, writes the same text, and asserts that the article changed, so a drifted fixture cannot pass silently.
Five batch tests wrapped publish_readback in the same closure that publishes a card and then runs an edit. _after_each_card installs that wrapper and returns the real publisher; each test keeps its own edit.
_record and the prepare filesystem-error test listed one flag per line. The argv lists hold the same strings in the same order; only the line breaks moved.
Seventeen sites read an article or card, replaced one string, and wrote it back. _edit does the same replacement and also asserts the string was there, so a drifted fixture cannot turn a test into a no-op.
Four review test files spelled out all seventeen DeclarationSkeleton fields. tests/skeleton_fixtures.declaration builds the shared defaults and each file passes only the fields it changes, so every test gets equal values.
Two tests ran the batch in a thread, released any FIFO it blocked on, and asserted it had not blocked. _record_without_blocking does that and returns the exit statuses; each test keeps its own assertions.
The nested-manifest test and _damage_bundle built the same texts as _undecodable_json, and the number test repeated its skip. They now call it, so each case runs the same input and skips where it did before.
Conflicts: - autoform_cli/__main__.py: keep main's one-line project import (#154) and this branch's readback, render and review imports. - autoform_cli/graph.py: take the union of the imports, main's lean import (#158) beside this branch's markdown and snapshot imports. Semantic: - tests/test_audit.py: since #158 a formalized proof without a formalized statement fails to load, and the audit's proof-without-statement finding is gone, so the snapshot test's rewritten article now reports invalid-graph. The audit of the state the graph loaded is unchanged.
This was referenced Oct 6, 2026
Deicyde
added
blocked
Deicyde
marked this pull request as draft
October 6, 2026 17:11
Contributor
Author
|
Correcting the public status while the dedicated worker completes its restack: current head |
This was referenced Oct 6, 2026
test_testimony_mathjax.py typeset a corpus with MathJax 3.2.2 under Node.js and compared the result with readback._TexLayout. No CI job provides Node.js and the MathJax package, so it skipped on every run. It moves to a follow-up that adds that job. tests/mathjax_package.py stays for test_site_math.py; its docstring no longer names the file.
Since 164f26e replaced read-backs with verified review bundles, the review check reports cards through autoform_cli/review.py: review_findings reports missing and invalid cards (through _article_readback_findings) and orphaned ones. readback_findings and its ReadbackFinding were left behind with only tests calling them, so delete both, and Readback.status, whose only caller was readback_findings. The module docstring now says what happens to a card whose hashes move: it is reported and rendered invalid. The read-back tests that checked missing, invalid, altered, and orphaned cards now run through review_findings, via a _findings helper in tests/test_readback.py that builds the review bundle for the fixture blueprint and fails if evidence findings would hide the read-back ones. The stale and revised cases now expect readback-invalid naming the hash that moved, which no test checked on the production path before. The Readback.status assertions are deleted.
Single-article `autoform review record` is unchanged: the same checks before Lean (bundle entry, packet bytes, testimony size and FIFO refusal, gone article_id, card conflicts, platform), the reload after extraction, the re-read of the article before the card is written, and the same error messages, exit codes and output. Removed: `review record --manifest`, the records manifest schema and loader (RecordRequest, load_record_manifest, REVIEW_RECORDS_SCHEMA and their path checks), the per-article scoping of a shared extraction, the "N of M filed" reporting, and the manifest wording in refusals. The record flags are required again, so a missing one is argparse's usage error. The README, the human-review skill and the readback docstrings no longer describe batches, and the batch tests are removed or rewritten as single records. Batch filing moves to a follow-up PR.
The site's MathJax script made a setting changed in any formula's menu apply to every document of the page and to the pages shown after it, by sharing renderers and defaults among the menus, replaying each change in every other menu, and remaking documents when the explorer extended the handler. That machinery is gone, so the menus behave as MathJax's own do. Each document has its own menu: the page's articles share one document and each card gets its own. A setting changed in a menu applies to that document's formulas, and MathJax saves it, so documents made later, such as those for the next page shown, read it back; documents already on the page keep their settings until then. What stays from the same change: the document MathJax starts with reads nothing (SETTINGS.startup), no document is made while a menu is loading (settled(), which now finds MathJax's map of loads through the startup document's menu), and each pass resets the renderer with reset(), which every renderer has. The menu-sharing test, the harness's simulated menu settings and explorer, the SVG renderer it loaded, and the README sentence on shared settings go with it.
The site's MathJax script compared window.MathJax with a snapshot of its configuration before fetching the bundle and when the bundle started, refused to start MathJax on any difference, and then started MathJax on a fresh copy whose startup, pageReady, tex and options parts could not be reassigned. That snapshot comparison and those property guards are gone. A script listed after javascripts/mathjax.js that mutates the configuration in place, such as one that sets window.MathJax.startup.pageReady, is no longer refused and MathJax reads what it set. What stays: window.MathJax is still an accessor, so assigning a new object there, such as the snippet Material's documentation gives, is ignored with an error in the browser console, and MathJax replaces it only with itself. The harness's mutation and proxy cases, the tests for them, and the README text on refused changes go with it; the harness configures node's MathJax directly again.
This was referenced Oct 7, 2026
Every extraction started a Lean process to compile the probe helpers, although the compiled module depends only on the toolchain and the helper source. Cache it under $XDG_CACHE_HOME/autoform/probe-helper, keyed by the toolchain's Git hash, the size and modification time of its Lean.olean, and the source, so later extractions with the same toolchain spend one `lake env` call and a copy instead. An entry holds the module followed by its SHA-256. An extraction copies an intact entry into its own temporary directory. A damaged or unreadable entry is a miss, and so is anything at its path but a regular file, or a module whose header lacks the toolchain's Git hash, which a toolchain change during a build can publish under the old toolchain's key and which Lean would refuse to load. Like Lean's own check, this misses a change between two toolchains built from the same commit. On a miss the helpers are compiled again, and the build replaces the entry unless a directory stands in its place. A fresh entry is written under a temporary name with the build's file mode and renamed into place, so another extraction reads the old entry or the new one. The helpers are still compiled every time when `lake env` exits with an error or lacks the Git hash, the toolchain library, or the search path, when the cache directory is not absolute or cannot be written, and when a search-path entry already provides a module or directory named like the helper, so the build's check still names it. The lookup drops an inherited LEAN_GITHASH, which Lake would report in place of the toolchain's own, and shares the helper's timeout with the build, so a lookup that times out stops the extraction as a build does. Each probe runs the helper's code, so a process that can write the cache can run code in later extractions in any project. The trust section now says a sandbox for an untrusted project must deny writes to the cache directory. Tests share one cache directory per session, so real-Lean tests after the first reuse the helpers as later extractions do.
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.
Moved from #40 (closed), whose head branch lived on VivienCabannes/autoform-bot. Review continues here. The review of 765f2cb and the earlier discussion stay on #40; "Changes since 765f2cb" below lists what changed after that review. Supersedes #39 (closed) and #42 (closed; its batch filing moved out after 7038b46, see below). #12 is already in main.
The branch fast-forwarded from 765f2cb to 61432cf, an
oursmerge that keeps 765f2cb reachable and changes no files; its five commits reappear as 3861e4e, e6cbb59, d43d5d8, 164f26e and c63119f. At 9d9005b the branch is 357 commits over main 7fa6d1d, a count that includes 765f2cb's five original commits. Squash on merge.Architecture
autoform review prepare blueprint --lean-root . --output review.json --packets DIRwrites anautoform-review-bundle/v1bundle from fresh Lean extraction: statements, cited passages, declaration mapping and packet bytes. Blind packets are named by their SHA-256. Anorigin: citedarticle without an in-vault source and exact#L<start>-L<end>range is refused.autoform review recordfiles one read-back. It rechecks the article and exact packet bytes, reads the article again just before the card is written, and writes anautoform-readback/v1card. Replacing a different card requires--expected-card-hash.autoform review check,audit --reviewor--review-bundle, andrender --reviewre-extract Lean (review checkandrendermay instead read a skeleton report with a matching blueprint hash) and judge articles, cited sources and cards as one snapshot; a concurrent edit fails withreview-snapshot-changed.review_approvedrecords the hash of the full review surface: it shows the surface is unchanged, not who approved it.review check --authenticate githubandreview authenticate --githubauthenticate an approval only when an individual code owner approved that hash under rulesets the token cannot bypass; other current approvals are labelled self-approved.blueprint/.autoform-review(new scaffolds commit it).autoform-verify.ymlrunsreview check --lean-root .on a bundle derived in the same run,autoform-review-gate.ymlrunsreview authenticate --github --pragainst the merge commit's base, andblueprint-pages.ymldeploys only a build of the default branch's current head.Untrusted-output boundary
Read-backs are model output shown on the site and GitHub, so
review recordrefuses testimony that could hide text, run code, or read differently in the two:\phantom,\colorand macro definitions are refused by name), more than 8 em of spacing per formula or 64 em per read-back, invisible characters, and more than two stacked accents. Text between two dollar signs that the site or GitHub could pair as a formula is held to the same rules and may not hold a percent sign;[, unread.The site loads MathJax with
ui/safeand allows no URLs, classes, IDs or styles; Mermaid draws only render's own graphs; render copies only images, PDFs and plain text fromblueprint/.Changes since 765f2cb
graph.childrenscans this PR's render and page code added with one containers set, as views: build scope views from one shared index per publication #99's scale test requires. adefd5f keeps this PR'sautoform-skeleton/v5schema and Harden project compatibility inspection snapshots #79's pinnedtomliparser. 3b0c648 keeps Replace orchestration with a Markdown formalize frontier #92's nested-checkout skip beside this PR's packet-stage skip in the Lean source walk, and drops_inject_after_lead, whose only call this PR had removed. 53b2547 keeps the probe per root module and names that module in Name exact Lake targets in skeleton guidance #128's reason for a declaration missing from the built environment, and moves the example's review-gate workflow, which only this PR has, to Refresh the bundled example Autoform pin #116's pin with the example's other workflows. 966b3b8 takes docs: simplify README for users #133's shorter README and keeps this branch's Intel Mac requirement, the Xcode Command Line Tools that compilecmarkgfm, as a sentence after its one-line requirements. 0072893 drops the two assertions that required the README's deprecation note, which e54e5ab removed; main's own run of that test fails at e54e5ab. 7c8c21e takes Bind Lean source snapshots to filesystem generations #95's snapshot model for the Lean source walk with this branch's#exithandling, review-packet schema, output-stage exclusion andelsewheredeclarations; shares Report Lean revision impact and deprecated targets #136's labelled probe runner, building this branch's helper module only when a probe imports it, so the impact probe skips it; dropsblueprint/javascripts/mathjax.jsfrom Create Lean projects atomically with catalog-backed defaults #96's required templates and adds the review marker and the review-gate workflow; and passes an explicitautoform_refin this branch's workflow tests, since after Create Lean projects atomically with catalog-backed defaults #96initomits the workflows on a commit no remote-tracking ref contains. b570d51 keeps both new frontmatter keys,review_approvedandopen_statements, and takes Add opt-in open statements and conditional proof status #138's retraction model, which keepslean:. Only Formalize changeslean:under it, so the rule that a commit dropping a declaration fromlean:deletes its read-back cards, and one removinglean:removesreview_approved, moves from the Roadmap skill to the revision contract in the CLI reference. 7038b46: since Reject formalized work the Lean cannot back at load time #158, a formalized proof without a formalized statement fails to load, so the snapshot audit test now expectsinvalid-graph.blueprint/.autoform-review, Formalize runs the--reviewaudit after the default build and hands each newly formalized statement to Human Review, whose read-backs and approval the review gate waits for; Human Review hands a rejected statement to Roadmap. The CLI reference names the commands that needarticle_idon every Lean-mapped article, and says that another article's empty or duplicatedlean:list stops every record until it is fixed.cmarkgfm==2025.10.22has no Intel-macOS wheel, and no release has one for Python 3.13, so an older pin does not help. A second lock test fails onceuv.locklocks a cmarkgfm release with an Intel-macOS wheel, so the source-build exemption is dropped when one ships.uv.lock. The old 9.6.21 pin cannot resolve beside pymdown-extensions 11.0.1, so the step failed in every generated project. A test now holds each pinned package thatuv.lockalso locks to the lock's version, except mkdocs-literate-nav, kept at 0.6.2 below the lock's 0.6.3; it does not run a resolver.review checkwithout--bundleandrender --reviewvalidate the bundle they derive, asreview preparedoes, so a source passage of only blank lines is refused instead of published as an empty box. The test runs all three commands on an empty and a whitespace-only line.[nested deeper than the JSON decoder goes (about 1,000 levels on Python 3.10 and 3.11, 10,000 on 3.12 and 3.13, and from 3.14 as deep as the stack allows, about 37,000 in 8 MiB on macOS arm64) give areadback-invalidfinding instead of a RecursionError; the test coversarticle_id,declarationandmodelwith 100,000 levels. A review bundle nested too deep to decode is refused as unreadable instead of a traceback, and atex-macros.jsonnested that deep is reported as not valid JSON (1eebf92). A review bundle holding a number too long to convert to an int, or an escaped lone surrogate, is likewise refused as unreadable:review check,audit --review-bundleandrender --review-bundleraised either as a traceback, andreview recordreported it without naming the file (8aac064, 1d168bf). An unreadable bundle exits 2, or 1 fromrender. The bundle andtex-macros.jsonnesting tests skip where a Python 3.14 stack decodes 100,000 levels, and the long-number test writes one digit more than the interpreter's limit and skips where there is none (c3ca39c, 995da76). The lone-surrogate test checks the whole report (40fefee).review record, a card another writer files while Lean runs stops the record before it writes. Deleting theAUTOFORM_REVIEW_ENABLEDgate from a statement review step in any of the three generated workflows, in the template or the bundled example, fails a test. Testimony tests cover\(...\)delimiters in a code block, list markers (-,+,*,1., and1)in a code block) in the nesting count, an invisible character before the first parsed text, and one case each that only MathJax's pairing or only the every-dollar reading refuses.$$inside emphasis is now doubted too. Every spaced form in the review and its follow-up is refused;So $ P \land Q $ holds.is still accepted.US$5 and $P \color{white}{\land Q} $is accepted, as is$ P $ \color{white}{Q} $ R $. Dollar signs in code, backslash runs split across elements, and\beginenvironments are not modelled. GitHub's rendering of a card was never observed, so all three readings are models of it.Costs \$5 for $x$ and 50% for $y$.is refused. Dollar signs meant as typed go in code, and the read-back guide no longer offers\$for them (a3b0f99).article_idis no longer in the blueprint, because its article was deleted or given a newarticle_idafterreview prepare, is reported as that blueprint edit instead of as a bundle missing a declaration or a card conflict, with what clears it: take--article-idfrom the packet manifest a newreview prepare --packetswrites and drop any--expected-card-hash; if that manifest names a different packet for it, the record must name that packet, and its testimony should be written from it, which the record cannot check (766b262, f25f485, 5d99ded). A platform that cannot publish is refused first (79691ed). The partial-batch message and the interrupt between cards (7d6aa4b, 94f92ac, 91751e7) moved out with batch filing. The same edit made while the record's extraction runs is reported as a blueprint change during extraction, and running the record again names the record (18b62b4); the README adds that a rerun after the evidence of a recorded article changed then reports it as differing from the prepared evidence (bbe8305). A refusal while publishing a card names its declaration, as the check before Lean does (45f1cfe).review prepareif the change is to the evidence; a deletion is reported as one, with advice to restore the article (766b262). An article that cannot be read is named with its record and the cause, and one left as a link to a missing file is reported as that (ae17709). The article is opened without waiting for a writer: one replaced after the reload by a FIFO, a directory or a device, or by a link to one, is refused unread as no longer a regular file, with the advice given for a deleted article, where the re-read as first written waited on a FIFO until the record was interrupted (12f7847). Tests cover an article longer than one 64 KiB read and one made a link to/dev/null, and the FIFO test fails rather than hangs when the record is held past its open (1cd3e05, 4477ee5, c9d025d). An edit after that read, while the card is written, still goes unseen; the README says so.\r\nas one byte, as read-back validation measures it. A larger file is refused before Lean without being read whole (for a 64 MiB file the test checks it is read to one byte past twice the limit and holds tracemalloc's peak under 2 MiB), a testimony saved with CRLF that is within the limit as text is filed, and one over it is refused by one message naming the file.tests/test_render_review.pywrites its invisible characters as escapes.audit --review --lean-root .derives the review evidence asreview checkdoes, so its review findings are the onesreview checkreports;--reviewand--review-bundleexclude each other, as inrender. With neither, the review-bundle-missing reason names both.lean:target of its article, and the helper build only when the helper is not cached: with a warm cache, 1 Lean process for a card whose article's declarations sit in one module, 2 when they span two. The helpers are built apart from project code (8103b0c), and each module gets its own probe (ca34f0c) so a packet reads as it does to a file importing only its module, whatever else is extracted. Folding the modules into one probe saved a start but changed packets in 3 of the 6 tests that guard those properties, with no finding in the report. Importing the modules in process neededenableInitializersExecutionand about 2.6 GB. 9d9005b caches the compiled helper under$XDG_CACHE_HOME/autoform/probe-helper, keyed by the toolchain's Git hash, the size and modification time of itsLean.olean, and the helper source. An extraction uses an entry only if it matches the SHA-256 stored with it and its module header names the toolchain's Git hash, and copies it into its own temporary directory. Any other entry means the helper is compiled again, which covers a damaged entry and one that a toolchain change during a build filed under the old toolchain's key; like Lean's own check, the header check cannot tell apart two toolchains built from the same commit. Deleting the cache is always safe. The lookup ignores an inheritedLEAN_GITHASHand shares the helper's timeout with the build; the helper is compiled every time whenlake envexits with an error or its report lacks the toolchain, its library or the search path, or when the cache directory is not absolute or cannot be written. A one-module extraction of the fixture project took 8.2 s with a warm cache against 18.9 s cold, on a heavily loaded machine. Each probe runs the helper's code, so the trust section says a sandbox for an untrusted project must deny writes to the cache directory that extractions outside the sandbox use.check,audit,renderand every review command hang, and a case alias of another chapter's README.md flattened that chapter into the root. A README.md link above the roadmap that leads back into it no longer hangs every command either. Both hangs predate the branch on main. A roadmap directory that cannot be listed, or a page that cannot be checked, is named instead of dropping its articles or raising; one unreadable page no longer hides a chapter without a README.md; and the chapter check skips a linked chapter, as the walk does..md.mdpath that does not exist, and adefarticle whose target is anirreducible_defno longer getslean-target-kind-mismatch.doctor, which cannot be given review evidence, leaves approvals out of its roadmap audit; a plainauditreports missing review evidence once instead of once per approved article; and article shape is checked without agraph.childrenscan per article.review record(d14f545, ad2f9a8, 93eb15c, d63c684, 3711f92, 5be882a, 5669124, 3a73910): a FIFO at a packet or testimony path is refused instead of waited on; an article replaced by a socket or a looping link gets the advice for one that is no longer a regular file; a named card that is gone is reported as "found no card" instead offound None; a gone single record is told which flags to change and thatreview preparewrites a packet manifest only with--packets;review checknames the card file to delete when a card is left under a gonearticle_id; the README says a run that names a gone record lists no card conflict; and a refusal no record can reach is removed.Readback.shows_what_it_attests, the read-back labels a validated card cannot reach, two pass-through wrappers inskeleton.py, andwrite_readback, which only tests called and which moves into a test helper. The review bundle is written through scaffold's_atomic_write,atomic_renamefolds into_rename_no_replace, and planned and prepared record cards are built through one helper. Two details change: on Windows the review bundle is written with LF line endings, as on other platforms, and a rename refusal no longer chains aNotImplementedError.review record --manifest(d6d8d16, by ArmelRandy, and the batch parts of items 4, 6, 7 and 8), goes to a follow-up PR, not opened yet. Until it lands each card is its ownreview recordrun with its own extraction, so the record half of Add verified statement-review bundles #40's blocker 6 is open again: an article with N declarations takes N runs of at least one Lean process each, two while the helper is not cached.javascripts/mathjax.jsthat changeswindow.MathJaxin place is no longer refused. Assigning a new object there is still ignored.readback_findings, which no production code called; its tests run throughreview_findings, and a card filed for an earlier declaration is now tested on that path.Open
skills/setup/assets/cabannes-thesis-project) still runs Autoform at c994d83, which has noautoform_cli.markdown:FormulaExtensionfor itsmkdocs.ymland none of the review commands. The repository contract asks for a full SHA on canonical main that contains the behavior, so the pin, its substitution assertions and a run through it follow this PR's merge commit instead of pinning a branch commit that a squash would orphan.Validation
At 9d9005b. GitHub Actions push run 37603809732 passed
test (3.10),test (3.13),real Lean (fixture toolchain)(its skeleton step took 13 of its 25 minutes, against 18 at ea7befe; the tests now share one helper cache) and the Windows inspection, subprocess, and publication hardening job; no pull-request run starts while the PR conflicts with main. Locally, the test runs below are for 329ad626, which differs from 9d9005b only in two docstrings:uv sync --frozen --extra dev --extra repl):pytestgave 3675 passed, 93 skipped and 1 xfailed on each;ruff check autoform_cli servers testsandmake check-examplepass on both at 9d9005b.tests/test_skeleton.pyandtests/test_project_inspect.py::test_stale_inherited_mathlib_is_ignored_by_real_lake, 272 passed;tests/test_impact.py, 73 passed;tests/test_lake_artifact_audit.pyandtests/test_contract.py, 76 passed and 1 skipped.tests/test_site_math.pyagainst MathJax 3.2.2 (AUTOFORM_MATHJAX_DIR), 292 passed.