Each theory is its own derivation, whose inputs are its one .v file and the objects of the theories it imports, so an edit recompiles that file and its importers and nothing else; every other object comes from the store or a cache. Imports are read here from the sources' From Nanofil Require sentences; deps below checks them against rocq dep.

link N: the objects of everything N imports, under theories/.

The grammar check (web/rocq/tests/parse.sh), one theory at a time: reprint it with every subterm in parentheses and compile the reprint against the original objects of its imports. It needs neither its own object nor the other reprints, so a grammar change reruns every file at once and a theory edit reruns that file.

parse.sh's own Ltac, term and Iris fixtures.

The compiled theories as one tree, for the logic spikes (spikes.nix), which compile against them. Nothing in CI's gate needs it.

The model: every theory compiled, no Admitted or stray Axiom, imports as rocq dep reads them, and the extracted driver, with the sources the checks read (programs.sh compares the Code.v files). Its output is a few MB; the objects stay in their own derivations.

The check reads compiler sources, harnesses and corpora, not the wiki, benchmarks or theories (the latter enter through model above).

The corpus reads the extracted driver (Extract.v's imports, a few of the theories) and the sources, so it runs beside the proof compiles; the check below still requires the whole model.