diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py index 94860398c..e021c61f5 100644 --- a/autoform_cli/impact.py +++ b/autoform_cli/impact.py @@ -656,12 +656,6 @@ def _glob(glob: str, library: LeanLibrary) -> tuple[str, str]: return base, mode -def _impact_template() -> str: - """The Lean impact probe source, kept under probes/ beside this module.""" - - return (Path(__file__).parent / "probes" / "impact_probe.lean").read_text(encoding="utf-8") - - def render_impact_probe( *, imports: Iterable[str], @@ -689,7 +683,8 @@ def render_impact_probe( walks = [ [str(directory), list(lean_name_components(base)), glob] for directory, base, glob in glob_directories ] - return _impact_template().format( + return lean_probe.render_probe_template( + "impact_probe.lean", imports="\n".join(f"import {module}" for module in modules), marker=IMPACT_MARKER, module_marker=IMPACT_MODULE_MARKER, @@ -697,8 +692,6 @@ def render_impact_probe( emit_module_evidence="true" if emit_module_evidence else "false", artifact_dir=json.dumps(str(artifact_dir or ""), ensure_ascii=False), glob_directories=json.dumps(json.dumps(walks, ensure_ascii=False), ensure_ascii=False), - output_env=lean_probe.PROBE_OUTPUT_ENV, - output_limit=lean_probe.DEFAULT_PROBE_OUTPUT_LIMIT, project_modules=lean_requests(tuple(sorted(set(project_modules)))), selected_modules=lean_requests(tuple(sorted(set(selected_modules)))), ) diff --git a/autoform_cli/lean_probe.py b/autoform_cli/lean_probe.py index 9f3cc6545..992f84082 100644 --- a/autoform_cli/lean_probe.py +++ b/autoform_cli/lean_probe.py @@ -830,21 +830,28 @@ def _stable_detail(text: str, lean_root: Path, *scratch: Path) -> str: # The probe # --------------------------------------------------------------------------- # -def _probe_template() -> str: - """The probe's Lean helpers, kept under probes/ beside this module.""" +def render_probe_template(name: str, **fields: object) -> str: + """Fill the probe template ``probes/`` with ``fields`` and the records-file contract. + + Every probe writes its records to the file ``PROBE_OUTPUT_ENV`` names, which + ``run_probe`` sets, and stops before its records pass + ``DEFAULT_PROBE_OUTPUT_LIMIT`` bytes, which ``_read_probe_records`` + enforces; ``output_env`` and ``output_limit`` give the template both. Read + at call time, so a patched limit applies. + """ - return (Path(__file__).parent / "probes" / "skeleton_probe.lean").read_text(encoding="utf-8") + template = (Path(__file__).parent / "probes" / name).read_text(encoding="utf-8") + return template.format(**fields, output_env=PROBE_OUTPUT_ENV, output_limit=DEFAULT_PROBE_OUTPUT_LIMIT) def _render_probe_helper() -> str: """Render the helper module every probe imports; see ``_build_probe_helper``.""" - return _probe_template().format( + return render_probe_template( + "skeleton_probe.lean", core_roots=", ".join(_lean_name(name) for name in _CORE_MODULE_ROOTS), error_limit=_FAILURE_DETAIL_LIMIT, marker=PROBE_MARKER, - output_env=PROBE_OUTPUT_ENV, - output_limit=DEFAULT_PROBE_OUTPUT_LIMIT, ) @@ -1298,6 +1305,7 @@ def run(module: str) -> _T: "project_control_snapshot", "read_snapshot_file", "render_probe", + "render_probe_template", "run_module_probes", "run_probe", "stable_paths", diff --git a/autoform_cli/library/generate.py b/autoform_cli/library/generate.py index abab59cf6..bc11afaac 100644 --- a/autoform_cli/library/generate.py +++ b/autoform_cli/library/generate.py @@ -132,12 +132,10 @@ def render_library_probe(modules: Sequence[str]) -> str: names = sorted(set(modules)) if not names: raise GenerateError("the indexed libraries hold no Lean module") - template = (Path(__file__).parent.parent / "probes" / "library_probe.lean").read_text(encoding="utf-8") - return template.format( + return lean_probe.render_probe_template( + "library_probe.lean", imports="\n".join(f"import {module}" for module in names), marker=LIBRARY_MARKER, - output_env=lean_probe.PROBE_OUTPUT_ENV, - output_limit=lean_probe.DEFAULT_PROBE_OUTPUT_LIMIT, modules=_module_set(names), ) diff --git a/autoform_cli/probes/impact_probe.lean b/autoform_cli/probes/impact_probe.lean index 6d5db20f7..ad350617e 100644 --- a/autoform_cli/probes/impact_probe.lean +++ b/autoform_cli/probes/impact_probe.lean @@ -1,6 +1,8 @@ {imports} -- Autoform impact probe. This file is a Python-format template: `{{`/`}}` are --- literal braces and single-brace fields are filled by autoform_cli.impact. +-- literal braces and single-brace fields are filled by autoform_cli.impact +-- through lean_probe.render_probe_template, which adds `output_env` and +-- `output_limit`: the variable naming the records file, and its byte cap. -- It is written to a temporary file and run with `lake env lean` inside the -- built project; it never modifies the project. import Lean.Linter.Deprecated diff --git a/autoform_cli/probes/library_probe.lean b/autoform_cli/probes/library_probe.lean index 082984df4..f148b1101 100644 --- a/autoform_cli/probes/library_probe.lean +++ b/autoform_cli/probes/library_probe.lean @@ -1,6 +1,8 @@ {imports} -- Autoform library index probe. This file is a Python-format template: `{{`/`}}` are --- literal braces and single-brace fields are filled by autoform_cli.library.generate. +-- literal braces and single-brace fields are filled by autoform_cli.library.generate +-- through lean_probe.render_probe_template, which adds `output_env` and +-- `output_limit`: the variable naming the records file, and its byte cap. -- It is written to a temporary file and run with `lake env lean` inside the built -- library; it never modifies the library. It is deliberately not a module file: only -- a plain importer sees module and non-module files together, private placeholders, diff --git a/autoform_cli/probes/skeleton_probe.lean b/autoform_cli/probes/skeleton_probe.lean index b988aaf18..68d69d8fe 100644 --- a/autoform_cli/probes/skeleton_probe.lean +++ b/autoform_cli/probes/skeleton_probe.lean @@ -1,5 +1,7 @@ -- Autoform skeleton probe helpers. This file is a Python-format template: `{{`/`}}` --- are literal braces and single-brace fields are filled by autoform_cli.lean_probe. +-- are literal braces and single-brace fields are filled by +-- lean_probe.render_probe_template, which adds `output_env` and +-- `output_limit`: the variable naming the records file, and its byte cap. -- Autoform compiles it with `lake env lean -o` into a module outside the project, -- which it never modifies. Each probe imports one root module and this module and -- only calls `AutoformSkeleton.main`, so no project name, notation, or option is diff --git a/tests/test_lean_probe.py b/tests/test_lean_probe.py index 49e86f26a..3681d6f4c 100644 --- a/tests/test_lean_probe.py +++ b/tests/test_lean_probe.py @@ -18,6 +18,7 @@ import psutil import pytest +from autoform_cli.impact import render_impact_probe from autoform_cli.lean_probe import ( PROBE_MARKER, PROBE_OUTPUT_ENV, @@ -45,6 +46,7 @@ stale_build_said, _terminate_process_tree, ) +from autoform_cli.library.generate import render_library_probe from tests.conftest import _SKELETON_FIXTURE, _lean_toolchain_available from tests.test_skeleton import _assert_no_survivors, _build, _pid_is_live, _project, _requested, _signal_driver @@ -880,6 +882,22 @@ def test_probe_requires_an_existing_lake_manifest(tmp_path: Path, monkeypatch) - run_probe(probe, tmp_path) +@pytest.mark.parametrize( + "render", + [ + lambda: _render_probe_helper(), + lambda: render_impact_probe(imports=["Demo"], project_modules=["Demo"]), + lambda: render_library_probe(("Lib.A",)), + ], + ids=["skeleton", "impact", "library"], +) +def test_every_probe_template_gets_the_records_file_contract(render, monkeypatch) -> None: + monkeypatch.setattr("autoform_cli.lean_probe.DEFAULT_PROBE_OUTPUT_LIMIT", 1234) + source = render() + assert f'IO.getEnv "{PROBE_OUTPUT_ENV}"' in source + assert "def probeOutputLimit : Nat := 1234" in source + + # --------------------------------------------------------------------------- # # Project layout # --------------------------------------------------------------------------- #