diff --git a/docs/flavour-text-audit.md b/docs/flavour-text-audit.md deleted file mode 100644 index 33f3babe..00000000 --- a/docs/flavour-text-audit.md +++ /dev/null @@ -1,32 +0,0 @@ -# Flavour-text audit inventory - -The lifecycle-overhaul plan reserves the final prose and provenance review for -humans. The inventory tool makes that review finite and reproducible without -generating, repairing, or semantically judging any text. It does not establish -that existing prose was human-authored. - -Run: - -```console -python scripts/flavour_text_inventory.py \ - --json-output /tmp/lean-eval-flavour-text.json \ - --markdown-output /tmp/lean-eval-flavour-text.md -``` - -The output paths must not already exist. The tool writes the pair fail-closed: -it never knowingly leaves only one output behind. - -The JSON report records, for every problem manifest, whether `notes`, `source`, -and `informal_solution` are present, their exact character and UTF-8 byte -counts, and SHA-256 digests of their exact TOML string values. The Markdown -rendering is a compact human work queue. A present field is not an approval: -every entry remains unreviewed until a human checks that it contains an -accurate informal statement, suitable citations and literature context, and -useful solving guidance whose authorship satisfies the no-LLM policy. Agents -must not generate, repair, or semantically approve hints. - -Reports are generated artifacts and are not committed. The eventual human -audit record should contain the reviewer identity, review date, repository -commit, exact per-field digests, an `approved` or `needs-edit` outcome, and an -explicit provenance attestation. That makes later prose changes visible without -treating this inventory as a quality gate. diff --git a/scripts/flavour_text_inventory.py b/scripts/flavour_text_inventory.py deleted file mode 100644 index 9523e868..00000000 --- a/scripts/flavour_text_inventory.py +++ /dev/null @@ -1,203 +0,0 @@ -#!/usr/bin/env python3 -"""Inventory LeanEval problem prose awaiting human provenance and quality review.""" - -from __future__ import annotations - -import argparse -import hashlib -import json -import os -import pathlib -import tempfile -from collections.abc import Mapping -from typing import Any - -from validate_catalog import CatalogError, load_problems, load_tag_registry - - -class InventoryError(ValueError): - """The manifest corpus cannot produce a trustworthy inventory.""" - - -PROSE_FIELDS = ("notes", "source", "informal_solution") - - -def _field_evidence(value: object) -> dict[str, Any]: - if value is None: - return { - "specified": False, - "present": False, - "character_count": 0, - "utf8_byte_count": 0, - "sha256": None, - } - assert isinstance(value, str) - encoded = value.encode("utf-8") - return { - "specified": True, - "present": bool(value.strip()), - "character_count": len(value), - "utf8_byte_count": len(encoded), - "sha256": hashlib.sha256(encoded).hexdigest(), - } - - -def load_inventory(root: pathlib.Path) -> dict[str, Any]: - manifest_dir = root / "manifests" / "problems" - if not manifest_dir.is_dir() or manifest_dir.is_symlink(): - raise InventoryError("manifests/problems must be one real directory") - - entries = sorted(manifest_dir.iterdir(), key=lambda path: path.name) - for path in entries: - if path.suffix != ".toml" or not path.is_file() or path.is_symlink(): - raise InventoryError( - f"{path}: manifests/problems may contain only regular TOML files" - ) - try: - registry = load_tag_registry(root) - problems, _revisions = load_problems(root, registry) - except CatalogError as error: - raise InventoryError(f"catalog validation failed: {error}") from error - - rows: list[dict[str, Any]] = [] - for problem_id, data in sorted(problems.items()): - path = manifest_dir / f"{problem_id}.toml" - module = data.get("module") - if not isinstance(module, str) or not module: - raise InventoryError(f"{path}: module must be a non-empty string") - for name in PROSE_FIELDS: - if name in data and not isinstance(data[name], str): - raise InventoryError(f"{path}: {name} must be a string when present") - - fields = {name: _field_evidence(data.get(name)) for name in PROSE_FIELDS} - rows.append( - { - "problem_id": problem_id, - "title": data["title"], - "module": module, - "group": data["group"], - "status": data["status"], - "visible": data.get("visible"), - "prose": fields, - "all_fields_present": all(field["present"] for field in fields.values()), - } - ) - - if not rows: - raise InventoryError("manifest corpus is empty") - - present_counts = { - name: sum(row["prose"][name]["present"] for row in rows) - for name in PROSE_FIELDS - } - return { - "schema_version": 1, - "scope": "inventory-only; every entry still requires human review", - "problem_count": len(rows), - "all_fields_present_count": sum(row["all_fields_present"] for row in rows), - "present_counts": present_counts, - "problems": rows, - } - - -def render_markdown(report: Mapping[str, Any]) -> str: - def cell(value: object) -> str: - return str(value).replace("|", "\\|").replace("\r", " ").replace("\n", " ") - - counts = report["present_counts"] - lines = [ - "# LeanEval flavour-text inventory", - "", - "This is an objective presence-and-digest inventory, not a semantic review.", - "Every entry remains pending human review; no prose is generated by this tool.", - "", - f"- Problems: {report['problem_count']}", - f"- All three prose fields present: {report['all_fields_present_count']}", - f"- Informal statement/notes present: {counts['notes']}", - f"- Citation/source present: {counts['source']}", - f"- Informal solution/hint present: {counts['informal_solution']}", - "", - "| Problem | Group | Status | Notes | Source | Hint |", - "|---|---|---|---:|---:|---:|", - ] - for row in report["problems"]: - fields = row["prose"] - - def marker(name: str) -> str: - field = fields[name] - return str(field["character_count"]) if field["present"] else "missing" - - lines.append( - f"| `{cell(row['problem_id'])}` — {cell(row['title'])} | " - f"{cell(row['group'])} | {cell(row['status'])} | " - f"{marker('notes')} | {marker('source')} | {marker('informal_solution')} |" - ) - return "\n".join(lines) + "\n" - - -def write_outputs( - json_output: pathlib.Path, - json_bytes: bytes, - markdown_output: pathlib.Path, - markdown_bytes: bytes, -) -> None: - outputs = ((json_output, json_bytes), (markdown_output, markdown_bytes)) - normalized = [path.absolute() for path, _contents in outputs] - if normalized[0] == normalized[1]: - raise InventoryError("JSON and Markdown outputs must be distinct paths") - for path in normalized: - if path.exists() or path.is_symlink(): - raise InventoryError(f"refusing to overwrite output {path}") - if not path.parent.is_dir() or path.parent.is_symlink(): - raise InventoryError(f"output parent must be one real directory: {path.parent}") - - temporary_paths: list[pathlib.Path] = [] - installed_paths: list[pathlib.Path] = [] - try: - for path, contents in zip(normalized, (json_bytes, markdown_bytes), strict=True): - with tempfile.NamedTemporaryFile(dir=path.parent, delete=False) as stream: - stream.write(contents) - stream.flush() - os.fsync(stream.fileno()) - temporary_paths.append(pathlib.Path(stream.name)) - for temporary, path in zip(temporary_paths, normalized, strict=True): - os.link(temporary, path) - installed_paths.append(path) - except OSError as error: - for path in installed_paths: - path.unlink(missing_ok=True) - raise InventoryError(f"cannot install complete output pair: {error}") from error - finally: - for path in temporary_paths: - path.unlink(missing_ok=True) - - -def main() -> int: - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("--root", type=pathlib.Path, default=pathlib.Path(".")) - parser.add_argument("--json-output", type=pathlib.Path, required=True) - parser.add_argument("--markdown-output", type=pathlib.Path, required=True) - args = parser.parse_args() - try: - report = load_inventory(args.root.resolve()) - json_bytes = ( - json.dumps(report, indent=2, ensure_ascii=False, sort_keys=True) + "\n" - ).encode("utf-8") - markdown_bytes = render_markdown(report).encode("utf-8") - write_outputs( - args.json_output, - json_bytes, - args.markdown_output, - markdown_bytes, - ) - except InventoryError as error: - parser.exit(1, f"flavour-text inventory failed: {error}\n") - print( - f"Inventoried {report['problem_count']} problems; " - f"{report['all_fields_present_count']} have all three prose fields." - ) - return 0 - - -if __name__ == "__main__": - raise SystemExit(main()) diff --git a/tests/python/test_flavour_text_inventory.py b/tests/python/test_flavour_text_inventory.py deleted file mode 100644 index 3da0f5c8..00000000 --- a/tests/python/test_flavour_text_inventory.py +++ /dev/null @@ -1,196 +0,0 @@ -from __future__ import annotations - -import importlib.util -import json -import pathlib -import sys -import tempfile -import textwrap -import unittest -from unittest import mock - -ROOT = pathlib.Path(__file__).resolve().parents[2] -sys.path.insert(0, str(ROOT / "scripts")) -SPEC = importlib.util.spec_from_file_location( - "flavour_text_inventory", ROOT / "scripts" / "flavour_text_inventory.py" -) -assert SPEC is not None and SPEC.loader is not None -INVENTORY = importlib.util.module_from_spec(SPEC) -sys.modules[SPEC.name] = INVENTORY -SPEC.loader.exec_module(INVENTORY) - - -class FlavourTextInventoryTest(unittest.TestCase): - def _root(self, directory: str) -> pathlib.Path: - root = pathlib.Path(directory) - (root / "manifests" / "problems").mkdir(parents=True) - (root / "manifests" / "tags.toml").write_text( - "schema_version = 1\n\n[tags]\n", encoding="utf-8" - ) - return root - - def test_inventory_is_sorted_and_binds_exact_present_prose(self): - with tempfile.TemporaryDirectory() as directory: - root = self._root(directory) - for problem_id, notes in (("beta", None), ("alpha", " Informal statement. ")): - optional = f'notes = "{notes}"\n' if notes is not None else "" - (root / "manifests" / "problems" / f"{problem_id}.toml").write_text( - textwrap.dedent( - f'''\ - id = "{problem_id}" - title = "{problem_id.title()}" - module = "LeanEval.{problem_id.title()}" - group = "formalization-evaluation" - status = "draft" - visible = true - statement_revision = 1 - tags = [] - {optional}source = "Citation" - informal_solution = "Proof hint" - ''' - ), - encoding="utf-8", - ) - - report = INVENTORY.load_inventory(root) - self.assertEqual( - [row["problem_id"] for row in report["problems"]], ["alpha", "beta"] - ) - self.assertEqual(report["present_counts"]["notes"], 1) - self.assertEqual(report["all_fields_present_count"], 1) - alpha = report["problems"][0] - self.assertEqual(alpha["prose"]["notes"]["character_count"], 21) - self.assertEqual(alpha["prose"]["notes"]["utf8_byte_count"], 21) - self.assertRegex(alpha["prose"]["notes"]["sha256"], r"^[0-9a-f]{64}$") - self.assertEqual( - INVENTORY.render_markdown(report), INVENTORY.render_markdown(report) - ) - - def test_empty_optional_text_is_missing(self): - evidence = INVENTORY._field_evidence(" ") - self.assertTrue(evidence["specified"]) - self.assertFalse(evidence["present"]) - self.assertEqual(evidence["character_count"], 2) - self.assertRegex(evidence["sha256"], r"^[0-9a-f]{64}$") - - def test_exact_digest_changes_with_boundary_whitespace(self): - plain = INVENTORY._field_evidence("hint") - padded = INVENTORY._field_evidence(" hint ") - self.assertNotEqual(plain["sha256"], padded["sha256"]) - self.assertNotEqual(plain["utf8_byte_count"], padded["utf8_byte_count"]) - - def test_filename_mismatch_fails_closed(self): - with tempfile.TemporaryDirectory() as directory: - root = self._root(directory) - (root / "manifests" / "problems" / "wrong.toml").write_text( - textwrap.dedent( - '''\ - id = "actual" - title = "Actual" - module = "LeanEval.Actual" - group = "formalization-evaluation" - status = "draft" - visible = true - statement_revision = 1 - tags = [] - ''' - ), - encoding="utf-8", - ) - with self.assertRaisesRegex(INVENTORY.InventoryError, "match the filename"): - INVENTORY.load_inventory(root) - - def test_catalog_validator_rejects_unknown_enums(self): - with tempfile.TemporaryDirectory() as directory: - root = self._root(directory) - (root / "manifests" / "problems" / "alpha.toml").write_text( - textwrap.dedent( - '''\ - id = "alpha" - title = "Alpha" - module = "LeanEval.Alpha" - group = "made-up" - status = "draft" - visible = true - statement_revision = 1 - tags = [] - ''' - ), - encoding="utf-8", - ) - with self.assertRaisesRegex(INVENTORY.InventoryError, "unknown group"): - INVENTORY.load_inventory(root) - - def test_emitted_module_must_be_a_non_empty_string(self): - for label, module_line in (("missing", ""), ("integer", "module = 3\n"), - ("empty", 'module = ""\n')): - with self.subTest(label=label), tempfile.TemporaryDirectory() as directory: - root = self._root(directory) - (root / "manifests" / "problems" / "alpha.toml").write_text( - textwrap.dedent( - f'''\ - id = "alpha" - title = "Alpha" - {module_line}group = "formalization-evaluation" - status = "draft" - visible = true - statement_revision = 1 - tags = [] - ''' - ), - encoding="utf-8", - ) - with self.assertRaisesRegex(INVENTORY.InventoryError, "module must"): - INVENTORY.load_inventory(root) - - def test_unexpected_directory_entry_fails_closed(self): - with tempfile.TemporaryDirectory() as directory: - root = self._root(directory) - (root / "manifests" / "problems" / "README.txt").write_text( - "ignored?", encoding="utf-8" - ) - with self.assertRaisesRegex(INVENTORY.InventoryError, "only regular TOML"): - INVENTORY.load_inventory(root) - - def test_output_pair_is_distinct_exclusive_and_complete(self): - with tempfile.TemporaryDirectory() as directory: - root = pathlib.Path(directory) - json_path = root / "report.json" - markdown_path = root / "report.md" - with self.assertRaisesRegex(INVENTORY.InventoryError, "distinct"): - INVENTORY.write_outputs(json_path, b"{}\n", json_path, b"# Report\n") - - json_path.write_text("existing", encoding="utf-8") - with self.assertRaisesRegex(INVENTORY.InventoryError, "refusing to overwrite"): - INVENTORY.write_outputs( - json_path, b"{}\n", markdown_path, b"# Report\n" - ) - self.assertFalse(markdown_path.exists()) - - json_path.unlink() - INVENTORY.write_outputs(json_path, b"{}\n", markdown_path, b"# Report\n") - self.assertEqual(json.loads(json_path.read_text(encoding="utf-8")), {}) - self.assertEqual(markdown_path.read_text(encoding="utf-8"), "# Report\n") - - def test_second_output_failure_rolls_back_first_and_temporary_files(self): - with tempfile.TemporaryDirectory() as directory: - root = pathlib.Path(directory) - json_path = root / "rollback.json" - markdown_path = root / "rollback.md" - real_link = INVENTORY.os.link - - def fail_second_link(source: object, destination: object) -> None: - if pathlib.Path(destination) == markdown_path: - raise OSError("synthetic second-link failure") - real_link(source, destination) - - with mock.patch.object(INVENTORY.os, "link", side_effect=fail_second_link): - with self.assertRaisesRegex(INVENTORY.InventoryError, "complete output pair"): - INVENTORY.write_outputs( - json_path, b"{}\n", markdown_path, b"# Report\n" - ) - self.assertEqual(list(root.iterdir()), []) - - -if __name__ == "__main__": - unittest.main()