diff --git a/autoform_cli/README.md b/autoform_cli/README.md index b8fcae37..59651f3e 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -127,6 +127,29 @@ autoform init . --title "Finite Flat Group Schemes" \ Pass `--autoform-ref ` 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. diff --git a/autoform_cli/__main__.py b/autoform_cli/__main__.py index a73fc876..39a278e0 100644 --- a/autoform_cli/__main__.py +++ b/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) diff --git a/autoform_cli/project/__init__.py b/autoform_cli/project/__init__.py new file mode 100644 index 00000000..b65259cd --- /dev/null +++ b/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", +] diff --git a/autoform_cli/project/catalog.py b/autoform_cli/project/catalog.py new file mode 100644 index 00000000..64212c3d --- /dev/null +++ b/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) diff --git a/autoform_cli/project/inspect.py b/autoform_cli/project/inspect.py new file mode 100644 index 00000000..be00e649 --- /dev/null +++ b/autoform_cli/project/inspect.py @@ -0,0 +1,475 @@ +"""Inspect a local Lean project's configuration without running Lake, Lean, or Git. + +Compatibility is decided by `lean-toolchain` and the Mathlib entry that +`lake-manifest.json` locks, which is what `lake build` materializes; a +`.lake/package-overrides.json` entry replaces it. `lakefile.toml` is read for +the package name, targets, and whether the lock is used and current. +`lakefile.lean` is never evaluated, so those projects stay indeterminate. +""" + +from __future__ import annotations + +import json +import os +import re +from collections.abc import Callable +from dataclasses import asdict, dataclass +from pathlib import Path + +from .catalog import ReleaseCatalog, canonical_git_url, load_release_catalog + +try: # Python 3.11+ + import tomllib +except ModuleNotFoundError: # pragma: no cover - Python 3.10 + import tomli as tomllib # type: ignore[no-redef] + +PROJECT_INSPECTION_SCHEMA = "autoform-project-inspection/v1" +_MAX_FILE_BYTES = 1024 * 1024 +_ROOT_MARKERS = ("lakefile.lean", "lakefile.toml", "lean-toolchain") +_MANIFEST = "lake-manifest.json" +_OVERRIDES = ".lake/package-overrides.json" +_MATHLIB = ("mathlib", "«mathlib»") # Lake reads both spellings as the same name +_LAKE_VERSION = re.compile(r"[0-9]+\.[0-9]+\.[0-9]+(?:-[^ \t\r\n]+)?") # Lake's StdVer +_MANIFEST_VERSION = re.compile(r"([0-9]+)\.([0-9]+)\.([0-9]+)(?:-\S+)?") +_URL_CREDENTIALS = re.compile(r"^([A-Za-z][A-Za-z0-9+.-]*://)[^/@]*@") +_AUTOFORM_PATHS: dict[str, Callable[[Path], bool]] = { + "blueprint": Path.is_dir, + "mkdocs.yml": Path.is_file, + ".github/workflows/autoform-verify.yml": Path.is_file, + ".github/workflows/blueprint-pages.yml": Path.is_file, +} + + +@dataclass(frozen=True, slots=True) +class ProjectDiagnostic: + severity: str + code: str + message: str + path: str | None = None + + +@dataclass(frozen=True, slots=True) +class LakeTarget: + kind: str + name: str + + +@dataclass(frozen=True, slots=True) +class LakeProject: + config: str + name: str | None + version: str | None + targets: tuple[LakeTarget, ...] + + +@dataclass(frozen=True, slots=True) +class MathlibLock: + """A Lake manifest or package-overrides entry for Mathlib.""" + + type: str + source: str + inherited: bool + url: str | None = None + input_rev: str | None = None + rev: str | None = None + dir: str | None = None + sub_dir: str | None = None + config_file: str | None = None + manifest_file: str | None = None + + @property + def loads_like_a_release(self) -> bool: + """Whether Lake loads Mathlib from its repository root with its own lakefile and manifest.""" + + return ( + self.type == "git" + and self.sub_dir in (None, "", ".") + and self.config_file == "lakefile.lean" + and self.manifest_file == "lake-manifest.json" + ) + + +@dataclass(frozen=True, slots=True) +class ProjectCompatibility: + status: str + release: str | None + recommended_release: str + + +@dataclass(frozen=True, slots=True) +class ProjectInspection: + project_root: str | None + lake: LakeProject | None + lean_toolchain: str | None + mathlib: MathlibLock | None + autoform_paths: tuple[str, ...] + compatibility: ProjectCompatibility + diagnostics: tuple[ProjectDiagnostic, ...] + + @property + def ok(self) -> bool: + return not any(diagnostic.severity == "error" for diagnostic in self.diagnostics) + + def as_dict(self) -> dict[str, object]: + return {**asdict(self), "ok": self.ok, "schema": PROJECT_INSPECTION_SCHEMA} + + def to_json(self) -> str: + return json.dumps(self.as_dict(), sort_keys=True, separators=(",", ":")) + + +def inspect_project(target: str | Path, *, catalog: ReleaseCatalog | None = None) -> ProjectInspection: + catalog = catalog or load_release_catalog() + diagnostics: list[ProjectDiagnostic] = [] + try: + start = Path(target).expanduser().resolve(strict=True) + if not start.is_dir(): + start = start.parent + root = next( + ( + directory + for directory in (start, *start.parents) + if any(_present(directory / marker) for marker in _ROOT_MARKERS) + ), + None, + ) + except (OSError, RuntimeError, ValueError): + diagnostics.append(ProjectDiagnostic("error", "target-unreadable", "The inspection target cannot be resolved.")) + return _result(catalog, diagnostics) + if root is None: + diagnostics.append( + ProjectDiagnostic("error", "project-not-found", "No enclosing Lean project (lakefile or lean-toolchain).") + ) + return _result(catalog, diagnostics) + + lake, requirement = _inspect_lake(root, diagnostics) + toolchain = _inspect_toolchain(root, diagnostics) + has_manifest = _present(root / _MANIFEST) + if not has_manifest: + diagnostics.append( + ProjectDiagnostic( + "warning", + "missing-lake-manifest", + "There is no lake-manifest.json, so the locked Mathlib is unknown.", + _MANIFEST, + ) + ) + locked = _locked_mathlib(root, _MANIFEST, diagnostics) + override = _locked_mathlib(root, _OVERRIDES, diagnostics) + mathlib = locked + if override is not None and has_manifest: # Lake applies overrides to a manifest's packages + diagnostics.append( + ProjectDiagnostic( + "warning", + "mathlib-overridden", + "Lake uses the Mathlib from package-overrides.json instead of the manifest's.", + _OVERRIDES, + ) + ) + mathlib = override + elif locked is not None and requirement is not None and _is_stale(requirement, locked): + diagnostics.append( + ProjectDiagnostic( + "warning", + "lake-manifest-stale", + "lakefile.toml requests a different Mathlib than the manifest locks; Lake builds the locked one.", + _MANIFEST, + ) + ) + if lake is not None and lake.config == "lakefile.lean": + mathlib = None + elif mathlib is not None and lake is not None and requirement is None and not mathlib.inherited: + diagnostics.append( + ProjectDiagnostic( + "warning", + "mathlib-manifest-unused", + "The manifest locks Mathlib directly, but lakefile.toml does not require it, so Lake will not build it.", + mathlib.source, + ) + ) + mathlib = None + return _result( + catalog, + diagnostics, + project_root="/".join([".."] * (len(start.parts) - len(root.parts))) or ".", + lake=lake, + lean_toolchain=toolchain, + mathlib=mathlib, + autoform_paths=tuple( + path for path, kind in _AUTOFORM_PATHS.items() if _exists_exactly(root, path) and kind(root / path) + ), + ) + + +def _result( + catalog: ReleaseCatalog, + diagnostics: list[ProjectDiagnostic], + *, + project_root: str | None = None, + lake: LakeProject | None = None, + lean_toolchain: str | None = None, + mathlib: MathlibLock | None = None, + autoform_paths: tuple[str, ...] = (), +) -> ProjectInspection: + errors = any(diagnostic.severity == "error" for diagnostic in diagnostics) + release = None + if errors or lean_toolchain is None or mathlib is None or mathlib.type != "git": + status = "indeterminate" + if not errors: + diagnostics.append( + ProjectDiagnostic( + "warning", + "release-indeterminate", + "The Lean toolchain or the Mathlib Lake will build is unknown, so compatibility cannot be checked.", + ) + ) + else: + if mathlib.loads_like_a_release: + release = catalog.match(lean_toolchain, mathlib.url, mathlib.rev) + status = "supported" if release is not None else "unlisted" + if release is None: + diagnostics.append( + ProjectDiagnostic( + "warning", + "release-unlisted", + "This Lean and Mathlib pair is not in the bundled release catalog.", + ) + ) + return ProjectInspection( + project_root=project_root, + lake=lake, + lean_toolchain=lean_toolchain, + mathlib=mathlib, + autoform_paths=autoform_paths, + compatibility=ProjectCompatibility( + status, release.id if release is not None else None, catalog.recommended.id + ), + diagnostics=tuple(sorted(diagnostics, key=lambda item: (item.severity, item.code, item.path or ""))), + ) + + +def _inspect_lake(root: Path, diagnostics: list[ProjectDiagnostic]) -> tuple[LakeProject | None, dict | None]: + if _present(root / "lakefile.lean"): + diagnostics.append( + ProjectDiagnostic( + "warning", + "lakefile-lean-not-evaluated", + "lakefile.lean takes precedence and is not evaluated, so its package, targets, " + "and Mathlib cannot be confirmed.", + "lakefile.lean", + ) + ) + return LakeProject("lakefile.lean", None, None, ()), None + if not _present(root / "lakefile.toml"): + diagnostics.append( + ProjectDiagnostic("error", "missing-lake-config", "The project has no lakefile.toml or lakefile.lean.") + ) + return None, None + text = _read_text(root, "lakefile.toml", diagnostics) + if text is None: + return None, None + try: + config = tomllib.loads(text) + except (tomllib.TOMLDecodeError, RecursionError): + config = None + problem = "it is not valid TOML" if config is None else _lakefile_problem(config) + if problem is not None: + diagnostics.append( + ProjectDiagnostic("error", "invalid-lakefile-toml", f"Lake cannot load lakefile.toml: {problem}.", "lakefile.toml") + ) + return None, None + targets = tuple( + LakeTarget(kind, entry["name"]) for kind in ("lean_lib", "lean_exe") for entry in config.get(kind, []) + ) + # Lake keeps the last of several requirements with the same name. + requirement = next((entry for entry in reversed(config.get("require", [])) if entry["name"] in _MATHLIB), None) + return LakeProject("lakefile.toml", config["name"], config.get("version"), targets), requirement + + +def _lakefile_problem(config: dict) -> str | None: + """Why Lake would refuse the fields Autoform reads, if it would.""" + + if not _is_name(config.get("name")): + return "it has no package name" + version = config.get("version") + if version is not None and not (isinstance(version, str) and _LAKE_VERSION.fullmatch(version)): + return "its version is not major.minor.patch" + if not all(_are_named_tables(config.get(key, [])) for key in ("require", "lean_lib", "lean_exe")): + return "a require, lean_lib, or lean_exe entry has no name" + targets = [entry["name"] for key in ("lean_lib", "lean_exe") for entry in config.get(key, [])] + if len(set(targets)) != len(targets): + return "two targets share a name" + return None + + +def _inspect_toolchain(root: Path, diagnostics: list[ProjectDiagnostic]) -> str | None: + if not _present(root / "lean-toolchain"): + diagnostics.append(ProjectDiagnostic("error", "missing-lean-toolchain", "The project has no lean-toolchain.")) + return None + text = _read_text(root, "lean-toolchain", diagnostics) + if text is None: + return None + # elan reads only the trimmed first line, and silently uses the default + # toolchain when that line is empty or malformed. + toolchain = text.split("\n", 1)[0].strip() + if not toolchain or not toolchain.isprintable() or any(character.isspace() for character in toolchain): + diagnostics.append( + ProjectDiagnostic( + "error", + "invalid-lean-toolchain", + "elan ignores this lean-toolchain because its first line is empty or malformed.", + "lean-toolchain", + ) + ) + return None + return toolchain + + +def _locked_mathlib(root: Path, relative: str, diagnostics: list[ProjectDiagnostic]) -> MathlibLock | None: + """Read the Mathlib entry of a Lake manifest or package-overrides file, if any.""" + + if not _present(root / relative): + return None + text = _read_text(root, relative, diagnostics) + if text is None: + return None + try: + payload = json.loads(text, parse_constant=_reject_json_constant) + layout = _manifest_layout(payload.get("version", payload.get("schemaVersion"))) # overrides use schemaVersion + packages = payload.get("packages") + packages = [] if packages is None else packages # Lake reads null as no packages + if layout is None or not isinstance(packages, list) or not all(isinstance(item, dict) for item in packages): + raise ValueError(relative) + # Lake keeps the last of several packages with the same name. + entry = next((package for package in reversed(packages) if package.get("name") in _MATHLIB), None) + if entry is not None and layout == "current" and entry.get("type") not in ("git", "path"): + raise ValueError(relative) + except (AttributeError, RecursionError, ValueError): + diagnostics.append( + ProjectDiagnostic("error", "invalid-lake-manifest", f"{relative} is not a Lake manifest Autoform reads.", relative) + ) + return None + if layout == "legacy": + diagnostics.append( + ProjectDiagnostic( + "warning", + "unsupported-lake-manifest", + f"Lake still reads the legacy layout of {relative}, but Autoform does not; `lake update` rewrites it.", + relative, + ) + ) + return None + if entry is None: + return None + common = {"source": relative, "inherited": entry.get("inherited") is True} + if entry["type"] == "path": + return MathlibLock("path", dir=_string(entry.get("dir")), **common) + return MathlibLock( + "git", + url=_redact(_string(entry.get("url"))), + input_rev=_string(entry.get("inputRev")), + rev=_string(entry.get("rev")), + sub_dir=_string(entry.get("subDir")), + config_file=_string_or(entry.get("configFile"), "lakefile"), + manifest_file=_string_or(entry.get("manifestFile"), "lake-manifest.json"), + **common, + ) + + +def _manifest_layout(version: object) -> str | None: + """Lake reads manifest versions 5 (0.5.0) up to 2.0.0; those before 7 (0.7.0) use a legacy layout.""" + + if isinstance(version, int) and not isinstance(version, bool): + parts = (0, version, 0) + elif isinstance(version, str) and (match := _MANIFEST_VERSION.fullmatch(version)): + parts = tuple(int(part) for part in match.groups()) + else: + return None + if parts < (0, 5, 0) or parts[0] > 1: + return None + return "legacy" if parts < (0, 7, 0) else "current" + + +def _reject_json_constant(constant: str) -> None: + raise ValueError(f"Lake's JSON parser rejects {constant}") + + +def _is_stale(requirement: dict, locked: MathlibLock) -> bool: + """Whether lakefile.toml asks for a different Mathlib source than the lock records.""" + + if ("path" in requirement) != (locked.type == "path"): + return True + revision = requirement.get("rev") + git = requirement.get("git") + return locked.type == "git" and ( + (isinstance(revision, str) and revision != locked.input_rev) + or (isinstance(git, str) and canonical_git_url(_redact(git)) != canonical_git_url(locked.url)) + ) + + +def _redact(url: str | None) -> str | None: + """Hide credentials embedded in a Git URL, since reports end up in logs.""" + + return None if url is None else _URL_CREDENTIALS.sub(r"\1***@", url) + + +def _read_text(root: Path, relative: str, diagnostics: list[ProjectDiagnostic]) -> str | None: + """Read a small UTF-8 regular file; never opens FIFOs or devices.""" + + path = root / relative + try: + if not path.is_file(): + raise OSError(relative) + with path.open("rb") as handle: + data = handle.read(_MAX_FILE_BYTES + 1) + if len(data) > _MAX_FILE_BYTES: + raise OSError(relative) + return data.decode("utf-8") + except (OSError, UnicodeError): + diagnostics.append( + ProjectDiagnostic( + "error", "unreadable-file", f"{relative} is not a readable UTF-8 file of at most 1 MiB.", relative + ) + ) + return None + + +def _present(path: Path) -> bool: + try: + return path.exists() or path.is_symlink() + except OSError: + return True + + +def _exists_exactly(root: Path, relative: str) -> bool: + """Whether a path exists with exactly this spelling, even on a case-insensitive filesystem. + + A Lean library named `Blueprint` must not be mistaken for the `blueprint` vault. + """ + + directory = root + for part in relative.split("/"): + try: + if part not in os.listdir(directory): + return False + except OSError: + return False + directory = directory / part + return True + + +def _is_name(value: object) -> bool: + return isinstance(value, str) and bool(value) + + +def _are_named_tables(value: object) -> bool: + return isinstance(value, list) and all(isinstance(entry, dict) and _is_name(entry.get("name")) for entry in value) + + +def _string(value: object) -> str | None: + return value if isinstance(value, str) else None + + +def _string_or(value: object, default: str) -> str | None: + """Lake's default for an absent or null field; any other non-string is malformed.""" + + return default if value is None else _string(value) diff --git a/autoform_cli/project/releases.json b/autoform_cli/project/releases.json new file mode 100644 index 00000000..c73e083d --- /dev/null +++ b/autoform_cli/project/releases.json @@ -0,0 +1,13 @@ +{ + "schema": "autoform-project-release-catalog/v1", + "releases": [ + { + "id": "lean-v4.32.2-mathlib-v4.32.2", + "recommended": true, + "lean_toolchain": "leanprover/lean4:v4.32.2", + "mathlib_git": "https://github.com/leanprover-community/mathlib4", + "mathlib_rev": "v4.32.2", + "mathlib_commit": "905b95818eb32af7874a58b427f50c1711a5e96c" + } + ] +} diff --git a/tests/test_plugin_runtime.py b/tests/test_plugin_runtime.py index 9c96b917..ba5ce1f7 100644 --- a/tests/test_plugin_runtime.py +++ b/tests/test_plugin_runtime.py @@ -94,6 +94,7 @@ def test_wheel_contains_only_the_minimal_runtime(repo_root, tmp_path): "autoform_cli/graph.py", "autoform_cli/probes/skeleton_probe.lean", "autoform_cli/visualize.py", + "autoform_cli/project/releases.json", "servers/lean_client.py", "servers/lean_runtime.py", "servers/lsp/server.py", @@ -155,3 +156,48 @@ def test_wheel_contains_only_the_minimal_runtime(repo_root, tmp_path): text=True, ) assert probe.returncode == 0, probe.stderr + + environment = tmp_path / "wheel-venv" + created = subprocess.run( + ["uv", "venv", "--python", sys.executable, str(environment)], + capture_output=True, + text=True, + ) + assert created.returncode == 0, created.stderr + python = environment / ("Scripts/python.exe" if sys.platform == "win32" else "bin/python") + installed = subprocess.run( + ["uv", "pip", "install", "--python", str(python), str(wheel)], + capture_output=True, + text=True, + ) + assert installed.returncode == 0, installed.stderr + command = environment / ("Scripts/autoform.exe" if sys.platform == "win32" else "bin/autoform") + outside = tmp_path / "outside" + project = outside / "project" + project.mkdir(parents=True) + (project / "lakefile.toml").write_text( + 'name = "WheelProject"\n' + '[[require]]\nname = "mathlib"\n' + 'git = "https://github.com/leanprover-community/mathlib4.git"\n' + 'rev = "v4.32.2"\n', + encoding="utf-8", + ) + (project / "lean-toolchain").write_text( + "leanprover/lean4:v4.32.2\n", encoding="utf-8" + ) + versions = subprocess.run( + [str(command), "project", "versions", "--json"], + cwd=outside, + capture_output=True, + text=True, + ) + assert versions.returncode == 0, versions.stderr + assert json.loads(versions.stdout)["schema"] == "autoform-project-release-catalog/v1" + inspection = subprocess.run( + [str(command), "project", "inspect", str(project), "--json"], + cwd=outside, + capture_output=True, + text=True, + ) + assert inspection.returncode == 0, inspection.stderr + assert json.loads(inspection.stdout)["lake"]["name"] == "WheelProject" diff --git a/tests/test_project_inspect.py b/tests/test_project_inspect.py new file mode 100644 index 00000000..f3a9a495 --- /dev/null +++ b/tests/test_project_inspect.py @@ -0,0 +1,584 @@ +from __future__ import annotations + +import json +import os +import sys +from pathlib import Path + +import pytest + +from autoform_cli.__main__ import _human_text, main +from autoform_cli.project import ( + PROJECT_INSPECTION_SCHEMA, + RELEASE_CATALOG_SCHEMA, + ProjectCatalogError, + inspect_project, + load_release_catalog, + parse_release_catalog, +) + +MATHLIB_URL = "https://github.com/leanprover-community/mathlib4" +COMMIT = "905b95818eb32af7874a58b427f50c1711a5e96c" +OTHER_COMMIT = "2" * 40 +LAKEFILE = ( + 'name = "Example"\nversion = "0.1.0"\n\n' + '[[require]]\nname = "mathlib"\nscope = "leanprover-community"\nrev = "v4.32.2"\n\n' + '[[lean_lib]]\nname = "Example"\n\n' + '[[lean_exe]]\nname = "example"\n' +) + + +def _mathlib(rev: str = COMMIT, input_rev: str = "v4.32.2", url: str = MATHLIB_URL, **fields: object) -> dict: + """A Mathlib entry spelled the way Lake 4.32 writes it.""" + + entry = { + "url": url, + "type": "git", + "subDir": None, + "scope": "", + "rev": rev, + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": input_rev, + "inherited": False, + "configFile": "lakefile.lean", + } + return {**entry, **fields} + + +def _write_manifest(root: Path, *packages: dict, version: object = "1.1.0") -> None: + (root / "lake-manifest.json").write_text( + json.dumps({"version": version, "packagesDir": ".lake/packages", "packages": list(packages)}), + encoding="utf-8", + ) + + +def _project( + tmp_path: Path, + *, + lakefile: str | None = LAKEFILE, + toolchain: str | None = "leanprover/lean4:v4.32.2\n", + manifest: tuple[dict, ...] | None = (_mathlib(),), +) -> Path: + root = tmp_path / "project" + root.mkdir() + if lakefile is not None: + (root / "lakefile.toml").write_text(lakefile, encoding="utf-8") + if toolchain is not None: + (root / "lean-toolchain").write_text(toolchain, encoding="utf-8") + if manifest is not None: + _write_manifest(root, *manifest) + return root + + +def _codes(result) -> set[str]: + return {diagnostic.code for diagnostic in result.diagnostics} + + +def test_catalog_pair_from_lakes_math_template_is_supported(tmp_path: Path) -> None: + result = inspect_project(_project(tmp_path)) + + assert result.ok + assert result.compatibility.status == "supported" + assert result.compatibility.release == "lean-v4.32.2-mathlib-v4.32.2" + assert result.lake.name == "Example" + assert [(target.kind, target.name) for target in result.lake.targets] == [ + ("lean_lib", "Example"), + ("lean_exe", "example"), + ] + assert result.lean_toolchain == "leanprover/lean4:v4.32.2" + assert result.mathlib.rev == COMMIT + assert result.diagnostics == () + + +def test_json_report_has_a_stable_shape(tmp_path: Path) -> None: + payload = json.loads(inspect_project(_project(tmp_path)).to_json()) + + assert payload["schema"] == PROJECT_INSPECTION_SCHEMA + assert payload["ok"] is True + assert sorted(payload) == [ + "autoform_paths", + "compatibility", + "diagnostics", + "lake", + "lean_toolchain", + "mathlib", + "ok", + "project_root", + "schema", + ] + assert payload["compatibility"] == { + "recommended_release": "lean-v4.32.2-mathlib-v4.32.2", + "release": "lean-v4.32.2-mathlib-v4.32.2", + "status": "supported", + } + + +@pytest.mark.parametrize("url", [MATHLIB_URL + ".git", MATHLIB_URL + "/"]) +def test_equivalent_mathlib_url_spellings_match(tmp_path: Path, url: str) -> None: + result = inspect_project(_project(tmp_path, manifest=(_mathlib(url=url),))) + + assert result.compatibility.status == "supported" + + +def test_fork_with_the_catalog_commit_is_unlisted(tmp_path: Path) -> None: + fork = _mathlib(url="https://github.com/someone/mathlib4") + result = inspect_project(_project(tmp_path, manifest=(fork,))) + + assert result.compatibility.status == "unlisted" + + +def test_other_toolchain_is_unlisted(tmp_path: Path) -> None: + result = inspect_project(_project(tmp_path, toolchain="leanprover/lean4:v4.33.0\n")) + + assert result.ok + assert result.compatibility.status == "unlisted" + assert "release-unlisted" in _codes(result) + + +def test_manifest_lock_decides_when_the_lakefile_moved_ahead(tmp_path: Path) -> None: + # The lakefile asks for v4.32.2 but the manifest still locks v4.31.0; Lake builds the lock. + old = _mathlib(rev=OTHER_COMMIT, input_rev="v4.31.0") + result = inspect_project(_project(tmp_path, manifest=(old,))) + + assert result.compatibility.status == "unlisted" + assert "lake-manifest-stale" in _codes(result) + + +def test_stale_requirement_still_reports_the_locked_catalog_pair(tmp_path: Path) -> None: + lakefile = LAKEFILE.replace('rev = "v4.32.2"', 'rev = "v4.31.0"') + result = inspect_project(_project(tmp_path, lakefile=lakefile)) + + assert result.compatibility.status == "supported" + assert "lake-manifest-stale" in _codes(result) + + +def test_requirement_git_url_is_compared_with_the_lock(tmp_path: Path) -> None: + lakefile = LAKEFILE.replace('scope = "leanprover-community"', 'git = "https://github.com/someone/mathlib4"') + result = inspect_project(_project(tmp_path, lakefile=lakefile)) + + assert "lake-manifest-stale" in _codes(result) + + +def test_last_duplicate_manifest_entry_wins(tmp_path: Path) -> None: + manifest = (_mathlib(rev=OTHER_COMMIT), _mathlib()) + result = inspect_project(_project(tmp_path, manifest=manifest)) + + assert result.compatibility.status == "supported" + + +def test_transitive_mathlib_still_decides_compatibility(tmp_path: Path) -> None: + inherited = {**_mathlib(), "inherited": True} + lakefile = 'name = "Example"\n\n[[require]]\nname = "loom"\ngit = "https://example.com/loom"\n' + result = inspect_project(_project(tmp_path, lakefile=lakefile, manifest=(inherited,))) + + assert result.compatibility.status == "supported" + + +def test_direct_lock_without_a_requirement_is_unused(tmp_path: Path) -> None: + result = inspect_project(_project(tmp_path, lakefile='name = "Example"\n')) + + assert result.mathlib is None + assert result.compatibility.status == "indeterminate" + assert "mathlib-manifest-unused" in _codes(result) + + +@pytest.mark.parametrize( + "fields", + [{"subDir": "Archive"}, {"configFile": "alternate.lean"}, {"configFile": None}, {"manifestFile": "other.json"}], +) +def test_lock_must_load_mathlib_the_way_releases_do(tmp_path: Path, fields: dict) -> None: + result = inspect_project(_project(tmp_path, manifest=(_mathlib(**fields),))) + + assert result.compatibility.status == "unlisted" + + +def test_uppercase_commit_is_the_same_commit(tmp_path: Path) -> None: + result = inspect_project(_project(tmp_path, manifest=(_mathlib(rev=COMMIT.upper()),))) + + assert result.compatibility.status == "supported" + + +def test_url_credentials_are_redacted_and_never_match(tmp_path: Path, capsys) -> None: + secret = "https://user:hunter2@github.com/leanprover-community/mathlib4" + lakefile = LAKEFILE.replace('scope = "leanprover-community"', f'git = "{secret}"') + root = _project(tmp_path, lakefile=lakefile, manifest=(_mathlib(url=secret),)) + + result = inspect_project(root) + main(["project", "inspect", str(root)]) + + assert result.mathlib.url == "https://***@github.com/leanprover-community/mathlib4" + assert result.compatibility.status == "unlisted" + assert "lake-manifest-stale" not in _codes(result) + assert "hunter2" not in result.to_json() + capsys.readouterr().out + + +def test_escaped_mathlib_spelling_is_the_same_package(tmp_path: Path) -> None: + lakefile = LAKEFILE.replace('name = "mathlib"', 'name = "«mathlib»"') + result = inspect_project(_project(tmp_path, lakefile=lakefile, manifest=(_mathlib(name="«mathlib»"),))) + + assert result.compatibility.status == "supported" + + +def test_path_requirement_with_a_git_lock_is_stale(tmp_path: Path) -> None: + lakefile = LAKEFILE.replace('scope = "leanprover-community"', 'path = "../mathlib4"') + result = inspect_project(_project(tmp_path, lakefile=lakefile)) + + assert "lake-manifest-stale" in _codes(result) + + +def test_project_without_mathlib_is_indeterminate(tmp_path: Path) -> None: + plausible = {**_mathlib(), "name": "plausible"} + result = inspect_project(_project(tmp_path, manifest=(plausible,))) + + assert result.ok + assert result.mathlib is None + assert result.compatibility.status == "indeterminate" + assert "release-indeterminate" in _codes(result) + + +def test_missing_manifest_is_indeterminate(tmp_path: Path) -> None: + result = inspect_project(_project(tmp_path, manifest=None)) + + assert result.ok + assert result.compatibility.status == "indeterminate" + assert {"missing-lake-manifest", "release-indeterminate"} <= _codes(result) + + +@pytest.mark.parametrize( + "content", + [ + "{", + "[]", + '{"packages": []}', + '{"version": "1.1.0", "packages": {}}', + '{"version": "2.0.0", "packages": []}', + '{"version": 4, "packages": []}', + '{"version": "1.1.0", "packages": [], "lakeDir": NaN}', + '{"version": "1.1.0", "packages": [{"name": "mathlib", "type": "zip"}]}', + ], +) +def test_manifests_lake_would_refuse_fail_inspection(tmp_path: Path, content: str) -> None: + root = _project(tmp_path) + (root / "lake-manifest.json").write_text(content, encoding="utf-8") + + result = inspect_project(root) + + assert not result.ok + assert result.compatibility.status == "indeterminate" + assert "invalid-lake-manifest" in _codes(result) + + +@pytest.mark.parametrize("version", [5, 6, "0.6.0"]) +def test_legacy_manifests_are_advisory(tmp_path: Path, version: object) -> None: + root = _project(tmp_path) + _write_manifest(root, _mathlib(), version=version) + + result = inspect_project(root) + + assert result.ok + assert result.compatibility.status == "indeterminate" + assert "unsupported-lake-manifest" in _codes(result) + + +@pytest.mark.parametrize("packages", ['"packages": null', '"packages": []', '"name": "Example"']) +def test_null_or_absent_packages_mean_no_packages(tmp_path: Path, packages: str) -> None: + root = _project(tmp_path) + (root / "lake-manifest.json").write_text(f'{{"version": "1.1.0", {packages}}}', encoding="utf-8") + + result = inspect_project(root) + + assert result.ok + assert result.compatibility.status == "indeterminate" + + +def test_integer_manifest_versions_are_read(tmp_path: Path) -> None: + root = _project(tmp_path) + _write_manifest(root, _mathlib(), version=7) + + assert inspect_project(root).compatibility.status == "supported" + + +def test_package_override_replaces_the_locked_mathlib(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / ".lake").mkdir() + (root / ".lake/package-overrides.json").write_text( + json.dumps( + { + "schemaVersion": "1.1.0", + "packages": [{"name": "mathlib", "type": "path", "dir": "../mathlib4", "inherited": False}], + } + ), + encoding="utf-8", + ) + + result = inspect_project(root) + + assert result.mathlib.type == "path" + assert result.mathlib.source == ".lake/package-overrides.json" + assert result.compatibility.status == "indeterminate" + assert "mathlib-overridden" in _codes(result) + + +def test_override_needs_a_manifest_to_replace(tmp_path: Path) -> None: + root = _project(tmp_path, manifest=None) + (root / ".lake").mkdir() + (root / ".lake/package-overrides.json").write_text( + json.dumps({"schemaVersion": "1.1.0", "packages": [_mathlib()]}), encoding="utf-8" + ) + + assert inspect_project(root).compatibility.status == "indeterminate" + + +def test_override_without_mathlib_leaves_the_manifest_in_charge(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / ".lake").mkdir() + (root / ".lake/package-overrides.json").write_text( + json.dumps({"schemaVersion": "1.1.0", "packages": []}), encoding="utf-8" + ) + + assert inspect_project(root).compatibility.status == "supported" + + +def test_lakefile_lean_cannot_confirm_an_inherited_mathlib(tmp_path: Path) -> None: + root = _project(tmp_path, lakefile=None, manifest=(_mathlib(inherited=True),)) + (root / "lakefile.lean").write_text("import Lake\n", encoding="utf-8") + + result = inspect_project(root) + + assert result.mathlib is None + assert result.compatibility.status == "indeterminate" + + +def test_invalid_override_file_blocks_a_supported_answer(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / ".lake").mkdir() + (root / ".lake/package-overrides.json").write_text("{", encoding="utf-8") + + result = inspect_project(root) + + assert not result.ok + assert result.compatibility.status == "indeterminate" + + +def test_lakefile_lean_takes_precedence_and_is_not_evaluated(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / "lakefile.lean").write_text('#eval IO.println "never run"\n', encoding="utf-8") + + result = inspect_project(root) + + assert result.lake.config == "lakefile.lean" + assert result.lake.name is None + assert result.mathlib is None + assert "lakefile-lean-not-evaluated" in _codes(result) + assert result.compatibility.status == "indeterminate" + + +@pytest.mark.parametrize( + ("toolchain", "ok"), + [ + ("leanprover/lean4:v4.32.2", True), + ("leanprover/lean4:v4.32.2\n\n", True), + ("leanprover/lean4:v4.32.2\r\n", True), + (" leanprover/lean4:v4.32.2\t\n", True), + ("leanprover/lean4:v4.32.2\nleanprover/lean4:v4.31.0\n", True), + ("", False), + ("\nleanprover/lean4:v4.32.2\n", False), + ("leanprover/lean4:v4.32.2 extra\n", False), + ("leanprover/lean4:v4.32.2\x1b\n", False), + ("leanprover/lean4:v4.32.2\x00\n", False), + ("leanprover/lean4:v4.32.2\u009b\n", False), + ], +) +def test_toolchain_follows_elans_first_line_rule(tmp_path: Path, toolchain: str, ok: bool) -> None: + # Checked against elan 4.2.0: it trims the first line and ignores the file when that line is malformed. + result = inspect_project(_project(tmp_path, toolchain=toolchain)) + + assert result.ok is ok + assert (result.lean_toolchain == "leanprover/lean4:v4.32.2") is ok + + +def test_missing_toolchain_and_lakefile_are_errors(tmp_path: Path) -> None: + root = _project(tmp_path, lakefile=None, toolchain=None) + (root / "lakefile.toml").mkdir() # still marks the root, but cannot be read + + result = inspect_project(root) + + assert not result.ok + assert {"missing-lean-toolchain", "unreadable-file"} <= _codes(result) + assert result.compatibility.status == "indeterminate" + + +@pytest.mark.parametrize( + "lakefile", + [ + "name = \n", + 'version = "0.1.0"\n', + 'name = ""\n', + 'name = "E"\nversion = "wat"\n', + 'name = "E"\nrequire = 5\n', + 'name = "E"\n[[lean_lib]]\n', + 'name = "E"\n[[lean_lib]]\nname = "A"\n[[lean_exe]]\nname = "A"\n', + ], +) +def test_lakefiles_lake_refuses_are_errors(tmp_path: Path, lakefile: str) -> None: + # Each case checked against Lake 4.32.0, which refuses to load it. + result = inspect_project(_project(tmp_path, lakefile=lakefile)) + + assert not result.ok + assert "invalid-lakefile-toml" in _codes(result) + + +@pytest.mark.parametrize("lakefile", ['name = "my-project"\n', 'name = "E"\nsrcDir = "../outside"\n']) +def test_lakefiles_lake_accepts_are_fine(tmp_path: Path, lakefile: str) -> None: + assert inspect_project(_project(tmp_path, lakefile=lakefile + LAKEFILE.split("\n\n", 1)[1])).ok + + +def test_oversized_and_non_utf8_files_are_errors(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / "lake-manifest.json").write_bytes(b" " * (1024 * 1024 + 1)) + (root / "lean-toolchain").write_bytes(b"\xff\n") + + result = inspect_project(root) + + assert [diagnostic.path for diagnostic in result.diagnostics if diagnostic.code == "unreadable-file"] == [ + "lake-manifest.json", + "lean-toolchain", + ] + + +@pytest.mark.skipif(not hasattr(os, "mkfifo"), reason="needs FIFOs") +def test_fifo_configuration_is_never_opened(tmp_path: Path) -> None: + root = _project(tmp_path, lakefile=None) + os.mkfifo(root / "lakefile.toml") + + result = inspect_project(root) # would block forever if opened + + assert "unreadable-file" in _codes(result) + + +def test_nearest_root_is_reported_relative_to_the_target(tmp_path: Path) -> None: + root = _project(tmp_path) + nested = root / "Example" / "Algebra" + nested.mkdir(parents=True) + (nested / "Basic.lean").write_text("", encoding="utf-8") + + assert inspect_project(nested).project_root == "../.." + assert inspect_project(nested / "Basic.lean").project_root == "../.." + assert inspect_project(root).project_root == "." + + +def test_nested_package_is_its_own_root(tmp_path: Path) -> None: + root = _project(tmp_path) + package = root / ".lake" / "packages" / "inner" + package.mkdir(parents=True) + (package / "lean-toolchain").write_text("leanprover/lean4:v4.32.2\n", encoding="utf-8") + + result = inspect_project(package) + + assert result.project_root == "." + assert "missing-lake-config" in _codes(result) + + +def test_missing_target_and_no_project_are_errors(tmp_path: Path) -> None: + assert "target-unreadable" in _codes(inspect_project(tmp_path / "absent")) + empty = tmp_path / "empty" + empty.mkdir() + result = inspect_project(empty) + assert not result.ok + assert result.project_root is None + assert "project-not-found" in _codes(result) + + +@pytest.mark.skipif(sys.platform == "win32", reason="symlinks need privileges on Windows") +def test_projects_behind_symlinked_directories_are_inspected(tmp_path: Path) -> None: + _project(tmp_path) + link = tmp_path / "link" + link.symlink_to(tmp_path, target_is_directory=True) + + result = inspect_project(link / "project") + + assert result.ok + assert result.compatibility.status == "supported" + + +def test_autoform_paths_need_their_exact_spelling(tmp_path: Path) -> None: + root = _project(tmp_path) + (root / "Blueprint").mkdir() # a Lean library, not the vault + (root / "mkdocs.yml").write_text("", encoding="utf-8") + + assert inspect_project(root).autoform_paths == ("mkdocs.yml",) + + (root / "Blueprint").rename(root / "blueprint") + assert inspect_project(root).autoform_paths == ("blueprint", "mkdocs.yml") + + (root / "blueprint").rmdir() + (root / "blueprint").write_text("", encoding="utf-8") + assert inspect_project(root).autoform_paths == ("mkdocs.yml",) + + +def test_bundled_catalog_lists_the_recommended_release() -> None: + catalog = load_release_catalog() + + assert catalog.recommended.id == "lean-v4.32.2-mathlib-v4.32.2" + assert catalog.recommended.mathlib_commit == COMMIT + assert json.loads(catalog.to_json())["schema"] == RELEASE_CATALOG_SCHEMA + + +def _release(**changes: object) -> dict: + release = { + "id": "a", + "recommended": True, + "lean_toolchain": "leanprover/lean4:v4.32.2", + "mathlib_git": MATHLIB_URL, + "mathlib_rev": "v4.32.2", + "mathlib_commit": COMMIT, + } + return {**release, **changes} + + +@pytest.mark.parametrize( + "payload", + [ + [], + {"schema": "other", "releases": [_release()]}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": []}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": [_release(extra=1)]}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": [_release(mathlib_commit="v4.32.2")]}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": [_release(recommended="yes")]}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": [_release(), _release(id="b", recommended=False)]}, + {"schema": RELEASE_CATALOG_SCHEMA, "releases": [_release(recommended=False)]}, + ], +) +def test_malformed_catalogs_are_rejected(payload: object) -> None: + with pytest.raises(ProjectCatalogError): + parse_release_catalog(payload) + + +def test_cli_reports_and_exit_codes(tmp_path: Path, capsys) -> None: + root = _project(tmp_path) + + assert main(["project", "inspect", str(root)]) == 0 + captured = capsys.readouterr() + assert "Compatibility: supported (lean-v4.32.2-mathlib-v4.32.2)" in captured.out + assert "lean_lib Example" in captured.out + + assert main(["project", "inspect", str(root), "--json"]) == 0 + assert json.loads(capsys.readouterr().out)["ok"] is True + + assert main(["project", "versions"]) == 0 + assert "lean-v4.32.2-mathlib-v4.32.2 [recommended]" in capsys.readouterr().out + + (root / "lean-toolchain").unlink() + assert main(["project", "inspect", str(root)]) == 1 + assert "error[missing-lean-toolchain]" in capsys.readouterr().err + + +def test_human_report_escapes_characters_that_could_forge_lines(tmp_path: Path, capsys) -> None: + lakefile = LAKEFILE.replace('name = "Example"', 'name = "Ex\\u202eample\\u009b\\n"') + root = _project(tmp_path, lakefile=lakefile) + + assert main(["project", "inspect", str(root)]) == 0 + + assert "Lake: Ex\\u202eample\\x9b\\n 0.1.0 (lakefile.toml)" in capsys.readouterr().out + assert _human_text("\U000e0001") == "\\U000e0001"