Pass the audit's module list and the remaining probe lists as JSON

[Deicyde]

Closes #241. #209 and #280 stopped compiling the probes' long name lists into Lean list literals: past about 1,500 entries, Lean's code generator stops with "maximum recursion depth reached in the code generator". Three lists were still literals:

• The kernel-trust audit's module list, in both the strict and the open probe of autoform_cli/templates/github/autoform_audit.py. Pass the remaining Lean probe lists as JSON, as #209 did for requested roots #241 missed this one. It holds every module of the root package, so the audit a project's own CI runs could not run at all on a root package of more than about 1,500 modules. On main's template, a scratch CI run compiles both probes with 1,000 and 1,500 modules and stops with the code generator's error at 2,000 and 3,000. With this branch's template, all four sizes compile and run to their first check: https://github.com/facebookresearch/autoform-bot/actions/runs/38497826590
• The skeleton probe's library roots (project_roots), which Pass the impact and unused-hypotheses probe name lists as JSON #280 left for after the Extract Lean skeletons one probe per root module #213 stack.
• The impact probe's glob walks (glob_directories), which Refuse root modules the inventory skips in work impact too #277 added after Pass the remaining Lean probe lists as JSON, as #209 did for requested roots #241 was filed.

Each now reaches Lean as one JSON string that the probe decodes when it runs, as the requested roots do:

• Library roots: Pass the skeleton probe its roots as JSON #209's [request, components] format, read with the skeleton probe's requestedRoots.
• Glob walks: [directory, components, glob] triples. Their names go through the impact probe's existing component rule, now shared as nameOf.
• Audit modules: lists of string components, read with the audit's existing autoformAuditNameOf and autoformOpenAuditNameOf.

The Cabannes example's copy of the template is updated to match, since test_example_and_template_helpers_are_identical requires an identical copy.

The skeleton probe's core_roots stays a literal: it is the four fixed names Init, Lean, Std and Lake.

Line breaks inside records (second commit)

#241 also asked for a test that a quoted name component holding a newline, a backspace, DEL or NEL survives the round trip. The input side does. The output side did not:

• Lean's JSON printer escapes only characters below U+0020, so U+0085 (NEL), U+2028 and U+2029 reach a record unescaped.
• The readers split probe output with str.splitlines, which breaks a line at each of those three characters.
• The record was cut in two, and the run failed with "emitted invalid JSON". A U+2028 in a docstring or source slice of a requested declaration was enough.

The skeleton, impact (constants and module evidence) and unused-hypotheses readers now split at "\n" only, as the library probe's reader already does. This change is its own commit, so it can be split out.

Tests

• test_both_probes_read_more_modules_than_lean_compiles_in_a_list (real Lean): both audit probes get 3,000 modules. Each compiles, reads its list, and stops at its first check outside the audit step.
• test_probe_reads_more_roots_than_lean_compiles_in_a_list in test_skeleton.py (real Lean): now also passes 3,001 library roots. An absent root whose quoted component holds a newline, a backspace, DEL, NEL and U+2028 comes back unchanged.
• The glob walk decoder runs in the existing real-Lean test_import_impact_refuses_a_glob_module_the_inventory_lacks, whose refusal names the glob and the module it found.
• Reader tests with NEL, U+2028 and U+2029 in a record, for the skeleton, impact (both readers) and unused-hypotheses readers.
• The render tests now decode the JSON strings.

Overlap

The #213 stack rewrites the skeleton probe's run_cmd block and render_probe. Whichever lands second resolves one hunk in each, plus _requested in test_skeleton.py: #213's AutoformSkeleton.main would take the library roots as a JSON string too. I'll recheck against #213's new head once it is pushed.

This machine is over the agreed load limit for local Lean and pytest runs, so CI on this PR is the test run.

[Deicyde]

Verdict: ready to merge once it is out of draft. This is an adversarial review of head 306ccc3. Two reviewers covered the Lean side and the Python, test and completeness side, and a verifier then tried to refute every finding. No blocker or should-fix survived. Six optional nits did.

What was checked

• CI: all 11 checks pass on 306ccc3, real Lean included: https://github.com/facebookresearch/autoform-bot/actions/runs/38498077842
  • The real-Lean steps run with AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1, so no real-Lean test can skip silently.
  • The new real-Lean audit test ran: audit and contract shows 120 passed, against 119 on main.
  • The "Audit the created project" step ran this template's probe on a project that imports all of Mathlib, and it ended with "kernel trust clean".
• The scaling fix: main's audit template fails at 2,000 and 3,000 modules with "maximum recursion depth reached in the code generator". This branch's template reaches its first check at 1,000, 1,500, 2,000 and 3,000: https://github.com/facebookresearch/autoform-bot/actions/runs/38497826590
• Semantics: each changed probe was rendered from main and from this branch with the same inputs, and the new JSON was decoded the way the Lean decoders do.
  • Inputs covered quoted and numeric components, numbers past 2^64, dots and spaces inside guillemets, quotes, backslashes, Windows paths, characters outside the BMP, U+2028 and U+2029, empty lists, duplicates, and ordering.
  • Every input the old renderers could render decodes to the same Name.
  • The only difference is in names holding a backspace or form feed. The old single-layer encoding wrote them as \b or \f escapes, which Lean string literals reject; the double encoding carries them.
• Toolchains: the README sets v4.27.0 as the minimum.
  • Every API the new decoders use has the same signature in every toolchain from v4.27.0 through v4.35.0: Json.parse, getArr?, getArrVal?, getStr?, getNat?, Array.foldlM and mapM, List.mapM, System.FilePath.mk.
  • The new nameOf clashes with nothing in Lean, Init or Std.
• The second commit's premise: in those same toolchains, escapeAux in Lean's JSON printer escapes only ", \, newline, CR and characters below U+0020.
  • So U+0085, U+2028 and U+2029 reach records raw.
  • split("\n") still handles CRLF, since a trailing \r is JSON whitespace.
  • The library probe's reader already splits at \n.
  • No other generated list grows with the project: core_roots has 4 entries and the audit's allowed has 3.
• Test runtime: the 3,001 library roots cost nothing measurable. The real-Lean skeleton suite took 1083 s here and 1069 s on Free the portable capture's state without the cyclic collector #294's run in the same window.

Optional nits. None of these blocks merge.

1. Error message: a malformed library-roots payload is reported as "the requested roots are malformed". That's because the skeleton probe now decodes both lists with requestedRoots (skeleton_probe.lean:736). Only a CLI bug can produce such a payload. The impact probe and the audit give each list its own message.
2. Unpinned ensure_ascii=False on the glob walks: no test pins it.
   • Dropping the outer ensure_ascii=False would still pass every test.
   • But a glob directory holding a character outside the BMP would then reach Lean as two NUL characters, and the probe would stop with "the glob directory list is malformed".
   • A non-BMP walk directory in test_rendered_probe_imports_modules_and_names_exact_local_modules, plus a check that the probe has no \ud8 escape, would pin it.
   • The old single-layer form was not pinned either.
3. The library roots are never shown to take effect: test_probe_reads_more_roots_than_lean_compiles_in_a_list passes 3,001 of them. That shows the probe compiles and decodes them, not that it applies them, because found depends only on env.contains. One assertion on a found root's trusted list would close that.
4. Inaccurate comment: the comment moved into _json_modules says "Lean reads a JSON surrogate pair as two NUL characters".
   • Lean's JSON parser decodes surrogate pairs. The NUL characters come from a Lean string literal reading the escape.
   • So the ensure_ascii=False that matters is the outer one, while the comment sits above the inner one.
5. Dotted quoted module untested: no audit test has a quoted module with a dot, such as Fixture.«a.b». So a module.split(".") mutant of _json_modules passes every test. It would fail closed, because the import fails, and the gap predates this PR.
6. Follow-up, not for this PR: isRoot still runs List.contains over the module list once per constant.
   • This predates the PR.
   • The probe's kernel replay of every root constant costs far more.
   • For very large root packages, a Std.HashSet would be the next step.

Overlap with the #213 stack. I rechecked against #213 at 7d32fe5 and #284 at c897e96. Merging either with this PR conflicts in four files, and one assertion breaks without a conflict. Whichever lands second can resolve it like this:

• autoform_cli/probes/skeleton_probe.lean: keep Extract Lean skeletons one probe per root module #213's def main, with two changes:
  • change its signature to def main (projectRoots roots : String) : CommandElabM Unit :=;
  • make this the first line of its do block: let projectRoots := (← requestedRoots projectRoots).toList.map (·.2).
• autoform_cli/skeleton.py (render_probe): keep Extract Lean skeletons one probe per root module #213's lines, with project = _lean_requests(tuple(sorted(set(project_roots)))) and run_cmd AutoformSkeleton.main {project} {_lean_requests(roots)}.
• tests/test_skeleton.py:
  • _requested reads both string arguments of AutoformSkeleton.main, and a library_roots=True flag picks the first.
  • The quoted-components test checks the library roots through it.
  • test_probe_elaborates_no_helper_under_the_project_imports merges cleanly but still spells out the old literal. Its last expected line becomes "run_cmd AutoformSkeleton.main " + json.dumps(json.dumps([["Skel", ["Skel"]]])) + " " + json.dumps(json.dumps([["Skel.x", ["Skel", "x"]]])).
• tests/test_impact.py: take this PR's side of both hunks. The glob walks are JSON now, so Extract Lean skeletons one probe per root module #213's Lean.Name.str spellings of them go away.

A merge of this PR into #213 with exactly that resolution passes the full CI, real Lean included: https://github.com/facebookresearch/autoform-bot/actions/runs/38499643799

Posted by PR swarm: PR Swarm Lead