Add bounded Lean project inspection

autoform_cli/README.md

@@ -127,6 +127,29 @@ autoform init . --title "Finite Flat Group Schemes" \
 Pass `--autoform-ref <sha>` to pin the generated workflows at an immutable
 commit, `--force` to overwrite, and `--json` for machine-readable output.
 
+Inspect a Lean project and list Autoform's bundled known-good release pairs:
+
+```bash
+autoform project inspect .
+autoform project inspect path/inside/project --json
+autoform project versions --json
+```
+
+`project inspect` reads the nearest enclosing project's `lean-toolchain`,
+`lake-manifest.json`, and `lakefile.toml` without running Lake, Lean, Git, or
+the network. Compatibility is decided by the toolchain and the Mathlib commit
+the manifest locks, which is what `lake build` uses: `supported` when that pair
+is in the bundled catalog, `unlisted` when it is not, and `indeterminate` when
+either is unknown (no manifest, no Mathlib, a path-based Mathlib, or any file
+error). A `.lake/package-overrides.json` entry for Mathlib replaces the
+manifest's, and a `lakefile.toml` that requests a different Mathlib than the
+lock gets a `lake-manifest-stale` warning. `lakefile.lean` takes precedence, as
+in Lake, but is never evaluated, so its projects stay `indeterminate`. As in
+elan, only the trimmed first line of `lean-toolchain` counts.
+
+`project versions` lists the bundled catalog of known-good Lean and Mathlib
+pairs. It is an allowlist, not a resolver.
+
 Publishing a project runs four steps in order: validate, write the Mermaid
 graph into the vault, render the site source, then strict-build the site.
 

autoform_cli/__main__.py

@@ -19,6 +19,7 @@
 from .doctor import diagnose_project
 from .graph import GraphValidationError, load_graph
 from .lean import build_linker, declaration_names
+from .project import ProjectCatalogError, inspect_project, load_release_catalog
 from .render import PublicationError, render_site
 from .scaffold import ScaffoldError, scaffold_project
 from .skeleton import (
@@ -71,6 +72,19 @@ def main(argv: Sequence[str] | None = None) -> int:
     doctor.add_argument("--lean-root", type=Path, help="Lean project to resolve local targets against")
     doctor.add_argument("--json", action="store_true", help="write stable machine-readable output")
 
+    project = subparsers.add_parser("project", help="inspect local project configuration and releases")
+    project_subparsers = project.add_subparsers(dest="project_command", required=True)
+    project_inspect = project_subparsers.add_parser(
+        "inspect", help="inspect a project without running Lake, Git, or network operations"
+    )
+    project_inspect.add_argument(
+        "target", nargs="?", default=".", help="a path inside the project (default: current directory)"
+    )
+    project_inspect.add_argument("--json", action="store_true", help="write stable machine-readable output")
+    project_versions = project_subparsers.add_parser(
+        "versions", help="list bundled known-good Lean and Mathlib releases"
+    )
+    project_versions.add_argument("--json", action="store_true", help="write stable machine-readable output")
     claim = subparsers.add_parser("claim", help="coordinate temporary node ownership through Git refs")
     claim_subparsers = claim.add_subparsers(dest="claim_command", required=True)
     for operation in ("acquire", "renew", "release"):
@@ -167,6 +181,8 @@ def main(argv: Sequence[str] | None = None) -> int:
         return _audit(args)
     if args.command == "doctor":
         return _doctor(args)
+    if args.command == "project":
+        return _project(args)
     if args.command == "claim":
         return _claim(args)
     if args.command == "migrate":
@@ -296,6 +312,65 @@ def _doctor(args: argparse.Namespace) -> int:
     return 0 if result.clean else 1
 
 
+def _project(args: argparse.Namespace) -> int:
+    try:
+        catalog = load_release_catalog()
+    except ProjectCatalogError as error:
+        if args.json:
+            print(json.dumps({"error": {"code": "project-catalog-invalid", "message": str(error)}, "ok": False}))
+        else:
+            print(f"error: {error}", file=sys.stderr)
+        return 1
+    if args.project_command == "versions":
+        if args.json:
+            print(catalog.to_json())
+            return 0
+        print("Known-good Lean/Mathlib releases:")
+        for release in catalog.releases:
+            print(f"  {release.id}{' [recommended]' if release.recommended else ''}")
+            print(f"    Lean: {release.lean_toolchain}")
+            print(f"    Mathlib: {release.mathlib_rev} @ {release.mathlib_commit} ({release.mathlib_git})")
+        return 0
+    result = inspect_project(args.target, catalog=catalog)
+    if args.json:
+        print(result.to_json())
+    else:
+        _print_project_inspection(result)
+    return 0 if result.ok else 1
+
+
+def _print_project_inspection(result) -> None:
+    if result.project_root is not None:
+        print(f"Project root: {_human_text(result.project_root)}")
+    if result.lake is not None:
+        version = f" {result.lake.version}" if result.lake.version else ""
+        print(f"Lake: {_human_text((result.lake.name or 'unknown package') + version)} ({result.lake.config})")
+        for target in result.lake.targets:
+            print(f"  {target.kind} {_human_text(target.name)}")
+    if result.lean_toolchain is not None:
+        print(f"Lean: {_human_text(result.lean_toolchain)}")
+    if result.mathlib is not None:
+        mathlib = result.mathlib
+        where = mathlib.dir if mathlib.type == "path" else f"{mathlib.input_rev} @ {mathlib.rev} ({mathlib.url})"
+        print(f"Mathlib: {_human_text(where)} [{mathlib.source}]")
+    if result.autoform_paths:
+        print(f"Autoform: {', '.join(result.autoform_paths)}")
+    release = f" ({result.compatibility.release})" if result.compatibility.release else ""
+    print(f"Compatibility: {result.compatibility.status}{release}")
+    for diagnostic in result.diagnostics:
+        location = f" {diagnostic.path}" if diagnostic.path else ""
+        print(f"{diagnostic.severity}[{diagnostic.code}]{location}: {diagnostic.message}", file=sys.stderr)
+
+
+def _human_text(value: object) -> str:
+    """Escape nonprintable characters so project files cannot forge report lines."""
+
+    return "".join(
+        character if character.isprintable() else character.encode("unicode_escape").decode("ascii")
+        for character in str(value)
+    )
+
+
 def _claim(args: argparse.Namespace) -> int:
     try:
         board = _claim_board(args)

autoform_cli/project/__init__.py

@@ -0,0 +1,21 @@
+"""Offline Lean project inspection and supported release data."""
+
+from .catalog import (
+    RELEASE_CATALOG_SCHEMA,
+    ProjectCatalogError,
+    ReleaseCatalog,
+    load_release_catalog,
+    parse_release_catalog,
+)
+from .inspect import PROJECT_INSPECTION_SCHEMA, ProjectInspection, inspect_project
+
+__all__ = [
+    "PROJECT_INSPECTION_SCHEMA",
+    "RELEASE_CATALOG_SCHEMA",
+    "ProjectCatalogError",
+    "ProjectInspection",
+    "ReleaseCatalog",
+    "inspect_project",
+    "load_release_catalog",
+    "parse_release_catalog",
+]

autoform_cli/project/catalog.py

@@ -0,0 +1,93 @@
+"""Autoform's bundled list of known-good Lean and Mathlib release pairs."""
+
+from __future__ import annotations
+
+import json
+import re
+from dataclasses import asdict, dataclass
+from importlib.resources import files
+
+RELEASE_CATALOG_SCHEMA = "autoform-project-release-catalog/v1"
+_COMMIT = re.compile(r"[0-9a-f]{40}")
+
+
+class ProjectCatalogError(ValueError):
+    """The bundled release catalog is missing or malformed."""
+
+
+@dataclass(frozen=True, slots=True)
+class SupportedRelease:
+    id: str
+    recommended: bool
+    lean_toolchain: str
+    mathlib_git: str
+    mathlib_rev: str
+    mathlib_commit: str
+
+
+@dataclass(frozen=True, slots=True)
+class ReleaseCatalog:
+    releases: tuple[SupportedRelease, ...]
+
+    @property
+    def recommended(self) -> SupportedRelease:
+        return next(release for release in self.releases if release.recommended)
+
+    def match(self, lean_toolchain: str, mathlib_git: str | None, mathlib_commit: str | None) -> SupportedRelease | None:
+        commit = None if mathlib_commit is None else mathlib_commit.lower()  # Git reads either case
+        return next(
+            (
+                release
+                for release in self.releases
+                if release.lean_toolchain == lean_toolchain
+                and release.mathlib_commit == commit
+                and canonical_git_url(release.mathlib_git) == canonical_git_url(mathlib_git)
+            ),
+            None,
+        )
+
+    def as_dict(self) -> dict[str, object]:
+        return {"releases": [asdict(release) for release in self.releases], "schema": RELEASE_CATALOG_SCHEMA}
+
+    def to_json(self) -> str:
+        return json.dumps(self.as_dict(), sort_keys=True, separators=(",", ":"))
+
+
+def canonical_git_url(url: str | None) -> str | None:
+    """Drop the trailing `/` and `.git`, which do not change the repository a URL names."""
+
+    return None if url is None else url.rstrip("/").removesuffix(".git")
+
+
+def load_release_catalog() -> ReleaseCatalog:
+    try:
+        payload = json.loads(files(__package__).joinpath("releases.json").read_text(encoding="utf-8"))
+    except (OSError, ValueError) as error:
+        raise ProjectCatalogError("the bundled release catalog is unreadable") from error
+    return parse_release_catalog(payload)
+
+
+def parse_release_catalog(payload: object) -> ReleaseCatalog:
+    try:
+        if payload["schema"] != RELEASE_CATALOG_SCHEMA:
+            raise ProjectCatalogError("the release catalog has an unsupported schema")
+        releases = tuple(SupportedRelease(**entry) for entry in payload["releases"])
+    except (KeyError, TypeError) as error:
+        raise ProjectCatalogError("the release catalog is malformed") from error
+    for release in releases:
+        strings = (release.id, release.lean_toolchain, release.mathlib_git, release.mathlib_rev, release.mathlib_commit)
+        if (
+            not all(isinstance(value, str) and value for value in strings)
+            or not isinstance(release.recommended, bool)
+            or not _COMMIT.fullmatch(release.mathlib_commit)
+        ):
+            raise ProjectCatalogError(f"release {release.id!r} is malformed")
+    pairs = {(release.lean_toolchain, release.mathlib_commit) for release in releases}
+    if (
+        not releases
+        or len({release.id for release in releases}) != len(releases)
+        or len(pairs) != len(releases)
+        or sum(release.recommended for release in releases) != 1
+    ):
+        raise ProjectCatalogError("releases need unique ids and pairs, with exactly one recommended")
+    return ReleaseCatalog(releases)