From 0e1b8122ebc263a7e116863ec9d0c3421cae2193 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Thu, 29 Oct 2026 21:54:45 -0400 Subject: [PATCH] Fill every probe's records-file contract in one lean_probe helper The skeleton, impact and library index probes each loaded their template from probes/ and filled `output_env` and `output_limit` by hand. Those two fields are the probe's half of the records-file contract that run_probe and _read_probe_records hold on the Python side, so three copies could drift apart. lean_probe.render_probe_template(name, **fields) now loads `probes/` and adds both fields. It reads PROBE_OUTPUT_ENV and DEFAULT_PROBE_OUTPUT_LIMIT when called, not as default arguments, so tests that patch the limit still reach the rendered program. It replaces _probe_template and impact's _impact_template, and generate.py's inline load. The template header comments now name the helper; they spell the field names without braces, since the templates are format strings. The new test renders all three probes with the limit patched to 1234 and checks each reads the records-file variable and declares the patched limit. Rendered output is unchanged apart from the header comments. --- autoform_cli/impact.py | 11 ++--------- autoform_cli/lean_probe.py | 20 ++++++++++++++------ autoform_cli/library/generate.py | 6 ++---- autoform_cli/probes/impact_probe.lean | 4 +++- autoform_cli/probes/library_probe.lean | 4 +++- autoform_cli/probes/skeleton_probe.lean | 4 +++- tests/test_lean_probe.py | 18 ++++++++++++++++++ 7 files changed, 45 insertions(+), 22 deletions(-) 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 # --------------------------------------------------------------------------- #