K12. Pipeline and operations

This document says how the corpus is produced: the stages that an item goes through, the jobs and the queues, the limits on speed, the cost, the commands and the libraries. It uses the orchestrator of spec 11.4 and 11.5 and the roles of spec 12.1 and K7.3. It adds no new write path. Each change is a pull request, and the audit is the gate (settled decision 7).

K12.1 The stages of an item

An item goes from "a source mentions it" to "a complete node" in stages. Each stage has a goal predicate that the build can compute, so a job knows when it is done.

The formal track runs next to stages 5 to 7. It does not wait for them:

An item that a formal library has (K06) starts on the formal track at "bound" and reaches stage 5 through the informalize role. An item from a textbook starts at stage 5 and reaches the formal track through formalize. Both paths end at the same node.

K12.2 Jobs

The corpus adds standing queues to the four sources of jobs in spec 11.4. Each queue is computed from the graph and the inventory on each build:

A job of the corpus has the record of spec 11.4. Its goal names a stage, for example goal: "node reaches W2" or goal: "row 9DK2RX7Q4H has an outcome".

K12.3 Priority

The priority formula of spec 11.4 applies. The corpus adds two terms, and the formula keeps its version like a prompt:

priority = w1 · centrality(target)
         + w2 · demand(target)
         + w3 · unlock(target)
         + w4 · tractability(target, role)
         − w5 · attempts(target, role)
         + w6 · spread(target)        # the number of independent sources that hold the item
         + w7 · curriculum(target)    # the item is in a curriculum or a standard volume (K10, K11)

spread puts first the items that many sources hold. An item that eight textbooks and two libraries hold is almost surely standard and is cheap to state well. An item that one source holds needs more care, and it can wait. curriculum puts first the items that a course or a book needs, so that the first volumes can be packed early (K14).

The order of work in spec 18.5 still applies: breadth first on the record plane, depth first on the statement plane. In the corpus, this means that the inventory of each area is built first, and then each area is written in depth, in the order of the curricula.

K12.4 Batches

Most corpus work has no person waiting for it. So it runs in batches:

• Model batches. The write, explain, exercise, informalize and enumerate roles, and the dedup judge, use Message Batches at half price (spec 12.3). A batch holds jobs of one role and one topic, so that the cached part of the context (the system prompt, the card, the style guide, the notation register of the topic) is the same for each job.
• Pull request batches. One pull request for each node would give millions of pull requests. A batch pull request holds up to 50 nodes of one topic, from one role and one configuration. The audit checks each node in it. A reviewer can merge a part of it: the nodes that pass, with the others sent back to the queue with their reasons.
• Small diffs. A batch pull request changes only the files of its nodes and their provenance logs. It never changes a register by hand. The build writes the registers.

K12.5 Review capacity is the limit

Settled decision 20 caps agent pull requests at a multiple of the measured review throughput. In the corpus, this is the main limit on speed, not money and not model speed. So the plan starts from the review hours.

Each month, the review hours go first to the work that keeps the measurements honest, and then to the work that moves items:

The agents then get pull request capacity in proportion to the review hours that remain, by spec 11.5. A role that makes work that nobody can review in time does not run.

An example with round numbers. 100 active reviewers give 10 hours each month: 1,000 hours. The sample audit and the reports take 250 hours. Of the 750 hours that remain, 400 go to F2 reviews (8,000 statements) and 350 go to confirmation (about 14,000 sections). At this rate, F2 for the 500,000 statements of the textbook layer takes about five years, and W3 for 1.5 million nodes takes longer. This is why W2 is the target of the textbook layer and W3 is the target of the standard volumes only (K2.7, K11). It is also why the corpus must recruit reviewers (K14) and make each review fast (spec 16.3).

K12.6 The cost of the models

The model cost is small next to the cost of people, but it is not zero, and the plan must say what it is. The numbers below are estimates for planning, with the prices of spec 12.3 and batch pricing. They assume that the cached part of each context is read from the cache. The run records replace them with measured numbers after the first thousand jobs of each role. K7.8 gives the cost of each configuration of models for one node.

For the textbook layer of 1.5 million nodes at W2, the writing cost is about $0.10 for each node, or about $150,000. Retries and escalation can double it. Formalization of 500,000 statements costs $250,000 to $2.5 million, and it is the largest model cost. The copy check (K9.4) and the sanity checks by computation run on math2's own machines.

No model run starts without a budget that a person approved. The global monthly budget of spec 11.5 is the only source of money. m2 corpus plan (K12.8) estimates the cost of a queue before anyone approves it.

K12.7 Measurement

The corpus has its own section in the weekly agent report (spec 12.9) and in each release manifest:

• the open count, for each layer and each MSC code, and its change since the last report;
• the number of nodes at each writing level, for each layer;
• the formal outcomes of K2.5;
• the error rates of K9.7, with their intervals;
• the review hours used, by use (K12.5), and the queue lengths;
• the model spend, by role and stage, and the cost of each item that reached a new stage;
• the rate of fabricated sources (K9.5) and of copy matches (K9.4), by configuration.

A number that goes the wrong way is in the report with the others. The release notes account for each change in the counts (rule R03).

K12.8 Commands and libraries

The corpus adds two command groups to m2. Each command is a thin layer over a library package. The packages follow the conventions of the toolchain: one package for each concept, no internal/ directory, exported types with documentation and a testable example, and tests that use fakes for each model and each network service.

K12.9 Scale of the repository

The textbook and formal layers add 1 to 2 million node files, with their provenance logs. That is in the range of spec 06.1 and 06.7. The research layer is in the record plane, and its inventory rows are in the record plane too (K4.8). When the repository passes the trigger of spec 06.1 (10 GB packed or 5 million files), the record plane and the inventory of the research layer move to tamnd/math2-records together.

Agent branches are short. A batch branch lives until its pull request merges or closes, and the orchestrator deletes it then. Contributors who work on one area use a sparse checkout of the shards that they need. m2 works on a sparse checkout, except for the commands that need the full graph (m2 build, m2 audit), which run in CI.

Markdown · Source · Edit