Repository navigation
Conversation
Phase 3 of the split. `build_store.py --statement-set <dir> --tagging-universe
<file>` builds a sealed wikilean.statement-set/1 into the same store a record
set builds into, on its own or beside one.
An unchecked passage is not an unresolved one. `unresolved` means a locate run
ran and settled nothing; `not_formalized` means every library was searched and
it is not there. A published cut means nothing has been searched at all, so:
passage outcome "unchecked", status null, locations [], and the cut's own
`statement`, `conjuncts` and `shape`, which a located passage has
nowhere to put
article checked: false (and true on a record-set article of the same build),
records_sha256 null and NO records file, licence CC-BY-SA-4.0 from
the source family, the tagging universe, and a `seal` with the cut
rules and producer_commit — never written as skill_commit, because
the cut is WikiLean's pipeline's and not formal-companion's
store a sixth summary status, not_checked, in every by_status map, and
appended to the index fields after `libraries`, where the Worker
looks a field up by name
not_checked is never folded into not_formalized, and never into unresolved.
Only `formal_math` statements are published: a locate run searches those and no
others, so "0 of 89 checked" is the same 89 phase 2 will answer for.
The mixed-build rule is #177's with one clause: every set of a build resolves to
one universe.json, byte for byte. A cut names no libraries, so --tagging-universe
supplies them, and in a mixed build it must be the record sets' own file. Page
ids and title keys stay disjoint across every set; the schema, sourceset,
skill_commit and status-rule agreement stays a record-set rule, because a cut
has none of those to agree on. The tagging universe's (library id, repo) pairs
must be the ones phase 2 will search — POST /api/articles/tag derives pair_key
from the repo — which the operator holds and the builder does not pretend to.
**A build with no statement set is byte for byte the build it always was.** R0
and the golden store are unchanged, INDEX_FIELDS is unchanged, and no article
carries `checked`. The new fields appear only in a build that holds a cut; an
older Worker degrades an unknown status to "no status yet" and ignores a sixth
by_status key, so an early upload is survivable — ship the Worker first anyway.
build_store keeps its own copy of the contract, as it does for the record set,
and scripts/pipeline/test_vocab.py pins the two vocabularies together. Two
things the consumer's copy owes the producer's: a statement holding text UTF-8
cannot carry (a lone surrogate, which reaches a set only as a \udXXX escape) is
refused by name rather than raised by the canonical JSON of the view it would
have reached, and a line ends at "\n" alone, as statements._jsonl reads it,
because JSON holds a U+2028 unescaped inside a string and str.splitlines would
call a sealed, untampered file broken.
The five side files describe what they are about and no more, so one store can
hold both kinds of article. A statement set seals every statement's span on the
pinned layer, which is all --reader-html and --passage-text join on, so a cut's
article has its marked revision and its passages' full text like any other --
and without that the design's own reader, a neutral highlight on the article's
text, could never be published at all. Each mark of a cut carries the passage's
own outcome, data-status="unchecked" (passage_status_word), and a statement the
store does not publish may not be marked. --signatures describes the
declarations a card links, and a cut has no card; --provenance describes the
locate runs that made the records, and a cut has none, so a statement set is
skipped there and its article carries no `provenance` -- its own is the `seal`
it already carries. --audit-summary still lists every sealed set of the build.
docs/ARTICLES.md section 4a is the exact field list, for the reader to build
against. scripts/articles/fixtures/store-mixed/ is the golden store of the
record set beside the pipeline's synthetic cut, with that cut's first article's
marked revision (fixtures/make_reader_fixture.py writes the side file), and the
Worker's own tests serve those same bytes, so the two halves of phase 1 cannot
drift.
Release-neutral: scripts/ and docs/ only.
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
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.
Phase 3 of the split.
build_store.py --statement-set <dir> --tagging-universe <file>builds a sealed
wikilean.statement-set/1into the same store a record set builds into,on its own or beside one.
An unchecked passage is not an unresolved one.
unresolvedmeans a locate run ranand settled nothing;
not_formalizedmeans every library was searched and it is notthere. A published cut means nothing has been searched at all, so:
outcome: "unchecked",status: null,locations: [], and the cut'sown
statement,conjunctsandshape, which a located passage has nowhere to put;checked: false(andtrueon a record-set article of the same build),records_sha256: nulland no records file,licence.textCC-BY-SA-4.0from thesource family, the tagging universe, and a
sealwith the cut rules andproducer_commit— never written asskill_commit, because the cut is WikiLean'spipeline's and not formal-companion's;
not_checked, in everyby_statusmap, andappended to the index fields after
libraries, where the Worker looks a field up byname.
not_checkedis never folded intonot_formalized, and never intounresolved.Only
formal_mathstatements are published: a locate run searches those and no others,so "0 of 89 checked" is the same 89 phase 2 will answer for.
The mixed-build rule is #177's with one clause: every set of a build resolves to one
universe.json, byte for byte. A cut names no libraries, so--tagging-universesupplies them, and in a mixed build it must be the record sets' own file. Page ids and
title keys stay disjoint across every set; the schema, sourceset,
skill_commitandstatus-rule agreement stays a record-set rule, because a cut has none of those to agree
on. The tagging universe's
(library id, repo)pairs must be the ones phase 2 willsearch —
POST /api/articles/tagderivespair_keyfrom the repo — which the operatorholds and the builder does not pretend to.
A build with no statement set is byte for byte the build it always was. R0 and the
golden store are unchanged,
INDEX_FIELDSis unchanged, and no article carrieschecked. The new fields appear only in a build that holds a cut; an older Workerdegrades an unknown status to "no status yet" and ignores a sixth
by_statuskey, so anearly upload is survivable — ship the Worker first anyway.
build_storekeeps its own copy of the contract, as it does for the record set, andscripts/pipeline/test_vocab.pypins the two vocabularies together. Two things theconsumer's copy owes the producer's: a statement holding text UTF-8 cannot carry (a lone
surrogate, which reaches a set only as a
\udXXXescape) is refused by name, ratherthan raised as a
UnicodeEncodeErrorby the canonical JSON of the view it would havereached; and a line ends at
"\n"alone, asstatements._jsonlreads it, because JSONholds a U+2028 unescaped inside a string and
str.splitlineswould call a sealed,untampered file broken.
The side files describe what they are about and no more, so one store can hold both
kinds of article — which it must, because one store is what the operator uploads. A
statement set seals every statement's span on the pinned layer, and that span is all
--reader-htmland--passage-textjoin on, so a cut's article has its marked revisionand its passages' full text like any other article's. Each mark of a cut carries the
passage's own outcome,
data-status="unchecked"— the design's neutral highlight, whichwithout this could never be published at all — and a statement the store does not
publish may not be marked.
--signaturesdescribes the declarations a card links, and acut has no card.
--provenancedescribes the locate runs that made the records, and acut has none: a statement set is skipped there and its article carries no
provenance,its own being the
sealit already carries.--audit-summarystill lists the sealsha256 of every sealed set of the build.
docs/ARTICLES.mdsection 4a is the exact field list, for the reader to build against,and §5 says what each side file does beside a cut.
scripts/articles/fixtures/store-mixed/is the golden store of the record set besidethe pipeline's synthetic cut, with that cut's first article's marked revision
(
fixtures/make_reader_fixture.pywrites the side file, and a test holds the committedcopy to what that maker writes). The Worker's own tests serve those same bytes
(
wiki/test/articles-store-mixed.test.ts, on the reader's branch), so the two halves ofphase 1 cannot drift: the builder's test owns the bytes and the Worker's test says what
it does with them.
Release-neutral:
scripts/anddocs/only.