Fill every probe's records-file contract in one lean_probe helper

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,16 +683,15 @@ 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,
         check_inventory="false" if artifact_dir is None else "true",
         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)))),
     )

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/<name>`` 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",

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),
     )
 

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

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,

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

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
 # --------------------------------------------------------------------------- #