leanchecker checks every module under a name prefix, in parallel

[carlok]

leanchecker <Module> checks every module whose name starts with <Module>, all in parallel. LeanChecker.lean (toolchain v4.34.1) matches with target.isPrefixOf m and runs one IO.asTask per matching module.

LeanFrontier.NumberTheory.MarkovTree is both a file and a folder of 20 modules, so checking it checks 21 modules at once. That's what killed the v4.34.1 upgrade audit in its 6 GB container (#423 raised it to 12 GB).

Measured locally on v4.34.1 (/usr/bin/time -l lake env leanchecker <m>):

module	modules under the prefix	time	peak memory
NumberTheory.MarkovTree.Paths	0	9 s	1.2 GB
NumberTheory.SternBrocot.Intervals	0	7 s	1.2 GB
NumberTheory.SternBrocot	3	9 s	6.0 GB
NumberTheory.MarkovTree	20	73 s	13.5 GB

MarkovTree itself is trivial for the kernel: compiled with -Dprofiler=true, its type checking takes 18 ms. It passed the receiver in 2 GB on 21 Sep because the folder was empty then.

Consequences

• The upgrade audit (tools/audit_mathlib_upgrade.py) calls leanchecker once per corpus module, so every module under a prefix is checked again with its parent. It's correct but redundant, and the memory spike grows by about 0.6 GB per child. 12 GB leaves room for roughly 20 more MarkovTree/* modules.
• The receiver (kernel_recheck in tools/frontier_validate.py) only checks newly submitted modules. It's affected only if a submission adds a file whose folder already has modules. Since fix: the receiver names a silent kernel-recheck kill, with room to avoid one #426, that case is reported as a memory kill rather than a silent rejection.

Options

1. Leave it; revisit when the largest family nears ~35 modules. (current choice)
2. Check each module exactly once: the audit calls leanchecker only for modules that no other corpus module is a prefix of. That removes the redundancy; peak memory stays equal to the largest family.
3. A Tools/ executable replaying exactly one module (leanchecker's replayFromImports, about 20 lines). Best memory, but it adds trusted code and we could no longer say the corpus was checked by the standard leanchecker.

Recommendation: option 2 when a family approaches the limit.

[carlok]

Decision (29 Sep): option 1, leave the audit as it is, with a tripwire.

#434 adds a test that fails when any module family passes 30 submodules. It fails on the pull request that would push a family past the limit, naming the family and pointing here, before an upgrade audit runs out of memory. When it fires: apply option 2 (check each module exactly once), or raise the audit's memory, then raise the test's limit.

Correction to the description above: NumberTheory.MarkovTree has 19 submodules, not 20, so leanchecker NumberTheory.MarkovTree checks 20 modules, not 21. The measurements are unchanged: 13.5 GB and 73 s on macOS. Largest family today: MarkovTree, 19. Next: SternBrocot and MarkovEquation, 3 each.

[carlok]

Closing as decided. Nothing is pending, and the watch is automated.

• Decision (29 Sep): option 1. The audit stays as it is.
• Guard: test_no_module_family_outgrows_the_kernel_recheck (test: a tripwire before a module family outgrows the kernel recheck (#429) #434, tests/test_mathlib_upgrade.py) fails when any module family passes 30 submodules. Its docstring points here.
• Family sizes on 4 Oct: MarkovTree 19 (unchanged), SternBrocot 6 (was 3; RunLength, RunEncoding and QuotientSequence landed this week), MarkovEquation 3.

Reopen when the tripwire fails. Then apply option 2 (check each module exactly once) or give the audit more memory, and raise the test's limit.