Add bounded Lean project inspection

[Deicyde]

Part of the reviewed split of #8. This PR is independent of #13.

What this adds

• autoform project inspect [path] [--json]: a read-only report on the nearest Lean project: the package name and targets from lakefile.toml, the Lean toolchain, the Mathlib that lake-manifest.json locks, Autoform scaffold paths, and whether that Lean/Mathlib pair is in the bundled release catalog.
• autoform project versions [--json]: lists the catalog (one pair today, Lean and Mathlib v4.32.2).

Nothing runs Lake, Lean, Git, or the network.

How compatibility is decided

• supported: the toolchain and the locked Mathlib commit match a catalog entry.
• unlisted: both are known, but the pair is not in the catalog.
• indeterminate: no manifest, no Mathlib, a lakefile.lean (never evaluated), a path-based Mathlib, or any file error.

The rules follow the tools, checked against elan 4.2.0 and Lake 4.32.0. elan reads only the trimmed first line of lean-toolchain and ignores the file when that line is blank or malformed. Lake builds the manifest's lock (a stale lock gets a warning), applies .lake/package-overrides.json over the manifest, and refuses a lakefile.toml with no name, a malformed version, or duplicate targets. Credentials in a Mathlib URL are redacted from reports.

History

The first version of this PR (5.2k lines) hardened every read against concurrent modification with descriptor walks, generation rechecks, and no-follow paths. That made inspection fail on Windows and under symlinked paths such as macOS /tmp, and four review rounds kept finding new edge cases. f7bfd97 cuts it to plain size-capped reads. 44fd1f2 restores the behaviours the cut lost, found by running the previous 190-test suite against the new code. The remaining differences are deliberate: symlinks and case variants are treated as Lake treats them, and Lean's name grammar for manifest root names is not re-implemented.

Code that later PRs used from the first version moves into them: bounded_toml.py to #16, configuration hashes to #32, and inspection bound to a staged directory to #26. Write-side case-collision hardening is tracked separately in #62.

Validation

• tests/test_project_inspect.py: 82 passed on Python 3.13, with each guard mutation-tested
• full suite: 804 passed, 29 skipped
• local projects (cft-challenges, tao-measure-lean, Velvet, Veil, Mathlib itself, and three more) get the same answers as the first version
• ruff check autoform_cli servers tests

Reference implementation: #8

[Deicyde]

Review result: changes needed.

• project/inspect.py:494-503 probes lowercase blueprint without requiring exact directory-entry spelling. On default macOS filesystems, formal-math's tracked Blueprint/ Lean library is falsely reported as an Autoform vault; Linux reports differently.
• project/inspect.py:257-266 rejects projects containing both Lake configuration formats, although Lake 4.32.2 validly selects lakefile.lean. Treat the unused file as an advisory diagnostic or document the stricter policy.
• project/inspect.py:819-825 permits C1 controls such as U+009B and prints them raw in human output. Apply the catalog's Unicode control/surrogate rejection consistently.

All three cases were reproduced; the focused inspection suite still passes.

[Deicyde]

Second pass on exact head 8bbe9d8, in addition to the three findings already filed:

1. P1: compatibility can be computed from a project state that never existed. The root descriptor is retained, but Lake, toolchain, and manifest files are read sequentially without a generation recheck (project/inspect.py:60-67,606-676). I began with Mathlib 4.32.2 plus Lean 4.31.0, switched to Mathlib 4.31.0 plus Lean 4.32.2 after the Lake read, and received status: supported for the synthetic 4.32.2 pair. Snapshot all decision-file identities/content together, or revalidate and retry/fail on change.

2. P2: nonregular config nodes are opened before being rejected. _relative_status identifies a FIFO as unsafe, but _inspect_lake treats every non-missing status as readable and _read_file opens it before fstat (inspect.py:257-280,625-653). Opening a FIFO unblocked a waiting writer even though inspection later emitted lake-config-not-regular; device opens can have stronger effects. Reject the known non-file status before opening, while retaining the post-open race check.

3. P2: a Lake-valid dependency is rejected. Explicit scope = "" is Lake's accepted default (tryDecodeD scope ""), including for a direct Git dependency. Exact Lake 4.32.2 accepts and translates it, while inspection returns invalid-lake-field, discards the Lake/Mathlib model, and marks compatibility indeterminate (inspect.py:697-700). Treat absent and explicit-empty scope equivalently.

4. P2: the documented offline operation can invoke account-service I/O without a deadline. Path(target).expanduser() (inspect.py:121) resolves ~user through pwd.getpwnam, which may use LDAP/NIS/SSSD. Restrict expansion to the current user's local home semantics or reject named-user forms.

5. P2: project inspect is unavailable on Windows without that limitation being declared. The capability gate requires POSIX O_NOFOLLOW, O_DIRECTORY, and dir-fd operations, so every Windows call returns secure-file-inspection-unavailable. Add a safe backend or explicitly scope and test platform support.

6. P3: malformed target paths escape the stable diagnostic contract. inspect_project("\0") raises ValueError, and an unencodable surrogate raises UnicodeEncodeError; _entry_status/_open_directory catch only OSError. Convert these to target-unreadable.

7. P3: the compatibility catalog accepts contradictory release metadata. A catalog entry pairing toolchain leanprover/lean4:v4.32.2 with lean.version = "v9.9.9" parses and certifies a 4.32.2 project because matching ignores the version field (catalog.py:55-72, inspect.py:550-558). Validate consistency inside the authority document.

Validation: all 91 project-inspection tests pass; the first four behaviors were reproduced independently.

[Deicyde]

Third pass on exact head 32e76b7. Review result: changes needed.

13 of the 17 earlier findings are fixed, including the generation recheck, rejecting FIFOs before opening them, explicit empty scope, and the malformed-target exceptions. Four problems block merging. Three make the compatibility answer, the headline feature, wrong or missing in common cases; the fourth is a regression from the last fix round. All four were reproduced on 32e76b7.

Blocking

1. P1: compatibility ignores lake-manifest.json, so supported is reported while Lake builds a different Mathlib. _compatibility (project/inspect.py:807-847) compares only lean-toolchain with the lakefile.toml require, and _optional_digest (:849-867) only hashes the manifest. Bump the lakefile to Mathlib v4.32.2 and the toolchain to v4.32.2 without running lake update, so the manifest still locks v4.31.0: lake build only warns manifest out of date: git revision of dependency 'mathlib' changed and builds the locked v4.31.0 (Lake's materializeDeps/validateManifest in Load/Resolve.lean), while inspection reports supported (lean-v4.32.2-mathlib-v4.32.2) with no diagnostic. A manifest with "version": "2.0.0" or invalid JSON, which Lake refuses to load (Manifest.lean:217-230), also yields supported. Fix: parse the manifest with Lake's version rules, treat the root's direct mathlib entry (url, inputRev, rev) as what will be built, and never claim supported when it disagrees with the require (emit a stale-manifest diagnostic instead). Adding the Mathlib commit to the catalog (v4.32.2 is 905b95818eb32af7874a58b427f50c1711a5e96c) lets the locked rev be checked exactly instead of trusting a tag name. .lake/package-overrides.json can also replace entries: account for it, or do not report supported when it is present.

2. P1: catalog matching cannot recognize Lake's own Mathlib template or any real project checked. _parse_mathlib (:903-930) returns None unless the require has a git key, but lake new foo math writes scope = "leanprover-community" plus rev = "v4.32.2" (mathTomlConfigFileContents in Lake's CLI/Init.lean). At exactly the catalog pair, inspection reports mathlib: null, indeterminate, and "Offline inspection cannot determine a Lean and Mathlib release pair", which is false whenever a manifest exists, since the manifest records the Mathlib url, inputRev and locked rev. Three real Mathlib projects (all using the scope form) also come back indeterminate, and test_lake_generated_scope_requirement_is_indeterminate_offline (tests/test_project_inspect.py:593) pins this outcome. The exact-string URL match also rejects https://github.com/leanprover-community/mathlib4 without .git, which is the URL the manifest records. Decision needed before freezing schema v1: how a catalog entry identifies Mathlib (git URL, Reservoir scope and name, or the manifest entry). Fix together with item 1: resolve scope-form requires through the root manifest entry, normalize URLs, and report indeterminate only when no usable manifest exists.

3. P1: a case-variant Lakefile.lean is hidden on macOS while Lake executes it. With Lakefile.lean next to lakefile.toml on default case-insensitive APFS, inspection returns ok: true, lake.format: "toml" and no lakefile-lean-not-evaluated warning. Lake 4.32.2 in the same directory prints lakefile.lean and lakefile.toml are both present; using lakefile.lean and evaluates the file (its #eval ran). This contradicts the README ("A lakefile.lean ... takes precedence over lakefile.toml, matching Lake") and hides exactly the fact that warning exists to report. Cause: the exact-spelling rule added for Blueprint/ (_exact_entry_exists, :698, used by _relative_info at :718-719, by _capture_file and by _open_parent_descriptor) reports any case variant as missing, for Lake configuration as well as for Autoform scaffold paths. The same rule makes discovery skip a subpackage whose only marker is Lakefile.toml. Fix: distinguish "exists under some spelling" (a no-follow stat of the canonical name succeeds) from "exists under the exact spelling"; treat a case-variant decision file as present for precedence and fail closed with a dedicated diagnostic; keep exact spelling only for scaffold detection. Add a test that is skipped on case-sensitive filesystems. While there: every existence check lists the whole parent directory (23 to 37 listdir calls per run, 3 to 4 s with 15,000 entries in the root), so list each directory at most once per attempt or check per name.

4. P2: an unreadable decision file now aborts as project-changed-during-inspection (regression from 3a259da). chmod 000 on lake-manifest.json, lean-toolchain or lakefile.toml of a stable supported project returns only project-changed-during-inspection, status indeterminate, lake: null. At 8bbe9d8 the same cases gave lake-manifest-unreadable (a warning, still supported), lean-toolchain-unreadable and lake-config-unreadable. Cause: _capture_file records a failed open or read as _SnapshotEntry("unreadable", None, None) (:378, :390, :406, :438), and the recheck (:339-344) compares that with a fresh stat that still says file, so every attempt counts as changed and the accurate diagnostics are discarded after _SNAPSHOT_ATTEMPTS. Fix: compare stat-derived identity with stat-derived identity (keep content None and the unreadable diagnostic), and add chmod-000 tests for the manifest and the toolchain. While reworking the snapshot:

   • Make content the generation token: re-read each file and compare bytes or a digest. The metadata check misses a same-size rewrite within one timestamp tick on coarse-timestamp filesystems, and replacing the torn-read check with changed = False fails no test.
   • Compare only type and inode for nodes whose content is never read (.git, blueprint, mkdocs.yml, the workflow files): churn inside .git made 3 of about 2,000 stable inspections fail.

Non-blocking follow-ups (the cheap ones are better done before JSON v1 freezes)

• project_root is always "." (:104), so a report never says which directory it describes. Inspecting .lake/packages/mathlib/Mathlib/Algebra silently reports the nested Mathlib package. Report the root relative to the target (for example ../..).
• Format, bidi and line-separator characters (Cf, Zl, Zp, such as U+202E and U+2028) from project files are printed raw in the human report, so report lines can be forged. Escape them in _print_project_inspection (which also fixes the UnicodeEncodeError on a non-UTF-8 stdout) or reject them in consumed fields.
• The no-follow policy also applies above the project root: inspect /tmp/proj fails on macOS, as does a project under a symlinked ~/code or under an execute-only ancestor. Apply it from the discovered root down, or document it and name the offending path component.
• ~\x still reaches pwd.getpwnam on POSIX (earlier finding 4 is only partly fixed). Expand only a bare ~ or a ~/ prefix, from HOME.
• On Python 3.10 the locked tomli 2.4.1 accepts TOML 1.1 that Lake and tomllib on 3.11+ reject, so results depend on the Python version (the same gap exists on main).
• Keys Lake accepts and ignores (lean_lib.root, lean_exe.roots) and Lake's git = {url, subDir} table form are rejected as invalid-lake-field, which discards the whole model. lean-toolchain forms that elan accepts (a trailing blank line, a bare vX.Y.Z) are rejected or left unnormalized.
• Guards with no test that fails when they are removed: the 2 MiB read cap, control-character rejection in Lake strings, never opening an ignored lakefile.toml (32e76b7), each TOML depth guard on its own (test_toml_depth_limit_is_independent_of_python_recursion_limit has no effect), and several post-open race guards.
• skeleton.lean_libraries is a second Lake-config reader with toml-first precedence and unbounded TOML parsing (this predates the PR). autoform_cli.project should become the single authority.
• Nits: the catalog validator still accepts duplicate release pairs, ids that contradict their contents and URLs no project could match (earlier finding 7 is only partly fixed); unreadable paths get *-is-symlink codes; the README says symlinked decision-bearing files fail inspection, but a symlinked manifest only warns; small JSON shape inconsistencies; a few conditions that can never be true.

Validation: every blocking item was reproduced independently on 32e76b7. The Lake side of items 1 and 3 was confirmed with real Lake 4.32.2: a stale-manifest build against a local two-tag Mathlib repository, and lake env on the case-variant project. The tree merged with current main passes 281 tests, with only the known test_plugin_runtime load flake failing; ruff is clean.

[Deicyde]

Fourth-pass blockers are fixed at 7a175f8: Blueprint/ Lean libraries no longer trip scaffold alias errors; unsafe raw Git URLs cannot normalize into catalog matches; catalog material paths are canonical and material identities unique; and human output escapes nonprintable input across Python Unicode versions. Real formal-math now exits 0. Validation: 190 focused tests on Python 3.10 and 190 on 3.13, independent re-audits approved, and all five GitHub checks are green. The separate write-side scaffold collision is tracked in #62.

[Deicyde]

The slimmer current head is easier to review, but three headline blockers remain:

1. Incomplete Lake decoding can yield false supported. A catalog-exact
   manifest with "inherited": "false" returns ok:true/supported, while Lake
   rejects inherited: Bool expected. Likewise scope = 7 in the active TOML
   requirement is ignored while Lake rejects it.
2. Decision files are read sequentially without a coherent snapshot. I swapped
   Lean/Mathlib states after the toolchain read; neither real state was
   supported, but inspection synthesized a supported pair that never existed.
3. _read_text checks is_file() and then reopens by pathname. Replacing a
   regular lakefile.toml with a FIFO between those calls made inspection read
   from the FIFO with no diagnostic.

Please keep the slim public model, but strictly decode every Lake-consumed field
before certification; snapshot the small decision-file set in memory and
reread/compare bytes before returning (retry or fail on change); and read each
file through a nonblocking descriptor with fstat regular-file verification
before bounded reads. Add the three exact regressions. Real formal-math,
hatcher-at, and zeta7 behavior otherwise looks correct, and the wheel/package
surface is clean.