Repository navigation
Conversation
…tore
scripts/atlas/build_store.py turns one sealed record set from the
formal-companion locate pipeline (SEAL.json, universe, sources.jsonl,
records/<source-id>.jsonl, receipts/) into the tree the Worker will read:
atlas/v1/{current,manifest}.json, universes/<sha>.json, articles/<pageid>.json
(a compact per-article view model), records/<pageid>.jsonl (verbatim) and
hash-sharded index/<shard>.json.
It refuses a set whose files do not match SEAL.json, any record that fails
the vendored Literature Links 2.0 schema (through the existing
site/native_annotations checker, after pinning the schema sha), and any break
of the locate contract: proposal 2.7 record shapes, one lean end per universe
library on an absence, object [] on an unresolved passage, quote caps, unique
location keys, ranks, and the necessary conditions of the derived status.
Output is canonical and deterministic; --check rebuilds in memory and
compares byte for byte.
The hand-built fixture (two synthetic articles covering an exactMatch proved
Mathlib theorem, a FormalFrontier closeMatch, a statement_only TauCeti
declaration, an absence and an unresolved passage) and its golden store are
pinned by scripts/atlas/test_build_store.py, now run by ci-python.sh.
scripts/ is release-neutral.
The formalization atlas is a separate read-only data plane: the Worker reads
the store built by scripts/atlas/build_store.py through an AtlasReader over
the optional R2 binding ATLAS (Env type only; no bucket is added to
wrangler.jsonc). KV and static-asset readers exist for the open backend
decision, and tests use the golden fixture store through an R2-shaped fake.
Unbound, every atlas route answers 503 "atlas store not configured".
Routes: GET /atlas (totals by derived status, library and WikiProject
importance; article list searched through the index shards), /atlas/:pageid
and /atlas/:pageid/:slug (one article's coverage), /atlas/universe/:sha, and
/api/atlas/{current,article,records,universe,index}. The coverage page has a
strip with filter chips and per-passage blocks: quote, section, kind, a status
pill with a full-sentence tooltip, one card per location (library, short
commit, relation, prominent proof status, namespace-faint name, a pinned
"Source @sha7" blob link from the library registry in libraries.ts), checked
absences naming the searched universe, and undecided passages. Rendering
escapes everything server-side; atlas.js uses textContent only and there are
no inline handlers. Status is never colour alone, dark mode uses style.css
tokens, and the browser soak runs axe in both schemes.
Article pages get a summary box injected per request, never in the cached
base page, so render:v18 bytes are unchanged and need no bump.
Migration 0015 adds atlas_feedback. POST /api/atlas/feedback is session-only,
same-origin, byte-capped, rate limited on EDIT_LIMITER, validated against the
current store (409 on a stale campaign), and 503 until 0015 is applied.
GET /api/atlas/feedback/export streams rows to the pipeline bearer under
research-export pseudonyms, for benchmark seeding.
/atlas stays in RESERVED; retired-routes no longer expects /atlas to 404.
Release-affecting: ships only in a release.
docs/ATLAS.md records why the atlas is a separate plane, the sealed record set contract and the checks the builder applies, the contract notes formal-companion must agree to (the CSL citation id the schema requires, section/prominence in the locate extension, the receipt reference shape), the v1 store layout, building and publishing, routes, UI, the per-request article box, feedback and how it becomes G4 benchmark candidates, release coupling, the later D1 import (proposal 11.2) and Brain path (11.3), and the decisions left to Jack, with recommendations. docs/ROADMAP.md gains a "Proposed amendment" at the top of the End goal with Jack's new goal, marked PROPOSED pending ratification (the old text is kept), Waiting on Jack item 16 and a status-log line. CLAUDE.md and AGENTS.md (kept identical) and BRAIN-API.md stop saying /atlas is a retired 404 and point at the atlas.
…to crash on or misread
The builder used to check only necessary conditions of proposal §2.6, so an example
or construction passage matched only to a sorry-backed or proof_wanted declaration
could be published as formalized, and a proved exact match stamped statement_only or
partial passed too. It now recomputes the status per passage from kind, relation and
proof status (derive_status), refuses any mismatch in either direction, accepts both
readings where the table is ambiguous, and refuses passages the table gives no status.
The justifying location is stored as the passage's basis, so pages can name it.
Other refusals that used to pass or crash:
- subject URIs are parsed: oldid must equal the revision exactly (oldid=20029 no
longer passes for 2002), on an en.wikipedia.org permanent link;
- two pages with one title key (only one was reachable by title);
- blob_url_template (it could point "Source" links at any https host) and library
repos with dot segments ("https://github.com/../..");
- unknown statuses, non-string quote affixes and malformed or duplicate-key YAML are
refusals (exit 2) instead of tracebacks (exit 1, the code --check uses for "store
differs"); an internal error now exits 3, and every check runs before any view.
--replace no longer deletes a directory holding anything besides atlas/v1/, and the
previous store is restored if the final move fails. The view model's by_library
splits locations into complete and incomplete, and index rows gain a libraries field,
so the dashboard can say where and how completely an article is formalized.
…ing and the UI
Security and data handling:
- libraries.ts builds every source link from GitHub's blob scheme for the
library's own repository: a universe's blob_url_template is ignored (the
builder already refuses it), owner or repo names "." and ".." get no link,
and a display_name never renames a seeded repository nor names one
("Mathlib", "ATLAS", "FormalFrontier · ..."). The universe page links a
repository only through repoHref (build_store's REPO_RE shape).
- atlas-render.ts puts every store number through int(), so a string where a
count, rank, revision or page id belongs renders as 0, never as markup.
- The feedback export's pseudonyms are domain-separated
(sha256("atlas-feedback\0" + user_id + salt)) so its free-text notes cannot
be joined to the research export's pseudonyms.
- /api/atlas/universe/:sha is no longer "immutable": its key does not cover
the display metadata stored beside the libraries.
Load: parsed index shards are cached per reader for 60 s (registered before
any await, so one request's concurrent loads share the map), with search and
sort keys computed once per entry; a dashboard ?q= search takes the per-IP
anonymous read budget of /api/brain/* and /mcp and answers 429 over it.
What the pages say:
- A located passage states, in visible text, the location that justifies its
status: the store's basis, or the first location meeting the status's row,
never simply rank 1. The pill no longer repeats it as a hover title, and the
producer's "In-text #<hex>" id moved to a data attribute.
- The dashboard splits each library's locations into complete and incomplete
and lists the libraries holding each article (index field "libraries").
- The article box says its counts are separate from the page's annotations
and names the page's revision when the atlas checked another.
- The footer claims only what the page shows; "1 passage", not "1 passages".
Accessibility and layout: Coverage and Passages headings, an h3 per passage
and an h4 over related declarations; aria-current only on /atlas; scrollable
tables are labelled focusable regions with sticky row labels on phones; the
status and library chips filter as two facets combined with AND; inert chips
look flat; status chips carry the bar's fill as a legend; undecided has a
visible hatch and its own stroke; unfinished-proof badges use the amber
statement-only palette; passage permalinks clear the sticky header; short
shas do not wrap and full hashes do. Asset versions bump to v=2.
Tests: atlas.test.ts covers each of these; atlas.spec.ts adds axe and a
no-sideways-scroll check at 375px in both schemes, the combined filters and a
passage permalink. docs/ATLAS.md follows the code.
…ad of crashing derive_status is now a port of formal-companion's cflib.vocab.derive_status (scripts/cflib/vocab.py at b4ac86a), which implements the cases proposal §2.6 leaves to references/vocabulary.md §1.11. The builder's own readings disagreed with it: over every one- and two-location case, 532 statuses the producer stamps were refused and 660 it never stamps were accepted. Each location that counts now gets a status from its kind's row (construction and notation are definition passages; example and other take the better of the two rows), the passage takes the best, and exactly that one status is accepted. The basis is the highest-ranked location reaching it. A theorem matched exactly to data (Real.instField for "R is a field") is partial; a definition matched to a proved theorem is partial; a proved theorem never formalizes a construction or notation. The lean end's optional `statement` flag (a Prop-valued definition) is read from its locate extension: a non-bool value or the flag on a proved declaration is refused, as the producer refuses it, and the view model's locations carry it. fixtures/producer_derive_status.json holds the producer's own answers for all 420 one-location cases and 300 sampled two- and three-location ones (make_producer_table.py regenerates it from a checkout); the parity test requires the port to match every one. A separate exhaustive run over all 1,123,038 one- to three-location cases found no difference. A passage whose only locations are relatedMatch, with no checked absence, has no derived status. Its relatedMatch records may now omit `status`: the builder stores it as outcome unresolved (counted as undecided, never as not formalized) and keeps its related declarations. Such a passage that stamps a status is still refused, as is a status-less record beside one that counts or beside an absence. Malformed values that used to crash the builder (exit 3) are refusals (exit 2): a non-list `excluded`; a list-valued challenge, confidence, prominence, proof_status or rank; `renderer` that is not a short token; a number such as 1e400 that parses as infinity; nesting too deep to parse. A bad value is reported and dropped, so no later check meets it. A new test sets nine hostile values into 58 fields in turn and requires a refusal or a build, never another exception. display_name must be at most 100 printable ASCII letters, digits, spaces and ,.()/+:'&_- or the middle dot, so no zero-width, soft-hyphen or look-alike character reaches the Worker. current.json copies only the sourceset's id and manifest_sha256.
… lists, and the producer's rows libraries.ts: a universe display_name is used only when it is printable ASCII (the builder's pattern) and its skeleton (letters and digits, lowercased, with I, i and 1 read as l, 0 as o, rn as m, vv as w) contains no seeded library's name, checked with and without its "(qualifier)", since chips show the short form. "Mathlib" followed by a zero-width space, Cyrillic "Mathlib", a soft hyphen, "MathIib", "Mathlib4", "Mathlib 4" and the like used to be shown as given; they now fall back to owner/repo. repoHref links only a github.com/<owner>/<repo> repository, so the universe page names any other host as text instead of linking it. atlas-render.ts: a universe's libraries and excluded are read through list(), so a non-array never throws (a missing `excluded` made every article page of the universe a 500) and its "length" never reaches the HTML; the excluded count goes through int(). The page's fallback basis (for a store without one) now uses locationStatus, a port of the builder's per-location rows, checked against the producer's truth table. A definition with the statement flag is badged "Prop definition" and described as stating the claim without proving it. A related-only passage renders as undecided with its related cards. docs/ATLAS.md: check 6 gives the producer's table; contract note 7 records that WikiLean follows formal-companion b4ac86a (not yet on its master); new notes 8 and 9 ask for the statement flag in the lean end and record the status-less relatedMatch shape; display names, renderer, excluded and non-finite numbers are listed under the checks.
…t salt; pin headers and CSP The atlas branch now sits on claude/security-hardening (#84), so the atlas plane follows its rules instead of carrying copies of them. atlas.ts: POST /api/atlas/feedback reads its body through readJsonCapped with its own entry MAX_JSON_BODY_BYTES.atlasFeedback (4 KiB, the cap it had), after the origin, session, bot and rate-limit checks as before. A declared or streamed body past it gets the shared 413 "request body too large (max 4096 bytes)" instead of "payload too large"; a non-object is still "bad json". The private checkOrigin and readCappedText copies are gone in favour of security.ts. The feedback export salts its domain-separated pseudonyms with researchExportSalt (RESEARCH_EXPORT_SALT, else PIPELINE_TOKEN), like the research export, so a bearer holder cannot recompute them once the salt is set and rotating the bearer does not re-key them. Unset, nothing changes. security.ts: the atlasFeedback cap entry, and researchExportSalt moved here from index.ts so both exports share it. Tests: atlas.test.ts checks the cap to the byte (4096 accepted, 4097 refused, refused callers answered 401/403 rather than 413), the export salt, the security headers on every atlas response (pages, APIs, 404, 503, every feedback answer, the streamed export), and that the pages, the article box and atlas.js load only same-origin URLs with no inline handlers under a policy whose 'unsafe-inline' no nonce or hash voids. request-limits.test.ts adds the feedback route to the JSON body cap table and scans wiki/src: no c.req.json() or private body reader, and every readJsonCapped call names a MAX_JSON_BODY_BYTES entry, each in use. security-headers.test.ts checks the _headers rule on /assets/atlas.css and /assets/atlas.js. atlas.spec.ts runs the atlas flows with the Worker's Report-Only policy served as an enforced CSP and asserts no securitypolicyviolation fires. Docs: ATLAS.md (feedback cap, export salt, CSP fit, tests), SECRETS.md (RESEARCH_EXPORT_SALT covers the atlas export; PIPELINE_TOKEN's routes; the request-cap list), and the ROADMAP atlas entry records the stack.
Deicyde
force-pushed
the
claude/formalization-atlas
branch
from
October 18, 2026 02:45
ec8800a to
42d6e65
Compare
Owner
Author
|
Restacked on #84 (security hardening). Merge #84 first; after that, this PR shows only the atlas commits. The combination needed one fix: the feedback POST now reads its body through #84's |
This was referenced Oct 18, 2026
…ect passage
formal-companion and WikiLean agreed one record-set format after smoke 2,
whose export the builder refused on seven mismatches (proposal §2.3 and
references/locate-documents.md §6, made precise; docs/ATLAS.md section 3).
build_store.py now accepts exactly that shape and refuses any other with a
message naming the key or rule:
- SEAL.json has exactly schema, set_id, campaign, universe {id,
universe_sha256}, sourceset {id, manifest_sha256}, skill_commit, created,
byte_budget and files; `runs`, `sourceset.version` and the old
`universe.sha256` are refused by name. campaign is always a token: a
campaign id (not starting "run:") or run:<run-id>[+<challenge-run-id>],
never null. byte_budget is an integer, 0 (none) by default; when it is not
0 a source over it (records plus the receipts its absences reference) is
refused, and current.json records set_id and byte_budget.
- universe.json has exactly id, universe_sha256, frozen, libraries and
excluded. libraries is a list sorted by id, never a dict; each library has
exactly id, brain_lib, repo, commit, toolchain, roots and licence {spdx},
with display_name optional (absent or null). index, conventions, src_dir
and blob_url_template are refused; excluded is a list of {id, reason}.
universe.yaml is no longer accepted (and PyYAML no longer needed).
- Every record carries its passage's section (heading path, [] in the lead)
and prominence. A lean end's end_line is optional (atlas's published index
has only line) but never null; the view model omits it when absent. A
closeMatch still needs a non-empty note. An absence's lean ends are
minimal {type, uri, version}.
- Hex, token and time patterns now match in full (\Z, ASCII digits), so a
trailing newline no longer passes as a sha.
Worker: a lean end's path is relative to the repository root (Lean core's
real paths are src/Init/...), so the registry no longer prefixes a seeded
src/ to lean4 links (it would have linked src/src/...). A location without
end_line reads "line N" and links #L<line>. CAMPAIGN_RE takes the same
grammar as the builder, so feedback on a run outside any campaign is
accepted, and the pages name such a run ("run L with challenge run C,
outside any campaign"). The coverage page marks subject passages: a
"Subject of the article" tag, an accent frame (is-subject,
data-prominence), and a Subject row in the strip linking each one.
atlas.css ?v=3.
Fixture regenerated in the agreed format (synthetic): libraries sorted by
id, the Widget theorem and the Gadget lead definition as subject passages,
FormalFrontier's closeMatch with line only and a challenge-downgrade note.
The universe sha is unchanged. The derived-status parity table is unchanged
(decision D1 pending).
Tests: test_build_store.py gains AgreedFormatTests (seal keys, campaign ids
and run tokens, the budget, the universe's list and keys, section and
prominence, end_line, closeMatch notes, minimal absences) and hostile values
in the seal; atlas.test.ts covers the subject marking, a location without
end_line, ordering by id, repository-relative paths and a run-token store
with its feedback; atlas.spec.ts follows the Subject link.
…agreed format left unwritten
The builder refused challenge_pending, a challenge verdict the producer's
proposal (section 2.7) and cflib.vocab define: smoke-2b's real set was
refused over its 4 such records, and now builds (31 files). The pages read
it as unchallenged ("not challenged yet (a challenge is pending)"), and the
fixture's Gadget location carries it.
Where the agreement named a value but not its grammar, docs/ATLAS.md
section 3 now states the builder's rule, and each refusal names it: the
token grammar of set_id, universe.id and sourceset.id; the repo grammar
(no trailing slash, one to four segments); a licence that is never null;
module, path and line required on a location's lean end (only end_line is
optional); receipt counts as the lengths of the receipt's lists, repeats
included, with both numbers in the message; and length caps of 300
characters for brain_lib, toolchain and roots and 1000 for an exclusion's
reason (was 300, with a message that named the wrong rule; u1's longest
reason is 215).
Deicyde
added a commit
that referenced
this pull request
Oct 18, 2026
PR #85 changed site/assets/atlas.css (the record-set format alignment), so its attested sha moves; atlas.js and every other entry are unchanged.
…ata that states a theorem
D1 (2026-10-18): "Formalized when the hasPart locations together cover every
clause (challenger confirms coverage), and when an exact/closeMatch is to an
equivalence or data declaration that states the theorem (e.g. CRT's RingEquiv)."
Builder (scripts/atlas/build_store.py):
- A theorem or conjecture passage with an exactMatch or closeMatch to data (a
definition without the statement flag) is formalized. A broadMatch to data
stays partial, and a Prop-valued definition stays statement_only.
- The builder reads a passage's coverage claim from extensions[locate].coverage:
{complete: true, parts: [location_key, ...], challenge}. Every record of the
passage carries the same claim, or none does. A null claim, a missing or
extra key, complete false, fewer than two distinct parts, a challenge outside
the vocabulary, or a part that is not a hasPart location of the same passage
is refused, with a message naming the rule.
- Only a survived claim counts. On a theorem passage, or the theorem row of an
example or other passage, it gives formalized when every part is proved, and
statement_only when every part is proved or unproved. On a definition,
construction or notation passage, it gives formalized when every part is a
definition or proved. Where the decision says nothing more, these follow its
literal wording, as the skill does (Q1-Q3, docs/ATLAS.md contract note 11).
- The best status over all the evidence wins. On a tie, the location is the
basis; when only the claim reaches the status, the claim is the basis.
View model and page: each passage carries coverage {complete, parts, challenge,
status, basis}. A survived claim shows "Formalized by N parts together" with
its parts listed, or the statement-only or no-upgrade wording. A claim that did
not survive shows nothing. theoremRow follows D1. atlas.css goes to v=4.
Fixtures: two synthetic Gadget theorems. One is a conjunction that two proved
hasPart parts cover under a survived claim; the other is stated exactly by an
equivalence. producer_derive_status.json is regenerated from formal-companion
b33f17f (locate/d1), the producer commit that implements D1. Exactly 13
answers changed, each a theorem with an exact or close match to data. The
table adds 959 coverage cases from the producer's own derive_status, and
make_producer_table.py now refuses a producer with uncommitted changes to its
scripts/cflib. The Worker and browser tests cover the line, its wording,
malformed claims, and axe on the Gadget page in both schemes at both widths.
Parity round one ran formal-companion's hand-written status table and an adversarial set through both sides. They agreed on every status an export can carry and differed on three inputs no export produces: an owed claim (challenge null), a claim with a note, and one location_key on two locations. WikiLean refused all three, as the agreed record format says; the producer's derive_status now refuses them too (formal-companion c165c65), so the builder's semantics are unchanged. - build_store.derive_passage_status takes the producer's arguments (passage_kind, locations, absent, coverage) and puts one passage through the builder's own checks (statement flag, distinct 64-hex keys, absence beside relatedMatch only, coverage_claim, coverage_part_problems), then derive_status; StatusRefused where build() would refuse the set. - fixtures/status_parity.json: the skill's tests/data/locate/status-parity.json at c165c65, byte for byte (97 cases, 22 refusals), its sha256 pinned. The Python test runs every case and checks the function against build() on every fixture passage; the Worker test runs its claim-free cases through the page's locationStatus fallback. - A null coverage challenge in a record is refused with its own message. - producer_derive_status.json regenerated at c165c65: all 1679 answers unchanged. - docs/ATLAS.md (claim format, checks 5 and 6, contract notes 7 and 11, tests) and the ROADMAP status log.
…m a claim's parts Parity round three: the lead set the reading of decision D1 that resolves the open questions Q1-Q3, and formal-companion implements it at 3225e95 (branch locate/d1). A survived coverage claim now counts, for derive_status, as one more exactMatch location whose declaration is the weakest of its parts. A part is finished when it is proved or data (a definition without the statement flag), and unfinished when it is statement_only, wanted, axiom_dependent or a Prop-valued definition. Every part finished gives formalized on either row; any part unfinished gives statement_only on both rows; an example or other passage takes the better row, as for any location. A claim that has not survived still adds nothing. - build_store: part_finished and coverage_location replace the two literal per-row rules, and coverage_status runs the claim through the same _theorem_row and _definition_row as an ordinary location. - Confirming a claim confirms its parts: the view model (confirmed_parts) shows a survived claim's not_required and sampled_out parts as survived. A part another verdict judged keeps that verdict, and so does one still pending. Records are copied verbatim, so a set exported before round three reads the same as one the producer now exports with its parts survived. - fixtures/status_parity.json: the skill's tests/data/locate/status-parity.json at 3225e95, byte for byte (117 cases, 22 refusals, P01-P04 with expected_challenges), with sha256 0ee06d56... pinned. The Python test checks confirmed_parts against expected_challenges. - producer_derive_status.json regenerated at 3225e95. 394 of the 1679 answers changed, all of them coverage cases under a survived claim. - Page: a statement-only claim reads "Stated by N parts together, not all of them finished". The "Covered by" line stays only for a store built before this round. The Worker test checks that both part cards say a challenger checked them. - docs/ATLAS.md (claim format, check 6, contract notes 7 and 11 with a round three paragraph, store and page notes, tests) and the ROADMAP status log. The skill's round-three smoke export (recordset-d1c, 331 passages, no claims) builds with its statuses: formalized 131, statement_only 2, partial 94, not_formalized 104.
…s stand-in is fixed (review 4) Review four of formal-companion 3225e95 and WikiLean 698cfd7 found the producer confirming a survived claim's parts before a prominence overturn's reopen, so a sampled_out part of a passage overturned to subject or central in the same run was exported survived, where WikiLean's confirmed_parts keeps challenge_pending. The lead decided the reopen wins, and the producer now confirms parts after the reopen (4fc2aa0). WikiLean's rules did not change. - status_parity.json: the skill's table at 4fc2aa0, byte for byte (118 cases; P05 is the reopen), and SHARED_TABLE_SHA256 re-pinned. The table test also checks that P05's challenge_pending parts stay pending under the survived claim. - producer_derive_status.json regenerated at 4fc2aa0: every answer unchanged, only the commit stamp moved. - The docs and comments said a survived claim acts as an exactMatch location "whose declaration is the weakest of its parts". Read literally that is wrong on the definition row; the code always used a fixed stand-in (proved on the theorem row and a definition on the definition row when every part is finished, statement_only on both otherwise), and docs/ATLAS.md, docs/ROADMAP.md, build_store.py and test_build_store.py now say so. - docs/ATLAS.md's "a set exported before round three reads the same" is now true for the parts' challenge values (checked by running the reopen repro through c165c65 and 4fc2aa0) and says so, names the 3225e95 exception, and says that stamped statuses are re-derived, so an older set builds only where no rule it turns on changed. The three smoke-2 sets (d1, d1c, d1e) build with the current builder to the same status and challenges.
Deicyde
added a commit
that referenced
this pull request
Oct 18, 2026
PR #85 changed site/assets/atlas.css again (the coverage-parts list of decision D1), so its attested sha moves to 044fbca9; atlas.js and every other entry are unchanged.
This was referenced Oct 19, 2026
Deicyde
added a commit
that referenced
this pull request
Oct 19, 2026
Attestation: drop the atlas assets until #85 merges
PR #104 dropped assets/atlas.css and assets/atlas.js from main's attestation until this PR merges, so release B could be built at 2cf36c7 without the atlas. This PR ships both files, so it restores both entries (atlas.css 044fbca9, atlas.js 29d8a77b): the files and their attestation land in one merge, and a release built from any later main freezes cleanly. Every other entry is main's, unchanged.
…atlas # Conflicts: # wiki/src/index.ts
…pt F5's span
docs/ATLAS.md said the builder "accepts this shape and refuses any other, naming
the key", but classify_record read only the keys it used from the locate
extension at its three places (the record, the subject end, a location's lean
end). A new, misspelt or malformed key there built without complaint and was
published in the store's records: `spann` for `span`, a stray `x_note`, a
second extension namespace.
- build_store: each place now has its agreed key set (the record's by shape:
location, absence, unresolved; the subject end; the lean end; the absence's
receipt), and any other key is refused naming the key, its place and the
record id. The record and both ends carry only the locate extension
namespace. A missing required key is still named by its value's check.
- The subject end's renderer (the source's token), licence (a non-empty SPDX
id) and span_sha256 (64 hex) are now checked; pageid and the receipt counts
must be integers (1001.0 and 2.0 compared equal before).
- formal-companion 722b30f ("F5") adds the passage's span and the layer_sha256
it indexes to every subject end. Both are accepted as optional, together or
not at all: span is [start, end], integers with 0 <= start < end, no shorter
than the quote's exact; layer_sha256 is 64 lowercase hex and the source's.
Where the quote and its suffix give the span's text in full, span_sha256
must be its sha256. Records of one passage agree on span and span_sha256.
The view model copies neither, so the golden store is unchanged.
- docs/ATLAS.md: the subject end's keys and F5 in section 3, a table of the
locate extension's keys, checks 5 and 6, contract note 12, the store note in
section 4, and the test list.
- test_build_store: an unknown key at each place (and a key of another shape,
a stray receipt key, another namespace) refused by name; the subject end's
new checks; integer receipt counts; a valid span building to the same view;
a malformed span or layer sha, either alone, a span shorter than its quote,
a contradicted span_sha256 and disagreeing records refused; hostile values
in the new fields.
The real sets smoke-2-d1e, smoke-2-p3 and an F5-shaped copy of smoke-2-p3
build byte for byte the stores the previous builder built (31 files each), and
the copy's misspelt, stray-key, bad-span and wrong-layer variants are refused.
Deicyde
added a commit
that referenced
this pull request
Oct 19, 2026
…ys and F5's span, with quote_capped #85's key checks at record level, subject end and lean end stay as they are; #103's quote_capped, passage_ends_in_suffix and by_prominence are store fields and pass them. quote_extent now takes F5's span as a shortcut (tail = (end - start) - len(exact)) and falls back to the span_sha256 search only for a tail one or two characters past the suffix. span_sha256 is now required, so #103's "a set without it builds" test is gone; #85's span test compares a set with spans against the same set without them, and new tests check the shortcut against the hash path case by case and on the fixture.
Proposal section 2.3 lets a universe split one repository into libraries at one
commit, one root each (lean-core as init and std, so the Brain gets one token
per root). The builder refused that universe ("repo appears twice (one library
per repository)"). The two sides agreed on 2026-10-19 to key libraries by id
and refuse only a true duplicate; formal-companion's side is locate/brain4
124a587 (records.absence_ends: one absence end per distinct (repo, commit)).
- build_store: the rule is each library id once, and each (repo, root) pair
in one library only (LIBRARY_RULE). Two libraries may share a repository, at
one commit or two, but not a root of it, and a library may not list a root
twice; a repeated id is now named as such. Nothing else about a shared
repository is refused.
- The absence check already compared the ends with the universe's distinct
(repo, commit) set, each pair once, which is what 124a587 writes; its
messages now say so. make_fixture writes the ends the same way (the
fixture's repositories are distinct, so its bytes do not change).
- The view model was already keyed by library id (locations, both by_library
maps, the index rows, the universe file). The pages now name libraries per
id too: libraries.ts libraryInfos tells apart libraries that would read
alike (one chip label, as libraries of one repository always do) by their
roots, "Lean core · Init" and "Lean core · Std", or by their ids when the
roots are not plain module names or do not tell them apart. The article
page, the dashboard (and the names atlas.js reads) and the universe page use
it. atlas.css and atlas.js are unchanged.
- docs/ATLAS.md: the rule in section 3, checks 2 and 5, contract note 13, the
view model in section 4, the Libraries UI note, the Brain path and the test
lists.
- Tests: init and std at one lean4 commit beside mathlib build, each kept
apart by id; an absence naming lean4 once builds, twice is refused, and one
repository at two commits needs two ends; a duplicate library id, a shared
root of one repository and a repeated root are refused. The Worker tests
name split libraries apart on every page.
Checked on brain4's locate e2e run over a split universe (alpha, and init and
std at one example.org/lean4 commit, a location in std): the previous builder
refuses its sealed set and this one builds it. The unsplit e2e set and the
smoke-2 sets d1, d1c and d1e build byte for byte the stores the previous
builder built.
Deicyde
added a commit
that referenced
this pull request
Oct 19, 2026
…ository, keyed by id Two conflicts. make_fixture's absence keeps #103's subject(source_id, quote, layout) and takes #85's ends, one per distinct (repo, commit), which for the fixture's distinct repositories are the same bytes. docs/ATLAS.md section 4 keeps #85's sentence that every library in the view model is a library id, followed by #103's quote_capped and passage_ends_in_suffix notes. The rest merged cleanly: #103's dashboard (held libraries by passages, the others listed below the table) reads the names libraryViews now gives, so libraries split from one repository are "Lean core · Init" and "Lean core · Std" there too. test_build_store passes (110 tests), as do wiki/test/atlas.test.ts and the typecheck. The smoke-2 sets d1, d1c and d1e and brain4's unsplit e2e set build byte for byte the stores the pre-merge builder built; brain4's split-universe e2e set, which it refused, builds.
Owner
Author
|
Verdict: request changes. There is one line to fix; after that, merge once release B is promoted and the demo hold lifts. Four static reviews covered security, correctness, the claims against CI, and fit with main and release B. Two or three refuters then checked each substantive finding. Blocks merge
What holds up
Notes (none blocks merge)
Posted by Claude Code (AutoformBot "Merge Currently Open PRs 4" session). |
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.
This adds the consumer side of the formal-companion skill's locate pipeline. That pipeline finds which passages of each WikiProject Mathematics article are formalized in Lean, in which library and at which commit, and how closely, across Mathlib, Lean core/Batteries, TauCeti, the FormalFrontier libraries, atlas-lean and formal-conjectures.
The atlas is a separate, read-only data plane. It writes no D1 annotations, so it is not subject to the 256 KB payload cap or the write limiter, and the nightly moderation cannot overwrite it. The design is in
docs/ATLAS.md.What is in it
scripts/atlas/build_store.py: turns a sealed Literature Links record set into a static store. Each record is validated against the vendored schema, SEAL shas are checked, and derived status is recomputed from the documented table, not trusted. The output is deterministic and has a--checkmode.wiki/src/atlas.tsandatlas-render.ts: a store reader over an optional R2 bindingATLAS. Every route returns 503 while it is unbound. The routes are:/atlas, with totals by status, library and importance;/atlas/:pageid, with per-passage cards (library chip, commit, relation, proof status, source link at the commit);site/assets/atlas.{css,js}: the coverage UI. It is accessible, does not rely on colour alone, and uses only textContent writes.0015_atlas_feedback.sql: confirm/report feedback per location, fail-soft (503 until it is applied). The routes are session-only, origin-checked, capped and rate-limited.wiki/src/libraries.ts: the library registry, with blob URLs limited to https GitHub.docs/ROADMAP.md: the End-goal amendment, marked PROPOSED for the maintainer to ratify.Gates (local):
npm run test:ci(47 files, 1,064 tests),scripts/ci-python.sh(101 commands, with npm on PATH) and Playwright (17/17) all pass.Before deploy: create the R2 bucket and binding, apply 0015, and add
assets/atlas.cssandassets/atlas.jsto the public-asset attestation (PR #82). This should merge after #84 and before #82.