diff --git a/.github/actions/build-lean-eval-generator/action.yml b/.github/actions/build-lean-eval-generator/action.yml new file mode 100644 index 0000000000..e023027333 --- /dev/null +++ b/.github/actions/build-lean-eval-generator/action.yml @@ -0,0 +1,40 @@ +# Copyright 2026 The Formal Conjectures Authors. + +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at + +# https://www.apache.org/licenses/LICENSE-2.0 + +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: Build the pinned lean-eval-generator +description: >- + Clone and build leanprover/lean-eval-generator at the revision + comparator/tools.toml pins under [generator], and export + LEAN_EVAL_GENERATOR_BIN. The package depends on nothing, so this is a + small Lean build, not a Mathlib one. Requires elan on PATH and a + checked-out Formal Conjectures tree. + +runs: + using: composite + steps: + - name: Clone and build the pinned revision + shell: bash + run: | + read -r GEN_REPO GEN_REV <<< "$(python3 - <<'PY' + import tomllib + + with open("comparator/tools.toml", "rb") as handle: + generator = tomllib.load(handle)["generator"] + print(generator["repository"], generator["rev"]) + PY + )" + git clone "$GEN_REPO" "$RUNNER_TEMP/lean-eval-generator" + git -C "$RUNNER_TEMP/lean-eval-generator" checkout "$GEN_REV" + (cd "$RUNNER_TEMP/lean-eval-generator" && lake build) + echo "LEAN_EVAL_GENERATOR_BIN=$RUNNER_TEMP/lean-eval-generator/.lake/build/bin/lean-eval-generator" >> "$GITHUB_ENV" diff --git a/.github/actions/install-elan/action.yml b/.github/actions/install-elan/action.yml new file mode 100644 index 0000000000..8483728b4c --- /dev/null +++ b/.github/actions/install-elan/action.yml @@ -0,0 +1,31 @@ +# Copyright 2026 The Formal Conjectures Authors. + +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at + +# https://www.apache.org/licenses/LICENSE-2.0 + +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: Install elan +description: >- + Install elan and put it on PATH, with no default toolchain: every job here + builds in a checkout whose `lean-toolchain` decides the version. The elan + release is pinned in one place so two jobs cannot install two different + installers. + +runs: + using: composite + steps: + - name: Install elan + shell: bash + run: | + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" diff --git a/.github/actions/prepare-extractor/action.yml b/.github/actions/prepare-extractor/action.yml new file mode 100644 index 0000000000..1484d29e4a --- /dev/null +++ b/.github/actions/prepare-extractor/action.yml @@ -0,0 +1,44 @@ +# Copyright 2026 The Formal Conjectures Authors. + +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at + +# https://www.apache.org/licenses/LICENSE-2.0 + +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: Prepare the comparator extractor +description: >- + Install elan at this repository's toolchain, restore the Mathlib cache, + build the comparator_facts extractor together with the source modules a + job needs elaborated, and run the extractor's self-test. The facts the + importer reads (ranges, binder boundaries, answer-slot types, category + tags) come from an elaborated environment, so every module a job imports + from has to be built first. + +inputs: + modules: + description: Space-separated Lake targets to build beside the extractor. + required: false + default: "" + +runs: + using: composite + steps: + - name: Install elan + uses: ./.github/actions/install-elan + + - name: Build the extractor and the source modules + shell: bash + env: + MODULES: ${{ inputs.modules }} + run: | + lake exe cache get + # shellcheck disable=SC2086 + lake build comparator_facts $MODULES + lake exe comparator_facts --self-test diff --git a/.github/workflows/build-and-docs.yml b/.github/workflows/build-and-docs.yml index c3b96176e6..63f7dea6d8 100644 --- a/.github/workflows/build-and-docs.yml +++ b/.github/workflows/build-and-docs.yml @@ -51,7 +51,9 @@ jobs: python-version: '3.12.9' - name: Run script tests - run: python3 -m unittest discover -s scripts -p 'test_*.py' -v + run: | + python3 -m unittest discover -s scripts -p 'test_*.py' -v + python3 -m unittest discover -s comparator/adapter -p 'test_*.py' -v build: runs-on: ubuntu-latest @@ -111,11 +113,7 @@ jobs: - name: Install elan if: steps.mode.outputs.website_only != 'true' - run: | - set -o pipefail - curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz - ./elan-init -y --default-toolchain none - echo "$HOME/.elan/bin" >> $GITHUB_PATH + uses: ./.github/actions/install-elan - name: Restore ~/.cache/mathlib if: steps.mode.outputs.website_only != 'true' diff --git a/.github/workflows/comparator-lean-4-33.yml b/.github/workflows/comparator-lean-4-33.yml new file mode 100644 index 0000000000..1d47a044b5 --- /dev/null +++ b/.github/workflows/comparator-lean-4-33.yml @@ -0,0 +1,303 @@ +# Copyright 2026 The Formal Conjectures Authors. + +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at + +# https://www.apache.org/licenses/LICENSE-2.0 + +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: Generated workspace at LeanEval pins + +# Everything that crosses the adapter's boundaries, in one job: +# +# 1. the elaborator to the importer, over a smoke set that covers each +# defect class the whole-set audit found; +# 2. the importer to the generator, by feeding the emitted request bytes +# back through the pinned binary and comparing the file map; +# 3. the generated workspace to Comparator, built at LeanEval's pins. +# +# Nothing here is checked in. A workspace that lives in the tree is a copy of +# generator output that drifts from the generator and says nothing about the +# importer, because a human wrote it; this job says the importer, the +# generator and Comparator work together, which is what +# `leanprover/lean-eval#536` needs before FC opens problem pull requests. +# +# These checks live here rather than beside the corpus build because they are +# about the adapter, not the corpus. A pull request that only edits a +# statement should not pay for them, and could not pass them: `pins()` refuses +# a source file that differs from the merge base, which is exactly what such a +# pull request changes. +# +# The two toolchains in this job are the point, not an accident. The importer +# reads the declaration's source range, binders and `answer(sorry)` slot types +# from an environment elaborated at this repository's Lean 4.33.1; the workspace +# is built and checked at LeanEval's Lean 4.33. If those two disagree about a +# statement or a slot type, this job is where it shows. + +# Two Mathlib builds make this the most expensive job in the repository, so a +# new push supersedes the run it replaces rather than queueing behind it. +concurrency: + group: comparator-lean-4-33-${{ github.ref }} + cancel-in-progress: true + +on: + pull_request: + # Not the imported statement's source file: `pins()` refuses to generate + # from a file that differs from the merge-base with upstream main, so a + # pull request editing it could never pass this job; the whole-set audit + # covers statement drift once the edit lands. + paths: + - 'comparator/**' + - '.github/workflows/comparator-lean-4-33.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + generate-build-and-compare: + runs-on: ubuntu-latest + name: Import, generate, build and run Comparator + steps: + - name: Checkout Formal Conjectures + uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6 + with: + # The importer pins each workspace to the merge base with upstream + # main, so that ref has to be present. + fetch-depth: 0 + # This job only reads the tree and builds; nothing here pushes, so + # the checkout token has no reason to stay in .git/config where a + # later step or a build script could reach it. + persist-credentials: false + + - name: Read the target pins + id: target + run: | + python3 - <<'PY' >> "$GITHUB_OUTPUT" + import tomllib + + with open("comparator/tools.toml", "rb") as handle: + target = tomllib.load(handle)["target"] + for key in ( + "comparator", + "comparator_repository", + "lean4export", + "lean_toolchain", + ): + print(f"{key}={target[key]}") + PY + + # At this repository's toolchain. The facts the importer reads come + # from an elaborated environment, not from the text, so every module a + # step below imports from has to be built first. + - name: Prepare the extractor and the source modules + uses: ./.github/actions/prepare-extractor + with: + modules: >- + FormalConjectures.Wikipedia.SumOfThreeCubes + FormalConjectures.Wikipedia.Hadamard + FormalConjectures.Wikipedia.Koethe + FormalConjectures.ErdosProblems.«100» + FormalConjectures.ErdosProblems.«940» + FormalConjectures.ErdosProblems.«1038» + FormalConjectures.OEIS.«303656» + FormalConjectures.OEIS.«308734» + FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture + + - name: Build the pinned lean-eval-generator + uses: ./.github/actions/build-lean-eval-generator + + # The elaborator-to-importer boundary, exercised on the oleans the + # build above produced: one plain theorem, a Prop answer slot, a + # non-Prop answer slot, a forall-conclusion (whose binder must not be + # applied), explicit parameters (which must be), and the qualified-id + # collision pair. The comparator run itself needs landrun and stays in + # a separate Linux job. + - name: Comparator generation smoke test + run: | + # The command prints the directory it wrote. Asking it removes the + # only other place that would have to know how a qualified name + # becomes a workspace id, and a change to that rule then fails in + # the code that owns it rather than in twenty lines of YAML. + ws() { + python3 comparator/adapter/make_comparator_workspace.py "$1" --out .comparator + } + hadamard=$(ws exists_hadamard_zero) + large_integers=$(ws erdos_940.variants.large_integers) + parts_i=$(ws erdos_1038.parts.i) + strong=$(ws erdos_100.variants.strong) + koethe=$(ws KotherConjecture.variants.le_KotherRadical) + oeis_a=$(ws OeisA303656.conjecture) + oeis_b=$(ws OeisA308734.conjecture) + curling=$(ws curling_number_conjecture) + echo "PARTS_I=$parts_i" >> "$GITHUB_ENV" + test -d "$hadamard" + grep -q "large_integers_answer : Prop" "$large_integers/Challenge.lean" + grep -q "i_answer : ENNReal" "$parts_i/Challenge.lean" + grep -q "Submission.erdos_100_variants_strong$" "$strong/Solution.lean" + grep -q "le_KotherRadical hI" "$koethe/Solution.lean" + # Two modules declare `conjecture`; qualified default ids keep the + # workspaces apart, and a guillemet module path decodes correctly. + test "$oeis_a" != "$oeis_b" + test -d "$oeis_a" && test -d "$oeis_b" + case "$curling" in *0912_2382*) ;; *) echo "guillemet module lost its digits: $curling"; exit 1 ;; esac + + # The importer-to-generator seam, on a real declaration. + # `--emit-import` writes the exact bytes that cross it — the v1 + # request and its context directory — and running the pinned binary on + # those bytes from inside the emitted directory has to reproduce the + # workspace exactly; if it does not, the emitted artifact is not the + # whole interface. See comparator/OWNERSHIP.md. + - name: Importer to generator seam + env: + WORKSPACE: ${{ env.PARTS_I }} + run: | + HANDED_OVER=$(python3 comparator/adapter/make_comparator_workspace.py \ + erdos_1038.parts.i --emit-import .comparator-import) + export HANDED_OVER + python3 - <<'PY' + import glob + import os + import pathlib + import sys + + sys.path.insert(0, "comparator/adapter") + import leaneval_generator_cli as generator_cli + from leaneval_interface import ProblemManifest + + handed_over = pathlib.Path(os.environ["HANDED_OVER"]).resolve() + workspace = pathlib.Path(os.environ["WORKSPACE"]).resolve() + problem_id = handed_over.name + + # One sidecar, named by the command, found rather than spelled. + (sidecar,) = glob.glob(str(handed_over / "fc-provenance-*.json")) + manifest = ProblemManifest.from_json( + pathlib.Path(sidecar).read_text(encoding="utf-8") + ) + assert len(manifest.source.commit) == 40, manifest.source.commit + assert manifest.source.declaration, "no FC declaration id" + + # The emitted request is fed back as its exact bytes — no reparse, + # no reserialise — which is the claim the seam test exists to check. + request_text = (handed_over / "request.json").read_text(encoding="utf-8") + regenerated = generator_cli.generate( + request_text, cwd=handed_over, expected_ids=[problem_id] + ) + files = regenerated[problem_id] + for name, content in files.items(): + expected = (workspace / name).read_text(encoding="utf-8") + assert content == expected, name + print(f"{len(files)} files reproduced from the emitted request") + PY + + # `--verify` elaborates the marked-up module here, at 4.33.1. It is not a + # substitute for the 4.33 build below; it is what keeps an FC-side + # copying defect from being reported as a LeanEval build failure. + - name: Import and generate two workspaces + # The target toolchain arrives as an environment variable rather than a + # `${{ }}` expansion inside the script, so the shell never has workflow + # syntax substituted into it before it runs. + env: + TARGET_TOOLCHAIN: ${{ steps.target.outputs.lean_toolchain }} + run: | + gen() { + python3 comparator/adapter/make_comparator_workspace.py "$1" \ + --out .comparator --verify + } + PLAIN=$(gen isSumOfThreeCubes_2) + HOLED=$(gen isSumOfThreeCubes_iff_mod_9) + echo "PLAIN=$PLAIN" >> "$GITHUB_ENV" + echo "HOLED=$HOLED" >> "$GITHUB_ENV" + # One plain theorem and one `answer(sorry)` slot typed at 4.33.1. + grep -q "isSumOfThreeCubes_iff_mod_9_answer : Prop" "$HOLED/Challenge.lean" + # Generated for LeanEval, not for here. + grep -q "$TARGET_TOOLCHAIN" "$PLAIN/lean-toolchain" + + - name: Build both workspaces at Lean 4.33 + run: | + for ws in "$PLAIN" "$HOLED"; do + (cd "$ws" && lake update && lake exe cache get && lake build) + done + + - name: Build the pinned Lean 4.33 verifier stack + env: + COMPARATOR_REV: ${{ steps.target.outputs.comparator }} + COMPARATOR_REPOSITORY: ${{ steps.target.outputs.comparator_repository }} + LEAN4EXPORT_REV: ${{ steps.target.outputs.lean4export }} + run: | + git clone "$COMPARATOR_REPOSITORY" "$RUNNER_TEMP/comparator" + git -C "$RUNNER_TEMP/comparator" checkout "$COMPARATOR_REV" + (cd "$RUNNER_TEMP/comparator" && lake build comparator lean4export) + # The lean4export this stack bundles must be the one tools.toml + # declares, or a green run certifies a different exporter. + BUNDLED="$(git -C "$RUNNER_TEMP/comparator/.lake/packages/lean4export" rev-parse HEAD)" + test "$BUNDLED" = "$LEAN4EXPORT_REV" + + # Three Comparator verdicts, each of which has to come out the stated way. + # A run that only ever accepts proves nothing about the gate. + - name: Run Comparator on the generated workspaces + run: | + export COMPARATOR_BIN="$RUNNER_TEMP/comparator/.lake/build/bin/comparator" + export COMPARATOR_LANDRUN="$RUNNER_TEMP/comparator/scripts/fake-landrun.sh" + export COMPARATOR_LEAN4EXPORT="$RUNNER_TEMP/comparator/.lake/packages/lean4export/.lake/build/bin/lean4export" + + # 1. The workspace as generated. Its Submission is `sorry`, which + # adds `sorryAx`, which `permitted_axioms` does not allow. A + # generated workspace that passed before anyone proved anything + # would be worthless. + if (cd "$PLAIN" && lake test); then + echo "::error::Comparator accepted an unproved generated workspace" + exit 1 + fi + + # 2. The same workspace with the statement actually proved. The + # witness is the one this repository's own source gives. + python3 - <<'PY' + import os + import pathlib + + submission = pathlib.Path(os.environ["PLAIN"]) / "Submission.lean" + text = submission.read_text(encoding="utf-8") + filled = text.replace(":= by\n sorry", ":= by\n exact ⟨1, 1, 0, by norm_num⟩") + assert filled != text, "nothing to fill in the generated submission" + submission.write_text(filled, encoding="utf-8") + PY + (cd "$PLAIN" && lake build && lake test) + + # 3. The `answer(sorry)` workspace, with the hole filled by the + # proposition on the other side of the iff and the bridge closed + # by `Iff.rfl`. Comparator accepts this, and it resolves nothing: + # the definition hole is a place where a machine check cannot + # stand in for a human reading the answer. The generated README + # tells the solver so; this asserts it. + python3 - <<'PY' + import os + import pathlib + + root = pathlib.Path(os.environ["HOLED"]) + submission = root / "Submission.lean" + text = submission.read_text(encoding="utf-8") + answer = ( + "noncomputable def isSumOfThreeCubes_iff_mod_9_answer : Prop :=\n" + " ∀ n : ℤ, IsSumOfThreeCubes n ↔ ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])" + ) + # Each replacement must actually fire: a generated shape change + # that made either a no-op would let this verdict pass vacuously. + filled = text.replace( + "noncomputable def isSumOfThreeCubes_iff_mod_9_answer : Prop := sorry", + answer, + ) + assert filled != text, "the answer hole was not where this step expects" + text = filled + filled = text.replace(":= by\n sorry", ":=\n Iff.rfl") + assert filled != text, "the proof hole was not where this step expects" + submission.write_text(filled, encoding="utf-8") + PY + (cd "$HOLED" && lake build && lake test) + echo "Comparator accepted a gamed definition hole; hole values need a human." diff --git a/.github/workflows/fc100-audit.yml b/.github/workflows/fc100-audit.yml new file mode 100644 index 0000000000..6b1fe3cfb8 --- /dev/null +++ b/.github/workflows/fc100-audit.yml @@ -0,0 +1,216 @@ +# Copyright 2026 The Formal Conjectures Authors. + +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at + +# https://www.apache.org/licenses/LICENSE-2.0 + +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: FC100 whole-set audit + +# The whole-set run lean-eval#536 gates the FC import on, as a CI artifact. +# It is two halves, and they are split because they cost differently. +# +# source import every declaration of the frozen set, elaborate each +# marked-up module at this repository's pins, generate every +# workspace through the pinned generator, and classify the set. +# One Mathlib, this repository's. This is where an FC-side defect +# shows, so it runs on every pull request that changes what it +# measures — the adapter, pins, ledger, templates or tooling. +# +# target compile every generated Challenge at LeanEval's pins in one +# shared project. A second Mathlib at a second toolchain, which is +# most of the cost, and it catches target-pin drift rather than an +# FC-side defect. Drift comes from the other repository bumping, +# not from a pull request here, so it runs weekly and on demand. +# +# Failures on either side must match comparator/known_failures.toml exactly: +# an unexpected failure and a silently fixed one both fail, because a gate +# that only ever passes proves nothing. Ordinary statement edits rely on the +# per-PR jobs' representative declarations and the weekly run as backstop. + +concurrency: + group: fc100-audit-${{ github.ref }} + cancel-in-progress: true + +on: + workflow_dispatch: + schedule: + # Weekly, early Monday UTC. + - cron: '17 4 * * 1' + # Dispatch and schedule only reach a workflow on the default branch, so a + # pull request that changes what the audit measures could never show its + # run. Trigger on everything the audit's outcome depends on: the adapter, + # the templates and problem overrides, the pins, the ledger, the composite + # actions that build its tools, and the toolchain the modules elaborate + # under. Ordinary statement edits stay out — the weekly run is their + # backstop, and a whole-set run per problem PR would be two Mathlib builds + # of noise. + pull_request: + paths: + - 'comparator/adapter/**' + - 'comparator/templates/**' + - 'comparator/problems/**' + - 'comparator/tools.toml' + - 'comparator/known_failures.toml' + - '.github/actions/build-lean-eval-generator/**' + - '.github/actions/prepare-extractor/**' + - '.github/workflows/fc100-audit.yml' + - 'FormalConjectures/Subsets/FC100OpenSet1.lean' + - 'lean-toolchain' + - 'lake-manifest.json' + +permissions: + contents: read + +jobs: + source: + runs-on: ubuntu-latest + name: Import, verify and generate FC100 + timeout-minutes: 120 + steps: + - name: Checkout Formal Conjectures + uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6 + with: + # The importer pins each workspace to the merge base with upstream + # main, so that ref has to be present. + fetch-depth: 0 + persist-credentials: false + + # The category tags, source ranges and answer-slot types come from the + # elaborated environment, so every module in the set has to be built. + - name: Prepare the extractor and the whole set + uses: ./.github/actions/prepare-extractor + with: + modules: FormalConjectures.Subsets.FC100OpenSet1 + + - name: Build the pinned lean-eval-generator + uses: ./.github/actions/build-lean-eval-generator + + # `--verify` elaborates every marked-up module at this repository's + # pins; generation runs each import through the pinned binary. Failures + # are recorded per declaration, and the run fails unless they are + # exactly the recorded ones. + - name: Import and verify the whole set + run: | + python3 comparator/adapter/make_comparator_workspace.py --set FC100OpenSet1 \ + --verify --out .fc100 --report fc100-report.json \ + --known-failures comparator/known_failures.toml + + # The open/solved split is a fact about the set the report must state. + # The list is frozen but its members keep getting solved — that is + # designed lifecycle, not an anomaly (formal-conjectures#5075) — so + # the check here is structural: every member accounted for, every + # category a research one. The report carries the current split. + - name: Check the set classification + run: | + python3 - <<'PY' + import json + + with open("fc100-report.json") as handle: + report = json.load(handle) + categories = report["categories"] + print("classification:", categories) + assert sum(categories.values()) == report["imported"], categories + assert set(categories) <= {"research open", "research solved"}, categories + assert sum(categories.values()) + report["source_failed"] == 100, categories + PY + + # The artifact is the review evidence, so it carries what produced the + # result, not just the result: the exact request bytes, every workspace + # with its provenance sidecar, the report, and a manifest digesting + # each file so the bundle can vouch for itself. The target job below + # consumes this same artifact rather than generating its own. + - name: Digest the audit bundle + if: always() + run: | + python3 - <<'PY' + import pathlib + import sys + + sys.path.insert(0, "comparator/adapter") + from leaneval_interface import dump_json, sha256_text + + # The same digest and the same serialisation the sidecars use, so a + # reader can compare a manifest entry with the digest recorded + # inside the artifact it names. + def digest(path): + return sha256_text(path.read_text(encoding="utf-8")) + + manifest = {} + for name in ("fc100-report.json",): + path = pathlib.Path(name) + if path.is_file(): + manifest[str(path)] = digest(path) + root = pathlib.Path(".fc100") + if root.is_dir(): + for path in sorted(root.rglob("*")): + if path.is_file(): + manifest[str(path)] = digest(path) + pathlib.Path("bundle-manifest.json").write_text( + dump_json(manifest, sort_keys=True), encoding="utf-8" + ) + print(f"{len(manifest)} files digested") + PY + + - name: Upload the generated set + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + with: + name: fc100-source-bundle + path: | + fc100-report.json + bundle-manifest.json + .fc100/ + if-no-files-found: warn + include-hidden-files: true + + # The second Mathlib. It answers "does LeanEval's toolchain still accept + # what we generate", and that changes when the other repository bumps, not + # when a pull request here edits the adapter. So it runs weekly and on + # demand, against the set the job above generated rather than regenerating + # it. `merge_group` is deliberately not a trigger: it does not support path + # filters, so this would then run on every merge in the repository. + target: + runs-on: ubuntu-latest + name: Compile FC100 at LeanEval pins + timeout-minutes: 240 + needs: source + if: github.event_name != 'pull_request' + steps: + - name: Checkout Formal Conjectures + uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6 + with: + persist-credentials: false + + - name: Install elan + uses: ./.github/actions/install-elan + + - name: Download the generated set + uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0 + with: + name: fc100-source-bundle + + # Kim's shared-project arrangement: every generated ChallengeDeps and + # Challenge compiles in one Lake project at LeanEval's pins, so Mathlib + # is built once for the whole set rather than once per workspace. + - name: Compile every generated Challenge at LeanEval pins + run: | + python3 comparator/adapter/compile_fc100_target.py .fc100 \ + --project "$RUNNER_TEMP/fc100-target" \ + --report fc100-target-report.json \ + --known-failures comparator/known_failures.toml + + - name: Upload the target report + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + with: + name: fc100-target-report + path: fc100-target-report.json + if-no-files-found: warn diff --git a/.gitignore b/.gitignore index a62e89ebd8..d464550c62 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,8 @@ FormalConjectures/All.lean # Python bytecode from the scripts in `scripts/`. __pycache__/ +.comparator/ +.comparator-import/ +# Whole-set audit output (make_comparator_workspace.py --set) +.fc100/ +.fc100v/ diff --git a/comparator/OWNERSHIP.md b/comparator/OWNERSHIP.md new file mode 100644 index 0000000000..1272250758 --- /dev/null +++ b/comparator/OWNERSHIP.md @@ -0,0 +1,166 @@ +# What this repository owns, and what it hands over + +[`lean-eval#536`](https://github.com/leanprover/lean-eval/pull/536) §10 divides +this integration in two, and the other half now exists: +[`leanprover/lean-eval-generator`](https://github.com/leanprover/lean-eval-generator) +is the extracted generator core — the part that turns a Lean module plus hole +metadata into a Challenge / Solution / Submission workspace, with the import +and scope fidelity work from +[`lean-eval#531`](https://github.com/leanprover/lean-eval#531). It is a +deterministic Lean CLI with a frozen, versioned JSON contract, consumed at the +exact revision `comparator/tools.toml` pins under `[generator]`. **The Formal +Conjectures importer does not fork the generation logic.** It maps FC +declarations and metadata to a schema-version-1 request, and records the FC source commit +and declaration id for every problem. + +## The seam + + comparator/adapter/fc_source.py reading FC source: where a declaration + is, its preamble, notation, answer slots + comparator/adapter/fc_leaneval_importer.py FC declaration -> (module, manifest), + assembled from those answers + comparator/adapter/leaneval_interface.py the request built from them, the + response checked against its digests + comparator/adapter/leaneval_generator_cli.py runs the pinned binary, nothing else + +`comparator/adapter/make_comparator_workspace.py` is the command that runs one after the +other. The arrow points one way: the CLI plumbing imports the interface and +never the importer, and a test asserts that. + +### What crosses it + +One **v1 request** (`schemas/request-v1.schema.json` at the pinned generator +revision is normative). Per problem it carries: + +| Field | Comes from | +|---|---| +| `moduleContent` | the rendered marked-up module: the statement's copied FC-local closure, the scope directives in force where it was written, one `noncomputable def : := sorry` per `answer(sorry)` slot, and the statement with its proof replaced by `sorry` — in that order, requiring Mathlib and nothing else | +| `resolvedHoles` | a source span, kind, and explicit parameters for each hole, computed from the rendered text — exactly, because this side rendered it | +| `holes`, `id`, `moduleName` | the qualified declaration name, slugged; two modules declaring `conjecture` in different namespaces must not share a workspace | +| `group`, `status`, `visible`, `statementRevision`, `submitter`, `tags` | LeanEval catalog policy, not source facts: they arrive as an explicit `ImportPolicy` the command constructs, with the draft-intake values stated in `make_comparator_workspace.import_policy`. For a frozen-set import the policy's group is the set itself — the list is immutable while its members keep getting solved, so every member stays in the open-conjectures display and the category rides along as a tag; for a single import the declaration's `@[category ...]` tag decides. A declaration that is not a problem is refused either way | +| `leanToolchain`, `mathlib` | LeanEval's pins, from `[target]` in `tools.toml` — the consumer's, never this repository's | +| `templates.workspaceTest` | `comparator/templates/WorkspaceTest.lean`, which stays FC-supplied: the contract requires the consumer to provide it | +| `contextRoot` | a directory this side materialises: the module file the generator byte-checks against `moduleContent`, and a synthesised `.ilean` carrying the spans above, because generator schema version 1 still resolves declaration spans from compiled metadata | + +The module carries no markers of any kind. `@[eval_problem]` does not exist +outside lean-eval, so a module carrying it could not elaborate under +`--verify`; the ranges in the request already say where the holes are. + +The module's `import Mathlib` header is faithful, not convenient. Every +problem file under `FormalConjectures/` imports exactly +`FormalConjecturesUtil`, which `public import`s all of Mathlib, so each +statement already elaborates under the full library; no file in the corpus +carries a narrow or third-party import the header could widen away. What the +header drops — the FC-local layer — travels as the copied closure, and +`--verify` elaborates under exactly the header that ships. The remaining +source-versus-target gap is the Mathlib revision, which the sidecar records +on both sides and the cross-pin CI job builds. + +The module is one file rather than four strings because the importer can then +elaborate exactly what it is about to hand over: `--verify` runs the module +through this checkout's Mathlib, so an FC-side defect — a lost `open`, an +unrecognised `local notation`, a namespace nothing declares any more — fails +here and not in lean-eval's CI. + +The response is the complete workspace file map with a SHA-256 digest per +file, and every digest is checked before a byte lands on disk. + +### Provenance rides beside the request, not in it + +lean-eval#536 requires each imported problem to record the FC source commit +and declaration id. The schema-version-1 wire format has no field for either — its optional +`source` is one free-text line — and lean-eval keeps that format frozen on +purpose, so the sidecar is the schema-version-1 provenance boundary **by design**, not a +stopgap (kim-em on #4951, 2026-08-21); a typed provenance object is a future-contract-revision +matter and does not gate the FC100 import. The manifest this repository +builds (`ProblemManifest`: commit, path, blob, module, declaration, copied +dependencies, the pins the hole types were read at) is written beside the +generated workspace as `fc-provenance.json`, and beside the emitted request +as `fc-provenance-.json`. + +Three properties make it fit to be that boundary. It is **strict**: a record +with a key the schema does not name is refused on load. It is +**deterministic**: serialisation is key-sorted, so the same record is the +same bytes. And it is **digested**: it carries the SHA-256 of the exact +`moduleContent` that crossed the seam and of every generated file the +response returned, so a workspace holds its own chain — FC commit → module +bytes → generated bytes — and each link can be checked without this +repository. It is also what makes regeneration possible when Formal +Conjectures corrects a misformalisation upstream. + +## What stays Formal Conjectures' permanently + +| File | Why it cannot move | +|---|---| +| `comparator/adapter/fc_source.py` | reads this repository's own Lean: where a declaration is, the file-scoped directives in force where it was written, the FC-defined notation it uses, its `answer(sorry)` slots and their elaborated types, and the pins the text was read at. Holds the strict `FactsRecord` boundary for the extractor's payload, and the prefetch cache a set run fills through the extractor's `--batch` arm so the Mathlib import is paid once | +| `comparator/adapter/fc_leaneval_importer.py` | assembles the marked-up module and the provenance record from those answers: resolves the declaration against an exact FC commit, copies the FC-local closure, hoists each slot, and records the provenance | +| `comparator/adapter/ComparatorFacts/` and `comparator_facts.lean` | the Lean extractor (a small library — `Binders.lean` recovers declaration-header binder boundaries from source syntax, `Extract.lean` reads the elaborated environment — and a thin executable): source ranges, declaration-header binder boundaries, elaborated binder names/explicitness, answer-slot types (anywhere in the statement, hypothesis binders included), and the `@[category ...]` tag. One `module declaration` pair per invocation, or `--batch` pairs on stdin sharing a single environment, one JSON object per line in input order. The parsed source distinguishes header parameters from `∀` binders in the conclusion; every emitted binder fact still comes from the elaborated environment. | +| `comparator/adapter/leaneval_interface.py` | the request builder and response checker — the FC side of the wire format, permanently, since the consumer owns hole resolution under the schema-version-1 contract | +| `comparator/adapter/leaneval_generator_cli.py` | plumbing for the pinned binary | +| `comparator/adapter/make_comparator_workspace.py` | the command, the emitted seam artifact, and the whole-set batch run| +| `comparator/adapter/known_failures.py` | the known-failures ledger's format and loader, shared by the set run and the target-stage compile | +| `comparator/templates/WorkspaceTest.lean` | the workspace test template the contract requires the consumer to supply | +| `comparator/problems/*.toml` | the rare source-boundary facts the compiled environment cannot recover: which module when two declare the same name, and an explicit copied proof dependency when opaque theorem-value erasure removes it from the compiled dependency graph | +| `comparator/tools.toml` | the pins, in one machine-readable place: LeanEval's under `[target]`, the generator revision under `[generator]`; every key has a consumer in the adapter or CI | + +The tests beside each file pin real defects: the importer suite covers +extraction, the interface suite covers the wire shapes, and the command suite +runs the real pinned binary end to end when one is built (CI always does). + +Nothing in the importer names a workspace file, a workspace layout, or an +import graph. If a change to it would, the change belongs on the other side. + +## Not built, on purpose + +**Disproof support.** Blocked upstream: Comparator has no interface for a +plain-statement disproof, and the overhaul plan defers it to the +open-conjectures phase. Nothing here anticipates one. + +**Multi-file Challenge support.** The generator carries a statement's whole +closure in `ChallengeDeps`, which is one file. Measured over `FC100OpenSet1`, +no statement needs another FC problem module, so this does not block the +first import. + +**A vendored workspace.** A workspace checked into this repository is a copy +of generator output, so it drifts from the generator, and it says nothing +about the importer because a human wrote it. The Lean 4.33 evidence comes +from generating one in CI instead. + +**Lifecycle.** Result records, resubmission, and revision tracking are +LeanEval's, per lean-eval#536. This repository regenerates and opens a pull +request; it keeps no state about what happened to one. + +## What this side cannot settle alone + +1. **Provenance fields in the contract.** Generator schema version 1 has no + home for the FC source commit and declaration id that §10 requires by + name, so they travel as a sidecar. A passthrough or provenance field in a + future generator contract revision would let a generated workspace carry + its own origin. Related: + `mathlib-initiative/formalization.yaml` already standardises a source + repository, revision, declaration and Comparator config — + `Paul-Lez/hadamard-668-comparator` uses it to describe a wrapper around FC + at `1721605c` — but its required `project`, `sources`, `automation` and + `review` sections belong to whoever formalised the statement rather than + to an import, and it deliberately omits pins. So the question is which + object is which, not whether to publish a schema. +2. **The `definition_names` config field is undocumented.** Comparator's + published no-hole config does not carry it, and hole support depends on + the comparator commit pinned in `tools.toml`. A generated workspace with + an `answer(sorry)` hole is only checkable against that build. +3. **Answer-slot types are read under this repository's toolchain.** The + importer asks Formal Conjectures' elaborated environment, at FC's pins, + for the type of each slot; the workspace is built at LeanEval's. The + overhaul plan assigns the re-resolution to LeanEval — the consumer + re-resolves hole metadata under its own target environment — and the + whole-set audit run is what observes the gap meanwhile: it generates at + FC's pins and compiles every generated workspace at LeanEval's, with the + failures recorded by name in `comparator/known_failures.toml` and + asserted exactly. Which side owns the answer when the two environments + disagree about a type is lean-eval's call. +4. **Who triggers regeneration is unassigned.** The plan gives the importer + the duty to regenerate and re-PR when Formal Conjectures fixes a + misformalisation upstream, and gives lifecycle to LeanEval. Nothing yet + says which side watches FC commits for a change to an imported + declaration. The provenance sidecar records what is needed to answer the + question — commit, path, blob and declaration — but nobody is asking it. diff --git a/comparator/README.md b/comparator/README.md new file mode 100644 index 0000000000..3530da6715 --- /dev/null +++ b/comparator/README.md @@ -0,0 +1,189 @@ +# Formal Conjectures to LeanEval adapter + +This directory contains the Formal Conjectures side of the integration with +[`leanprover/lean-eval`](https://github.com/leanprover/lean-eval) and +[`leanprover/comparator`](https://github.com/leanprover/comparator), following +the ownership split proposed in +[`lean-eval#536`](https://github.com/leanprover/lean-eval/pull/536), with +coordination tracked in +[`lean-eval#533`](https://github.com/leanprover/lean-eval/issues/533) and +[`formal-conjectures#4930`](https://github.com/google-deepmind/formal-conjectures/issues/4930). + +**[`OWNERSHIP.md`](OWNERSHIP.md) is the map**: which code is Formal +Conjectures' permanently, what crosses the seam to the pinned +[`leanprover/lean-eval-generator`](https://github.com/leanprover/lean-eval-generator), +and what the interface still needs from lean-eval. Read it first. This file is +the operator's page: the commands, their inputs, and the pins. + +## The generator binary + +Workspace generation runs the extracted generator at the revision `tools.toml` +pins under `[generator]`. Build it once — the package depends on nothing, so +this is quick — and point the importer at it: + +```bash +git clone https://github.com/leanprover/lean-eval-generator /tmp/lean-eval-generator +git -C /tmp/lean-eval-generator checkout "$(python3 -c ' +import tomllib; print(tomllib.load(open("comparator/tools.toml","rb"))["generator"]["rev"])')" +(cd /tmp/lean-eval-generator && lake build) +export LEAN_EVAL_GENERATOR_BIN=/tmp/lean-eval-generator/.lake/build/bin/lean-eval-generator +``` + +Import and `--verify` are offline as before; only generation needs the binary. + +## Two toolchains + +Formal Conjectures elaborates its own source under its own pinned toolchain. +LeanEval is the benchmark host: an imported problem is built and checked under +LeanEval's pinned Lean 4.33 and matching Mathlib. Supporting the integration +does not require a repository-wide toolchain upgrade here. + +So the importer reads a declaration's source range, binders, dependencies and +`answer(sorry)` slot types from an environment elaborated at *this* +repository's toolchain, and the workspace it produces is pinned to *LeanEval's* +toolchain and Mathlib. The request carries LeanEval's pins; the provenance +sidecar `fc-provenance.json` records the pins the hole types were read at. +`.github/workflows/comparator-lean-4-33.yml` generates a +workspace here and builds and Comparator-checks it there, in one job, which is +what turns the gap between them into something observed rather than assumed. + +## Generate one workspace + +```bash +python3 comparator/adapter/make_comparator_workspace.py erdos_940.variants.large_integers +``` + +Use `--out` to choose the parent directory. Generation refuses to overwrite an +existing workspace: it writes into a temporary directory and renames the +complete workspace into place. + +The importer stops when any file it read differs from the pinned upstream +revision — the statement's own file, every copied dependency's, every copied +notation command's, and the pin files the record quotes. One workspace, one +source revision: a pinned statement cannot be combined with working-tree +copied text, and an untracked file cannot slip in unrecorded. + +`--verify` elaborates the marked-up module before anything is written, so an +FC-side copying defect fails here rather than in LeanEval CI. It runs at this +repository's Lean and Mathlib, so it is not evidence about the 4.33 build. + +The workspace contains `ChallengeDeps.lean` with the statement's copied Formal +Conjectures closure, `Challenge.lean` with the trusted statement and its proof +hole, `Submission.lean` and `Submission/` where a solver works, `Solution.lean` +connecting the two, `config.json` with the theorem targets, definition targets +and permitted axioms, `holes.json`, and the `fc-provenance.json` sidecar this +side adds beside the generator's files. `Solution.lean` is fixed: it fails +to build if the submission changes the statement. Comparator rejects `sorryAx`, +because it is not in the permitted axiom list. + +### Emit only what this repository owns + +```bash +python3 comparator/adapter/make_comparator_workspace.py erdos_1038.parts.i \ + --emit-import .comparator-import +``` + +This writes the exact bytes that cross the seam — `request.json`, the +`context/` directory the schema-version-1 contract reads, and the provenance sidecar — and +generates no workspace. "Exact" is literal: generation pipes the same +serialisation to the binary that this writes to disk, the sidecar records its +SHA-256 under `digests.request`, and the seam test feeds the emitted file +back byte-for-byte. Running the pinned binary on that request from inside +the emitted directory yields the same file map generation would have written, +which is what makes the seam checkable rather than asserted. + +### Import a whole set + +```bash +python3 comparator/adapter/make_comparator_workspace.py --set FC100OpenSet1 \ + --verify --report fc100-report.json \ + --known-failures comparator/known_failures.toml +``` + +One request carries every declaration that imports; failures are recorded per +declaration in the report instead of aborting the run. The set is prefetched +through `comparator_facts --batch`, so the Mathlib environment is imported +once for the whole run rather than once per declaration; a declaration the +batch cannot answer falls back to its own single run and fails with that +run's message. With +`--known-failures`, the run fails unless the failures are exactly the recorded +ones — an unexpected failure and a silently fixed one both count. + +### Supported inputs + +- theorem proofs; +- definition answers represented by `answer(sorry)`; +- helper modules under `Submission/`. + +Plain-statement disproofs remain out of scope until Comparator provides an +upstream interface for them. + +The importer fails closed on ambiguous declarations, source drift, inaccessible +binders, unsupported dependencies, answer-slot types that cannot be matched +safely, and existing output. + +## Problem files + +`problems/*.toml` is an input, not the LeanEval manifest: it records the +choices this repository's Lean source cannot make for itself, and the importer +reads it. The request the generator receives, and the provenance sidecar, are +derived. + +Most declarations need no problem file. Add one TOML file under `problems/` +only when two files declare the same name, which is the one thing the Lean +environment cannot resolve. + +| Field | Meaning | +|---|---| +| `id` | Workspace name. It must match the TOML filename. | +| `declaration` | Lean declaration name. | +| `module` | Source file when the declaration name is ambiguous. | + +There is deliberately nothing else. The source citation comes from the module +docstring's `*Reference:*` line, because a copy kept here drifts from the one +the repository maintains — the copy this directory used to hold for +`Margulis.lean` had already lost the `v3` the docstring pins. An answer-slot +type Lean reports ambiguously is a `--answer-type` argument rather than a +field, since no problem currently needs one and a field nothing sets is a +format nobody checks. + +Run the problem-file check after moving or renaming a declaration: + +```bash +python3 comparator/adapter/make_comparator_workspace.py --validate +``` + +## Tool pins + +`tools.toml` is the one machine-readable source, and every key in it has a +consumer in the adapter or in CI — a pin nothing reads is confidence without +control, and gets deleted. `[target]` are LeanEval's pins: the Lean toolchain +and Mathlib revision every generated workspace is pinned to, and the +Comparator and `lean4export` commits that check it. `[generator]` is the +extracted generator revision every request is written against; bumping it is +a contract change and has to survive the seam round-trip test. Generation +itself does not run Comparator. For a local Comparator run under this +repository's own toolchain, build `lean4export` from its `v4.33.0` tag — +upstream has no v4.33.1 tag yet, and patch releases share the export format. + +## Conformance before a public import + +The adapter should cover these boundary cases before importing a frozen set: + +- a plain theorem proof; +- a `Prop`-valued `answer(sorry)` slot; +- a non-`Prop` answer slot; +- explicit declaration parameters versus `∀` binders in the conclusion; +- trusted helper dependencies requiring `ChallengeDeps` or multiple trusted + files. + +`comparator-lean-4-33.yml` exercises those distinctions: it generates eight +declarations covering each case, checks the importer-to-generator seam by +regenerating from the emitted request, and builds two of them at LeanEval's +pins to run Comparator on. It validates extraction and adapter behaviour, not +mathematical correctness or maintainer acceptance. + +`FC100OpenSet1` is a frozen list whose members keep getting solved — designed +lifecycle, not an anomaly (formal-conjectures#5075). The whole set imports +into the open-conjectures group, with each member's current category riding +along as a tag; the audit report states the split as it stands on each run. diff --git a/comparator/adapter/ComparatorFacts.lean b/comparator/adapter/ComparatorFacts.lean new file mode 100644 index 0000000000..a988409ea2 --- /dev/null +++ b/comparator/adapter/ComparatorFacts.lean @@ -0,0 +1,18 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import ComparatorFacts.Binders +import ComparatorFacts.Extract diff --git a/comparator/adapter/ComparatorFacts/Binders.lean b/comparator/adapter/ComparatorFacts/Binders.lean new file mode 100644 index 0000000000..c73753382c --- /dev/null +++ b/comparator/adapter/ComparatorFacts/Binders.lean @@ -0,0 +1,445 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Lean + +open Lean Meta + +/-! +# Declaration binder boundaries, from source syntax + +A theorem proved by bare `sorry` can be stored as a full-type `sorryAx`, so the +proof value's lambda arity does not reliably separate header parameters from +binders in the conclusion. This subsystem recovers that boundary from the +declaration's source text and matches it against the elaborated telescope; +every binder fact emitted still comes from the environment. -/ + +/-- Collect every node of one syntax kind. A declaration command must contain +exactly one `declSig`; finding zero or more than one means we did not parse the +source range we thought we did, and the importer fails closed. -/ +partial def collectKind (kind : Name) (stx : Syntax) (found : Array Syntax := #[]) : + Array Syntax := + let found := if stx.isOfKind kind then found.push stx else found + stx.getArgs.foldl (fun acc child => collectKind kind child acc) found + +structure SourceBinder where + name? : Option Name + info : BinderInfo + deriving Repr + +def sourceBinderName (stx : Syntax) : Except String (Option Name) := + if stx.isIdent then .ok (some stx.getId) + else if stx.isOfKind ``Lean.Parser.Term.hole then .ok none + else .error s!"unsupported declaration binder name {stx.getKind}: {stx}" + +/-- The names and binder kinds introduced by one declaration-header group. -/ +def declarationBinderGroup (binder : Syntax) : Except String (Array SourceBinder) := do + if binder.isIdent || binder.isOfKind ``Lean.Parser.Term.hole then + return #[{ name? := ← sourceBinderName binder, info := .default }] + if binder.isOfKind ``Lean.Parser.Term.instBinder then + let some optionalName := binder[1]? + | throw s!"malformed instance binder: {binder}" + let name? ← match optionalName.getArgs[0]? with + | some name => sourceBinderName name + | none => pure none + return #[{ name?, info := .instImplicit }] + let info? := + if binder.isOfKind ``Lean.Parser.Term.explicitBinder then some BinderInfo.default + else if binder.isOfKind ``Lean.Parser.Term.implicitBinder then some .implicit + else if binder.isOfKind ``Lean.Parser.Term.strictImplicitBinder then some .strictImplicit + else none + let some info := info? + | throw s!"unsupported declaration binder syntax {binder.getKind}: {binder}" + let some names := binder[1]? + | throw s!"malformed declaration binder: {binder}" + if names.getArgs.isEmpty then + throw s!"declaration binder has no names: {binder}" + names.getArgs.mapM fun name => do + return { name? := ← sourceBinderName name, info } + +def declarationSignature (command : Syntax) : Except String Syntax := do + let signatures := collectKind ``Lean.Parser.Command.declSig command + let [signature] := signatures.toList + | throw s!"expected exactly one declaration signature, found {signatures.size}" + return signature + +def declarationBinders (command : Syntax) : Except String (Array SourceBinder) := do + let signature ← declarationSignature command + let some header := signature[0]? + | throw "declaration signature has no binder header" + header.getArgs.foldlM (fun binders binder => do + return binders ++ (← declarationBinderGroup binder)) #[] + +/-- Number of parameters written before the colon in a declaration header. + +This is deliberately a syntax boundary, not a proof-value heuristic: +`theorem foo (n : Nat) : P n` has one declaration parameter, while +`theorem foo : ∀ n : Nat, P n` has none. Lean 4.32 may store a theorem proved +by `sorry` as a `sorryAx` at the full forall type, with no lambda wrappers, so +the old proof-value lambda arity silently reported zero for the first form. +The syntax supplies only the boundary; names, types, and explicitness still +come from the elaborated telescope below. -/ +def declarationBinderCount (command : Syntax) : Except String Nat := do + return (← declarationBinders command).size + +def sourceBinderMatches (source : SourceBinder) (elaborated : LocalDecl) : Bool := + source.info == elaborated.binderInfo && match source.name? with + | some name => name == elaborated.userName + | none => true + +def sourceBindersMatchAt (source : Array SourceBinder) (elaborated : Array LocalDecl) + (start : Nat) : Bool := + source.zipIdx.all fun (binder, offset) => + match elaborated[start + offset]? with + | some candidate => sourceBinderMatches binder candidate + | none => false + +/-- Locate the end of the declaration parameters in the elaborated telescope. + +Lean inserts used outer `variable`s before the binders written in the +declaration header. We therefore locate the exact typed/named header sequence +inside the telescope and retain everything through its end. This handles +Köthe's `{R} [Ring R]` outer parameters as well as ordinary self-contained +headers. Multiple matches are rejected rather than guessed. -/ +def declarationParameterBoundary (command : Syntax) (conclusion : Array SourceBinder) + (elaborated : Array LocalDecl) : Except String Nat := do + let source ← declarationBinders command + if source.isEmpty then + if conclusion.size > elaborated.size then + throw s!"source conclusion has {conclusion.size} binders, but the elaborated type has only {elaborated.size}" + let boundary := elaborated.size - conclusion.size + unless sourceBindersMatchAt conclusion elaborated boundary do + throw s!"source conclusion binders {repr conclusion} do not match the elaborated telescope suffix" + return boundary + if source.size > elaborated.size then + throw s!"source header has {source.size} binders, but the elaborated type has only {elaborated.size}" + let starts := (Array.range (elaborated.size - source.size + 1)).filter + (sourceBindersMatchAt source elaborated) + let [start] := starts.toList + | throw s!"expected one match for {source.size} source-header binders in the elaborated telescope, found {starts.size}" + return start + source.size + +def parseDeclarationBinderCount (env : Environment) (source : String) : Except String Nat := do + let command ← Parser.runParserCategory env `command source + declarationBinderCount command + +inductive ScanToken where + | signatureColon + | bodyMarker + | comma + | arrow + | iff + | openParen + | openBrace + | openBracket + | openStrict + | closeParen + | closeBrace + | closeBracket + | closeStrict + +def scanTokenAt (wanted : ScanToken) (chars : Array Char) (i : Nat) : Option Nat := + match wanted with + | .signatureColon => + if chars[i]? == some ':' && chars[i + 1]? != some '=' then some 1 else none + | .bodyMarker => + if chars[i]? == some ':' && chars[i + 1]? == some '=' then some 2 else none + | .comma => if chars[i]? == some ',' then some 1 else none + | .arrow => + if chars[i]? == some '→' then some 1 + else if chars[i]? == some '-' && chars[i + 1]? == some '>' then some 2 + else none + | .iff => if chars[i]? == some '↔' then some 1 else none + | .openParen => if chars[i]? == some '(' then some 1 else none + | .openBrace => if chars[i]? == some '{' then some 1 else none + | .openBracket => if chars[i]? == some '[' then some 1 else none + | .openStrict => if chars[i]? == some '⦃' then some 1 else none + | .closeParen => if chars[i]? == some ')' then some 1 else none + | .closeBrace => if chars[i]? == some '}' then some 1 else none + | .closeBracket => if chars[i]? == some ']' then some 1 else none + | .closeStrict => if chars[i]? == some '⦄' then some 1 else none + +/-- Find syntax punctuation at delimiter depth zero, ignoring comments and +strings. This scanner does not interpret terms; it only lets us replace the +result type with `True` before asking Lean's real command parser to read the +declaration header. Scoped notation in the result therefore cannot make an +otherwise ordinary header unparseable. -/ +partial def findTopLevelToken (wanted : ScanToken) (text : String) : Option (Nat × Nat) := + let chars := text.toList.toArray + let rec loop (i paren brace bracket strict blockComment : Nat) + (lineComment inString escaped : Bool) : Option (Nat × Nat) := + if i >= chars.size then none else + let current := chars[i]! + let next := chars[i + 1]? + if lineComment then + loop (i + 1) paren brace bracket strict blockComment (current != '\n') inString false + else if blockComment > 0 then + if current == '/' && next == some '-' then + loop (i + 2) paren brace bracket strict (blockComment + 1) false inString false + else if current == '-' && next == some '/' then + loop (i + 2) paren brace bracket strict (blockComment - 1) false inString false + else + loop (i + 1) paren brace bracket strict blockComment false inString false + else if inString then + if escaped then loop (i + 1) paren brace bracket strict 0 false true false + else if current == '\\' then loop (i + 1) paren brace bracket strict 0 false true true + else loop (i + 1) paren brace bracket strict 0 false (current != '"') false + else if current == '-' && next == some '-' then + loop (i + 2) paren brace bracket strict 0 true false false + else if current == '/' && next == some '-' then + loop (i + 2) paren brace bracket strict 1 false false false + else if current == '"' then + loop (i + 1) paren brace bracket strict 0 false true false + else if paren == 0 && brace == 0 && bracket == 0 && strict == 0 then + match scanTokenAt wanted chars i with + | some width => some (i, width) + | none => match current with + | '(' => loop (i + 1) 1 brace bracket strict 0 false false false + | '{' => loop (i + 1) paren 1 bracket strict 0 false false false + | '[' => loop (i + 1) paren brace 1 strict 0 false false false + | '⦃' => loop (i + 1) paren brace bracket 1 0 false false false + | _ => loop (i + 1) paren brace bracket strict 0 false false false + else match current with + | '(' => loop (i + 1) (paren + 1) brace bracket strict 0 false false false + | ')' => loop (i + 1) (paren - 1) brace bracket strict 0 false false false + | '{' => loop (i + 1) paren (brace + 1) bracket strict 0 false false false + | '}' => loop (i + 1) paren (brace - 1) bracket strict 0 false false false + | '[' => loop (i + 1) paren brace (bracket + 1) strict 0 false false false + | ']' => loop (i + 1) paren brace (bracket - 1) strict 0 false false false + | '⦃' => loop (i + 1) paren brace bracket (strict + 1) 0 false false false + | '⦄' => loop (i + 1) paren brace bracket (strict - 1) 0 false false false + | _ => loop (i + 1) paren brace bracket strict 0 false false false + loop 0 0 0 0 0 0 false false false + +def sliceChars (text : String) (start stop : Nat) : String := + String.ofList (text.toList.toArray.extract start stop).toList + +def forallBinders (term : Syntax) : Except String (Array SourceBinder) := do + let some marker := term[0]? + | throw s!"malformed forall syntax: {term}" + unless marker.isAtom && (marker.getAtomVal == "∀" || marker.getAtomVal == "forall") do + throw s!"expected forall syntax, got {term.getKind}: {term}" + let some binderSlot := term[1]? + | throw s!"forall syntax has no binder: {term}" + let mut binders := #[] + if binderSlot.isOfKind `null then + for binder in binderSlot.getArgs do + binders := binders ++ (← declarationBinderGroup binder) + else if binderSlot.isIdent then + binders := binders.push { name? := some binderSlot.getId, info := .default } + else + let some name := binderSlot.getArgs[0]? + | throw s!"unsupported forall binder syntax {binderSlot.getKind}: {binderSlot}" + binders := binders.push { name? := ← sourceBinderName name, info := .default } + let some predicate := term[2]? + | throw s!"forall syntax has no predicate slot: {term}" + let isBareTypeSpec := predicate.getArgs[0]?.any + (·.isOfKind ``Lean.Parser.Term.typeSpec) + if !predicate.isNone && !isBareTypeSpec then + binders := binders.push { name? := none, info := .default } + return binders + +/-- Parse only the leading Pi structure of a result type. The remainder is +replaced with `True` before parsing, so scoped term notation later in the +statement is irrelevant. -/ +partial def conclusionBinders (env : Environment) (text : String) : Except String (Array SourceBinder) := do + let text := text.trimAsciiStart.toString + let chars := text.toList.toArray + if chars[0]? == some '(' then + let afterOpen := sliceChars text 1 text.length + match findTopLevelToken .closeParen afterOpen with + | some (close, width) => + let trailing := sliceChars afterOpen (close + width) afterOpen.length + if trailing.trimAscii.isEmpty then + return ← conclusionBinders env (sliceChars afterOpen 0 close) + | none => pure () + let unicodeForall := chars[0]? == some '∀' && chars[1]?.any fun c => + c.isWhitespace || c == '(' || c == '{' || c == '[' || c == '⦃' + let asciiForall := text.startsWith "forall" && chars[6]?.any fun c => + c.isWhitespace || c == '(' || c == '{' || c == '[' || c == '⦃' + if unicodeForall || asciiForall then + let some (comma, width) := findTopLevelToken .comma text + | throw "leading forall has no top-level comma" + let forallPrefix := sliceChars text 0 (comma + width) + let command ← Parser.runParserCategory env `command + ("theorem _boundary : " ++ forallPrefix ++ " True := by trivial") + let signature ← declarationSignature command + let some typeSpec := signature[1]? + | throw "synthetic forall signature has no result type" + let some term := typeSpec[1]? + | throw "synthetic forall result type is malformed" + let here ← forallBinders term + let rest := sliceChars text (comma + width) text.length + return here ++ (← conclusionBinders env rest) + let unicodeExists := chars[0]? == some '∃' && chars[1]?.any fun c => + c.isWhitespace || c == '(' || c == '{' || c == '[' || c == '⦃' + let asciiExists := text.startsWith "exists" && chars[6]?.any fun c => + c.isWhitespace || c == '(' || c == '{' || c == '[' || c == '⦃' + if unicodeExists || asciiExists then + return #[] + -- A top-level comma before the first arrow means the arrow sits inside the + -- body of a binder notation that is not a Pi (`∀ᶠ n in l, p n → q n`, + -- `∃! x, p x → q x`, `∀ᵐ x ∂μ, …`): the elaborated type is an application + -- there, and its telescope is empty. + let commaBeforeArrow : Bool := match findTopLevelToken .arrow text, findTopLevelToken .comma text with + | some (arrow, _), some (comma, _) => comma < arrow + | _, _ => false + match findTopLevelToken .arrow text, findTopLevelToken .iff text with + | some (arrow, width), none => + if commaBeforeArrow then return #[] + let rest := sliceChars text (arrow + width) text.length + return #[{ name? := none, info := .default }] ++ (← conclusionBinders env rest) + | _, _ => return #[] + +structure DeclarationText where + beforeNameEnd : String + afterNameEnd : String + +def firstHeaderGroup (text : String) : Option (Nat × ScanToken × ScanToken × Char × Char) := + let candidates := #[ + (.openParen, .closeParen, '(', ')'), + (.openBrace, .closeBrace, '{', '}'), + (.openBracket, .closeBracket, '[', ']'), + (.openStrict, .closeStrict, '⦃', '⦄')] + candidates.foldl (init := none) fun best (openToken, closeToken, opener, closer) => + match findTopLevelToken openToken text with + | none => best + | some (position, _) => match best with + | none => some (position, openToken, closeToken, opener, closer) + | some current => + if position < current.1 then some (position, openToken, closeToken, opener, closer) + else best + +/-- Erase binder *types* while preserving binder names and kinds. The +elaborated telescope supplies the types; this parser pass needs only the +surface boundary. Erasing types prevents scoped notation inside a binder type +from making the header impossible to parse out of its original file context. -/ +partial def sanitizeHeaderBinders (text : String) : Except String String := do + let some (start, _, closeToken, opener, closer) := firstHeaderGroup text + | return text + let before := sliceChars text 0 start + let afterOpen := sliceChars text (start + 1) text.length + let some (close, width) := findTopLevelToken closeToken afterOpen + | throw s!"unclosed declaration binder beginning with {opener}" + let inner := sliceChars afterOpen 0 close + let rest := sliceChars afterOpen (close + width) afterOpen.length + let universeGroup := opener == '{' && before.trimAsciiEnd.toString.endsWith "." + let rewritten := if universeGroup then + String.singleton opener ++ inner ++ String.singleton closer + else match findTopLevelToken .signatureColon inner with + | some (colon, _) => + String.singleton opener ++ sliceChars inner 0 colon ++ " : True" ++ + String.singleton closer + | none => + if opener == '[' then "[True]" + else String.singleton opener ++ inner ++ String.singleton closer + return before ++ rewritten ++ (← sanitizeHeaderBinders rest) + +/-- Turn an exact declaration slice into a parser-safe header command and the +original result type. -/ +def DeclarationText.headerAndResult (text : DeclarationText) : Except String (String × String) := do + let some (colon, width) := findTopLevelToken .signatureColon text.afterNameEnd + | throw "declaration header has no top-level result colon" + let rawHeader := sliceChars text.afterNameEnd 0 colon + let header := text.beforeNameEnd ++ (← sanitizeHeaderBinders rawHeader) ++ + " : True := by trivial" + let afterColon := sliceChars text.afterNameEnd (colon + width) text.afterNameEnd.length + let result := match findTopLevelToken .bodyMarker afterColon with + | some (body, _) => sliceChars afterColon 0 body + | none => afterColon + return (header, result) + +/-- Read the exact declaration range from the source module. The elaborated +environment remains authoritative for the range and telescope; parsing the +slice is only how we recover where the source header ended. -/ +def declarationSource (modName : Name) (ranges : DeclarationRanges) : IO (Except String DeclarationText) := do + let some path ← (← getSrcSearchPath).findModuleWithExt "lean" modName + | return .error s!"source file for {modName} was not found" + let source ← IO.FS.readFile path + let fileMap := FileMap.ofString source + let start := fileMap.ofPosition ranges.range.pos + let stop := fileMap.ofPosition ranges.range.endPos + let nameStop := fileMap.ofPosition ranges.selectionRange.endPos + if start > nameStop || nameStop > stop || stop > source.rawEndPos then + return .error s!"invalid declaration range for {modName}: {repr ranges.range}" + return .ok { + beforeNameEnd := source.toRawSubstring.extract start nameStop |>.toString + afterNameEnd := source.toRawSubstring.extract nameStop stop |>.toString } + +def binderBoundarySelfTest (env : Environment) : IO UInt32 := do + let cases : Array (String × Nat) := #[ + ("theorem t (n : Nat) (hn : 1 < n) : True := by trivial", 2), + ("theorem t : ∀ n : Nat, 1 < n → True := by intro; trivial", 0), + ("theorem t (x y : Nat) {α : Type} {{β : Type}} [i : Inhabited α] z : True := by trivial", 6) + ] + for (source, expected) in cases do + match parseDeclarationBinderCount env source with + | .ok actual => + if actual != expected then + IO.eprintln s!"binder-boundary self-test expected {expected}, got {actual}: {source}" + return 1 + | .error message => + IO.eprintln s!"binder-boundary self-test failed: {message}: {source}" + return 1 + let mkLocal (index : Nat) (name : Name) (info : BinderInfo) : LocalDecl := + .cdecl index { name := `_selfTest |>.appendIndexAfter index } name (.sort .zero) info .default + let outerAndHeader := #[ + mkLocal 0 `R .implicit, + mkLocal 1 `instR .instImplicit, + mkLocal 2 `I .implicit, + mkLocal 3 `hI .default, + mkLocal 4 `n .default, + mkLocal 5 `instN .instImplicit] + let alignmentCases : Array (String × String × Array LocalDecl × Nat) := #[ + ("theorem t {I : Type} (hI : True) (n : Type*) [Fintype n] : True := by trivial", + "True", outerAndHeader, 6), + ("theorem t (n : Nat) (hn : 1 < n) : True := by trivial", + "True", #[mkLocal 0 `n .default, mkLocal 1 `hn .default], 2), + ("theorem t : ∀ n : Nat, True := by intro; trivial", + "∀ n : Nat, True", #[mkLocal 0 `R .default, mkLocal 1 `n .default], 1), + ("theorem t : ∀ n : Nat, 1 < n → True := by intro; trivial", + "∀ n : Nat, 1 < n → True", #[mkLocal 0 `n .default, mkLocal 1 `h .default], 0), + ("theorem t : True ↔ ∃ n : Nat, 1 < n → True := by simp", + "True ↔ ∃ n : Nat, 1 < n → True", #[], 0), + ("theorem t : ∃ f : Nat → Nat, ∀ n, True → f n = f n := by simp", + "∃ f : Nat → Nat, ∀ n, True → f n = f n", #[], 0), + ("theorem t : True → (∀ n : Nat, 1 < n → True) := by simp", + "True → (∀ n : Nat, 1 < n → True)", + #[mkLocal 0 `h₁ .default, mkLocal 1 `n .default, mkLocal 2 `h₂ .default], 0), + -- Binder notations that elaborate to applications, not Pis: the arrows in + -- their bodies are not declaration parameters (erdos_100.variants.strong). + ("theorem t : ∀ᶠ n in Filter.atTop, 1 < n → True := by simp", + "∀ᶠ n in Filter.atTop, 1 < n → True", #[], 0), + ("theorem t : ∃! n : Nat, 1 < n → True := by simp", + "∃! n : Nat, 1 < n → True", #[], 0), + ("theorem t : True → ∀ᶠ n in Filter.atTop, 1 < n → True := by simp", + "True → ∀ᶠ n in Filter.atTop, 1 < n → True", #[mkLocal 0 `h .default], 0) + ] + for (source, resultType, elaborated, expected) in alignmentCases do + let result := do + let command ← Parser.runParserCategory env `command source + let conclusion ← conclusionBinders env resultType + declarationParameterBoundary command conclusion elaborated + match result with + | .ok actual => + if actual != expected then + IO.eprintln s!"parameter-alignment self-test expected {expected}, got {actual}: {source}" + return 1 + | .error message => + IO.eprintln s!"parameter-alignment self-test failed: {message}: {source}" + return 1 + IO.println "binder-boundary self-test passed" + return 0 diff --git a/comparator/adapter/ComparatorFacts/Extract.lean b/comparator/adapter/ComparatorFacts/Extract.lean new file mode 100644 index 0000000000..a0eb49fa1b --- /dev/null +++ b/comparator/adapter/ComparatorFacts/Extract.lean @@ -0,0 +1,134 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Lean + +/-! +# Environment extraction + +What the elaborated environment knows about a declaration: which FC-local +constants it needs and in what order, how a requested name resolves within a +module, and the binder facts the importer emits. +-/ + +open Lean Meta + +/-- A request matches a name in full, or by dropping any whole prefix. -/ +def declares (declared : Name) (requested : String) : Bool := + let s := declared.toString + s == requested || s.endsWith ("." ++ requested) + +def binderJson (name : Name) (bi : BinderInfo) : Json := + Json.mkObj [("name", toJson name.toString), ("explicit", toJson bi.isExplicit)] + +def moduleOf (env : Environment) (n : Name) : String := + match env.getModuleIdxFor? n with + | some idx => (env.header.moduleNames[idx.toNat]?.getD Name.anonymous).toString + | none => "" + +/-- Declared by this repository, as opposed to arriving with `import Mathlib`. + +A constant with a module index the environment cannot name answers `true` +here rather than `false`. Both answers are wrong in that case, but they fail +in opposite directions: `false` means "arrives with Mathlib, copy nothing", +which drops it from `ChallengeDeps` and is caught only by elaborating the +result, while `true` means "copy it", and a constant with no source range is +reported as a generated dependency, which the importer refuses unless a +copied ancestor explains it. Fail towards the check that exists. -/ +def isFCLocal (env : Environment) (n : Name) : Bool := + match env.getModuleIdxFor? n with + | some idx => + match env.header.moduleNames[idx.toNat]? with + | some name => name.toString.startsWith "FormalConjectures" + | none => true + | none => false + +/-- The FC-local constants a declaration needs, dependencies before dependents. + +Post-order over the dependency graph, expanding through both the type and the +value of each FC-local constant: a definition's body names constants its type +does not, and `ChallengeDeps` has to carry them or the copy will not elaborate. +Mathlib and core constants are not expanded, since they arrive with +`import Mathlib`. -/ +partial def fcOrder (env : Environment) (n : Name) + (seen : Std.HashSet Name) (acc : Array Name) : Std.HashSet Name × Array Name := + if seen.contains n then (seen, acc) else + let seen := seen.insert n + match env.find? n with + -- Reached as a used constant but absent from the environment. Keeping it + -- costs a generated-dependency entry the importer will question; dropping + -- it costs a `ChallengeDeps` that is short by one declaration and says + -- nothing about it. + | none => (seen, acc.push n) + | some info => + let fromValue := match info.value? with + | some v => v.getUsedConstants + | none => #[] + -- An inductive has no value, and its fields live in the constructor + -- rather than in its own type: `structure EdgeN (N D : Nat) where u : V N` + -- has type `Nat → Nat → Type`, which never mentions `V`. Without the + -- constructors here the closure still contains `V`, reached some other + -- way, but orders it after `EdgeN`, and the copy does not elaborate. + let fromCtors := match info with + | .inductInfo val => val.ctors.toArray + | _ => #[] + let children := (info.type.getUsedConstants ++ fromValue ++ fromCtors).filter + fun c => isFCLocal env c && c != n + let (seen, acc) := children.foldl (fun p c => fcOrder env c p.1 p.2) (seen, acc) + (seen, acc.push n) + +/-- One declaration's heartbeat budget, in the context's raw units. A batch +caller multiplies this by its pair count rather than restating it. -/ +def heartbeatsPerDeclaration : Nat := 400000000 + +unsafe def runWithImports {α : Type} (moduleNames : Array Name) + (actionToRun : MetaM α) (heartbeats : Nat := heartbeatsPerDeclaration) : IO α := do + initSearchPath (← getBuildDir) + let imports := moduleNames.map fun n => { module := n } + Lean.enableInitializersExecution + let env ← Lean.importModules imports {} (trustLevel := 1024) (loadExts := true) + -- Twice the default budget, in the context's raw units, which are a + -- thousand times the `maxHeartbeats` option's: 800000 here meant "800" and + -- killed the first query. Finite, so a pathological statement errors and is + -- caught rather than grinding forever, which maxHeartbeats := 0 did. A + -- batch caller scales the budget by its pair count, since one context + -- meters the whole action. + let ctx := { fileName := "", fileMap := default, maxHeartbeats := heartbeats } + let (result, _) ← Core.CoreM.toIO (actionToRun.run' {} {}) ctx { env := env } + return result + +/-- Resolve within one module. Names declared elsewhere are not candidates, +which is what lets one environment holding every module still disambiguate +`conjecture_1_1` the way a per-module import does. -/ +def resolveIn (env : Environment) (modName : Name) (declName : String) : + Except String Name := + let inModule (n : Name) : Bool := + match env.getModuleIdxFor? n with + | some idx => env.header.moduleNames[idx.toNat]? == some modName + | none => false + -- No `isInternal` filter: `erdos_340.variants._33_mem_sub` has a component + -- starting with an underscore, which that heuristic calls internal. The + -- whole-suffix rule in `declares` already keeps auxiliary declarations out, + -- since `foo.proof_1` is not a suffix match for `foo`. + let matches_ := env.constants.toList.filterMap fun (n, _) => + if declares n declName && inModule n then some n else none + match matches_ with + | [] => .error s!"{declName} not found in {modName}" + | [n] => .ok n + | _ => + match matches_.filter (·.toString == declName) with + | [n] => .ok n + | _ => .error s!"{declName} is ambiguous: {matches_}" diff --git a/comparator/adapter/comparator_facts.lean b/comparator/adapter/comparator_facts.lean new file mode 100644 index 0000000000..7b0708baf4 --- /dev/null +++ b/comparator/adapter/comparator_facts.lean @@ -0,0 +1,194 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Lean +import FormalConjecturesUtil.Answer +import FormalConjecturesUtil.Attributes.Basic +import ComparatorFacts.Binders +import ComparatorFacts.Extract + +/-! +The executable over `ComparatorFacts/`: the elaborator-side facts `comparator/adapter/fc_leaneval_importer.py` would otherwise +get by reading Lean with regular expressions. + +Given a module and a declaration name, this prints JSON with what the +elaborated environment knows exactly and the text layer can only guess: + +- the declaration's source range, for slicing its original text; +- its declaration-header binders, with names and explicitness, for the + Solution adapter; +- the type of each `sorry` inside the *statement*, which is the type of an + `answer(sorry)` slot. The `answer_type` field in a `comparator/problems` + file exists only because surface syntax does not carry this; the + environment does. + +Usage: + lake exe comparator_facts + +The declaration may be given in full or by any whole suffix, the same rule +the Python importer uses. +-/ + + +open Lean Meta + +unsafe def main (args : List String) : IO UInt32 := do + match args with + | ["--self-test"] => + runWithImports #[`Mathlib] do binderBoundarySelfTest (← getEnv) + | ["--batch"] => + -- One `{"module": M, "declaration": D}` object per stdin line, one + -- environment for all of them: the Mathlib import dominates a run, and + -- `resolveIn` filters by module, so a shared environment answers each + -- pair exactly as a per-module import does. JSON lines rather than + -- space-delimited fields, because a guillemet name may contain anything. + -- One JSON object per line out, in input order. + let stdin ← IO.getStdin + let lines := (← stdin.readToEnd).splitOn "\n" |>.filter (· ≠ "") + let pairs ← lines.mapM fun line => do + match Json.parse line with + | .error msg => throw <| IO.userError s!"malformed batch line: {line} ({msg})" + | .ok json => + match json.getObjValAs? String "module", json.getObjValAs? String "declaration" with + | .ok modName, .ok declName => pure (modName, declName) + | _, _ => throw <| IO.userError s!"malformed batch line: {line}" + let modules := pairs.foldl (init := #[]) fun acc (m, _) => + if acc.contains m.toName then acc else acc.push m.toName + -- The heartbeat budget is shared by the whole action, so it scales with + -- the batch; each pair keeps the single-run allowance. + runWithImports modules + (heartbeats := pairs.length * heartbeatsPerDeclaration) do + let env ← getEnv + for (modName, declName) in pairs do + let tagged (rest : List (String × Json)) := Json.mkObj <| + [("module", Json.str modName), ("declaration", Json.str declName)] ++ rest + match resolveIn env modName.toName declName with + | .error msg => IO.println (tagged [("error", Json.str msg)]).compress + | .ok n => + try + let payload ← factsPayload env modName.toName n declName + IO.println (tagged [("facts", payload)]).compress + catch e => + IO.println (tagged [("error", Json.str (← e.toMessageData.toString))]).compress + return 0 + | [modName, declName] => + runWithImports #[modName.toName] do + let env ← getEnv + match resolveIn env modName.toName declName with + | .error msg => IO.eprintln msg; return 1 + | .ok n => + IO.println (← factsPayload env modName.toName n declName).pretty + return 0 + | _ => + IO.eprintln "usage: comparator_facts | --batch | --self-test" + return 1 +where + factsPayload (env : Environment) (modName name : Name) (decl : String) : MetaM Json := do + let some info := env.find? name | throwError "{name} vanished from the environment" + let some ranges ← findDeclarationRanges? name + | throwError "{name} has no source range" + -- The statement's sorries are `answer(sorry)` slots; a proof's sorry is + -- not in the *type*, so everything found here is a slot. + -- `findAnswerExprs` is the repository's own detection: it reads the + -- annotation the `answer` elaborator leaves, rather than guessing from + -- `sorryAx` applications. + let answerTypes ← forallTelescope info.type fun xs body => do + -- The slots live anywhere in the statement: a hypothesis binder + -- `(h : c = answer(sorry))` carries one just as the conclusion can. + -- Binder types come from the telescope's local declarations, so the + -- expressions are closed in the local context and inferType works. + let mut found := #[] + for x in xs do + found := found ++ Google.findAnswerExprs (← x.fvarId!.getDecl).type + found := found ++ Google.findAnswerExprs body + found.mapM fun a => do pure (toString (← ppExpr (← inferType a))) + let sourceResult ← declarationSource modName ranges + let declarationText ← match sourceResult with + | .ok source => pure source + | .error message => throwError message + let (header, resultType) ← match declarationText.headerAndResult with + | .ok pieces => pure pieces + | .error message => throwError message + let command ← match Parser.runParserCategory env `command header with + | .ok command => pure command + | .error message => + throwError "could not recover declaration parameters for {name}: {message}" + let conclusion ← match conclusionBinders env resultType with + | .ok binders => pure binders + | .error message => + throwError "could not recover conclusion parameters for {name}: {message}" + let binders ← forallTelescope info.type fun xs _ => do + let declarations ← xs.mapM fun x => x.fvarId!.getDecl + let arity ← match declarationParameterBoundary command conclusion declarations with + | .ok arity => pure arity + | .error message => + throwError "could not align declaration parameters for {name}: {message}" + (declarations.extract 0 arity).mapM fun d => + pure (binderJson d.userName d.binderInfo) + let rangeJson := rangeToJson (some ranges) + -- Only the statement's dependencies: the proof is replaced by `sorry` in + -- the generated Challenge, so nothing the value names has to be carried. + let direct := info.type.getUsedConstants.filter (isFCLocal env) + let (_, ordered) := direct.foldl (fun p c => fcOrder env c p.1 p.2) + (({} : Std.HashSet Name), (#[] : Array Name)) + -- The equation compiler and `decide` leave constants like + -- `Finset.greedySidon.aux._proof_1` and `.match_1` in the closure. They + -- have no source range because they have no source: copying the parent + -- declaration's text regenerates them. Emit them separately so the + -- importer can check each one has an ancestor that is being copied, + -- rather than dropping them silently. + let mut deps := #[] + let mut generated := #[] + for d in ordered.filter (· != name) do + match ← findDeclarationRanges? d with + | some r => + deps := deps.push <| Json.mkObj [ + ("name", toJson d.toString), + ("module", toJson (moduleOf env d)), + ("range", rangeToJson (some r))] + | none => generated := generated.push (toJson d.toString) + -- The `@[category ...]` tag, spelled the way the attribute is written. + -- lean-eval displays open conjectures apart from its evaluation set, so + -- the importer needs to know which of the two a declaration is; the tag + -- lives in the environment extension, not in anything the text layer + -- could read reliably. + let category := match (ProblemAttributes.categoryExt.getState env).toList.find? + (·.declName == name) with + | some tag => Json.str <| match tag.category with + | .research .open => "research open" + | .research .solved => "research solved" + | .textbook => "textbook" + | .test => "test" + | .API => "API" + | none => Json.null + let payload := Json.mkObj [ + ("declaration", toJson decl), + ("name", toJson name.toString), + ("category", category), + ("range", rangeJson), + ("binders", toJson binders.toList), + ("answerTypes", toJson answerTypes.toList), + ("dependencies", toJson deps.toList), + ("generatedDependencies", toJson generated.toList)] + return payload + rangeToJson (ranges : Option DeclarationRanges) : Json := + match ranges with + | some r => Json.mkObj [ + ("startLine", toJson r.range.pos.line), + ("startColumn", toJson r.range.pos.column), + ("endLine", toJson r.range.endPos.line), + ("endColumn", toJson r.range.endPos.column)] + | none => Json.null diff --git a/comparator/adapter/compile_fc100_target.py b/comparator/adapter/compile_fc100_target.py new file mode 100644 index 0000000000..e7494e3aa3 --- /dev/null +++ b/comparator/adapter/compile_fc100_target.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +"""Compile every generated Challenge in one shared project at LeanEval pins. + +Each generated workspace pins the same Lean toolchain and Mathlib revision, +so building them separately would build Mathlib once per workspace. This +arranges them as modules of one Lake project instead — Mathlib is fetched and +built once for the whole set — which is what makes a hundred-workspace target +audit affordable, and is the arrangement the audit on +`google-deepmind/formal-conjectures#4951` used. + +Per workspace it copies `ChallengeDeps.lean` and `Challenge.lean` in as +`Deps_.lean` and `Chal_.lean`, rewriting the one import between them, +and builds each `Chal_` target separately so a failure is attributed to +its workspace rather than to the batch. `sorry` warnings are the workspaces +working; only errors fail a target. + +Usage: + python3 compile_fc100_target.py WORKSPACES_DIR --project DIR + [--report FILE] [--known-failures FILE] + +With `--known-failures`, exit non-zero unless the failing workspaces are +exactly the recorded `target`-stage ones. +""" + +import argparse +import pathlib +import re +import subprocess +import sys +import tomllib + +from leaneval_interface import lean_errors, dump_json +from limits import LEAN_TIMEOUT_SECONDS +from known_failures import gate, load_known_failures + + +def arrange_project(workspaces_dir, project_dir): + """Lay out the shared project; returns `{workspace_id: module_name}`. + + Workspace ids are already identifiers (the importer slugs them), so the + module names need no further encoding. + """ + workspaces_dir = pathlib.Path(workspaces_dir) + project_dir = pathlib.Path(project_dir) + project_dir.mkdir(parents=True, exist_ok=True) + workspaces = sorted( + entry for entry in workspaces_dir.iterdir() if (entry / "Challenge.lean").is_file() + ) + if not workspaces: + raise SystemExit(f"no generated workspaces under {workspaces_dir}") + + toolchain = (workspaces[0] / "lean-toolchain").read_text(encoding="utf-8") + mathlib = None + modules = {} + libs = [] + for workspace in workspaces: + this_toolchain = (workspace / "lean-toolchain").read_text(encoding="utf-8") + if this_toolchain != toolchain: + raise SystemExit( + f"{workspace.name} pins {this_toolchain.strip()}, but the set " + f"started with {toolchain.strip()}; one project needs one pin" + ) + lakefile = tomllib.loads( + (workspace / "lakefile.toml").read_text(encoding="utf-8") + ) + this_mathlib = next( + requirement for requirement in lakefile["require"] + if requirement["name"] == "mathlib" + ) + if mathlib is None: + mathlib = this_mathlib + elif this_mathlib != mathlib: + raise SystemExit(f"{workspace.name} pins a different Mathlib") + + challenge = (workspace / "Challenge.lean").read_text(encoding="utf-8") + deps_path = workspace / "ChallengeDeps.lean" + deps_module = f"Deps_{workspace.name}" + challenge_module = f"Chal_{workspace.name}" + if deps_path.is_file(): + (project_dir / f"{deps_module}.lean").write_text( + deps_path.read_text(encoding="utf-8"), encoding="utf-8" + ) + challenge = re.sub( + r"^import ChallengeDeps$", + f"import {deps_module}", + challenge, + flags=re.MULTILINE, + ) + libs.append(deps_module) + (project_dir / f"{challenge_module}.lean").write_text( + challenge, encoding="utf-8" + ) + libs.append(challenge_module) + modules[workspace.name] = challenge_module + + (project_dir / "lean-toolchain").write_text(toolchain, encoding="utf-8") + lakefile = ['name = "fc100_target"', "", "[leanOptions]", "autoImplicit = false"] + lakefile += [ + "", + "[[require]]", + 'name = "mathlib"', + f'git = "{mathlib["git"]}"', + f'rev = "{mathlib["rev"]}"', + ] + for lib in libs: + lakefile += ["", "[[lean_lib]]", f'name = "{lib}"'] + (project_dir / "lakefile.toml").write_text( + "\n".join(lakefile) + "\n", encoding="utf-8" + ) + return modules + + +def build(project_dir, modules): + """Build each Challenge target, attributing failures per workspace.""" + project_dir = pathlib.Path(project_dir) + for command in (["lake", "update"], ["lake", "exe", "cache", "get"]): + # These two fetch over the network, so they get the same bound as a + # build rather than none: a stalled fetch would otherwise sit until + # the job's own timeout. + completed = subprocess.run( + command, cwd=project_dir, timeout=LEAN_TIMEOUT_SECONDS + ) + if completed.returncode != 0: + raise SystemExit(f"{' '.join(command)} failed in {project_dir}") + results = [] + for workspace_id, module in sorted(modules.items()): + completed = subprocess.run( + ["lake", "build", module], + cwd=project_dir, + capture_output=True, + text=True, + timeout=LEAN_TIMEOUT_SECONDS, + ) + errors = lean_errors(completed.stdout + completed.stderr) + ok = completed.returncode == 0 and not errors + results.append( + { + "workspace": workspace_id, + "status": "ok" if ok else "target-failed", + # A failure with no `error:` line is lake dying, not Lean + # rejecting: keep its output rather than recording the word + # "build failed", which the report cannot act on. + **( + {} + if ok + else { + "reason": "\n".join(errors[:10]) + or "\n".join( + (completed.stdout + completed.stderr).splitlines()[-20:] + ) + or f"lake exited {completed.returncode} with no output" + } + ), + } + ) + print(f"{workspace_id}: {'ok' if ok else 'FAILED'}", flush=True) + return results + + +def main(argv): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("workspaces", help="directory of generated workspaces") + ap.add_argument("--project", required=True, help="shared project directory") + ap.add_argument("--report", default=None, help="write the JSON report here") + ap.add_argument( + "--known-failures", + default=None, + help="fail unless failing workspaces are exactly the recorded target ones", + ) + args = ap.parse_args(argv) + + modules = arrange_project(args.workspaces, args.project) + results = build(args.project, modules) + failed = {entry["workspace"] for entry in results if entry["status"] != "ok"} + report = { + "total": len(results), + "ok": len(results) - len(failed), + "failed": sorted(failed), + "results": results, + } + if args.report: + pathlib.Path(args.report).write_text( + dump_json(report), encoding="utf-8" + ) + print(f"{report['ok']}/{report['total']} Challenges compile at target pins") + + if args.known_failures: + # Known failures are recorded by declaration; workspaces are named by + # the slugged id, which the `workspace` field of each entry supplies. + # The loader is the source gate's: one validator, one reading of the + # ledger, and a target entry without a `workspace` is refused there + # rather than silently dropped here. + recorded = load_known_failures(args.known_failures) + if not gate(recorded, failed, "target", "workspace"): + return 1 + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/comparator/adapter/fc_leaneval_importer.py b/comparator/adapter/fc_leaneval_importer.py new file mode 100644 index 0000000000..4e168c939c --- /dev/null +++ b/comparator/adapter/fc_leaneval_importer.py @@ -0,0 +1,766 @@ +#!/usr/bin/env python3 +"""Map one Formal Conjectures declaration to a LeanEval module and manifest. + +This is the Formal Conjectures side of the ownership split in +`leanprover/lean-eval#536`, and it is the part this repository owns +permanently. It resolves a declaration against an exact Formal Conjectures +commit, asks Lean what the elaborated environment knows about it, copies the +declarations it depends on, types each `answer(sorry)` slot, and records where +all of that came from. + +What it produces is the pair defined in `comparator/adapter/leaneval_interface.py`: one +marked-up Mathlib-only Lean module, and one manifest carrying the FC source +commit and declaration id. Turning that pair into a Challenge / Solution / +Submission workspace is the pinned `leanprover/lean-eval-generator` binary's +job, not this module's; `leaneval_interface.build_request` is where the pair +becomes that binary's input. + +Nothing here writes a workspace file, names a workspace layout, or decides +which generated module imports which. If a change to this file would do one of +those, it belongs on the other side of the seam. + +Two source-boundary facts may live in `comparator/problems/.toml`, one +file per problem: which file is meant when two declare the same name, and an +explicit source-only proof dependency when Lean's opaque-value erasure makes +that dependency unrecoverable from the compiled environment. +""" + +import dataclasses +import pathlib +import re +import subprocess +import sys +import tempfile +import tomllib + +from limits import GIT_TIMEOUT_SECONDS, LEAN_TIMEOUT_SECONDS +from leaneval_interface import ( + CONTRACT_VERSION, + MarkedUpModule, + ProblemManifest, + ProducerRecord, + SourceRecord, + TargetRecord, + lean_errors, + sha256_text, +) +import fc_source +from fc_source import ( + DECL_START, + FC_SOURCE_TREES, + docstring_reference, + elaborator_facts, + file_scoped_preamble, + find_declaration, + flatten_declared_name, + hoist_answers, + importer_state, + localise_notation, + module_name, + module_source_path, + notation_blocks, + pins, + replace_proof_with_sorry, + slice_range, + strip_decorations, + strip_fc_attributes, + unwrap_answers, +) +# Derived on each read, like every other path here, so that a root which +# moves takes them with it rather than leaving a snapshot from import time. +def comparator_dir(): + return fc_source.ROOT / "comparator" + + +def manifest_dir(): + """Where the per-problem source-boundary files live.""" + return comparator_dir() / "problems" + +SOURCE_REPOSITORY = "https://github.com/google-deepmind/formal-conjectures" + +PERMITTED_AXIOMS = ("propext", "Quot.sound", "Classical.choice") + + +def _tools_file(): + """comparator/tools.toml is the one machine-readable source of pins, and + this module refuses to restate it.""" + with (comparator_dir() / "tools.toml").open("rb") as handle: + return tomllib.load(handle) + + +def target_pins(): + """LeanEval's pins, where a generated workspace is built and checked. + + They are not this repository's, and the importer neither chooses them nor + elaborates against them. It records them because a workspace that is + vendored into lean-eval has to be buildable there, and because a manifest + that carries both pin sets makes the gap between where the hole types were + read and where they will be used a readable fact rather than an assumption. + """ + target = _tools_file()["target"] + for key in ("lean_toolchain", "mathlib_revision", "mathlib_git"): + if not target.get(key): + raise SystemExit(f"comparator/tools.toml [target] has an empty `{key}`") + return TargetRecord( + lean_toolchain=target["lean_toolchain"], + mathlib_revision=target["mathlib_revision"], + mathlib_git=target["mathlib_git"], + ) + + +def producer_record(): + """What produced a generated artifact: this adapter, that generator, those pins. + + A workspace is immutable once written, so its record names the producers + as they were at generation time — the importer's own commit and whether + its files carried uncommitted edits, the pinned generator and its + contract version, and the target pins the workspace was generated for. + These are facts about this artifact, not assertions about what any + consumer uses forever. + """ + tools = _tools_file() + generator = tools.get("generator", {}) + target = tools.get("target", {}) + for table, key in (("generator", "repository"), ("generator", "rev")): + if not tools.get(table, {}).get(key): + raise SystemExit(f"comparator/tools.toml [{table}] has an empty `{key}`") + commit, dirty = importer_state() + return ProducerRecord( + importer_commit=commit, + importer_dirty=dirty, + generator_repository=generator["repository"], + generator_rev=generator["rev"], + contract_version=CONTRACT_VERSION, + target_lean_toolchain=target.get("lean_toolchain", ""), + target_mathlib_revision=target.get("mathlib_revision", ""), + target_comparator=target.get("comparator", ""), + target_lean4export=target.get("lean4export", ""), + ) + + +def explicit_copy_dependencies(problem_file): + """Source-only dependencies the compiled environment cannot retain. + + Lean erases the values of opaque theorem constants. If the source body + of a copied definition invokes such a theorem only to construct a proof + argument, the compiled definition refers to a generated `_proof_*` + constant and no longer records which source theorem produced it. The + marked-up module still copies source text, so that theorem must be named + explicitly and audibly in the problem manifest. + """ + records, generated = [], [] + for entry in problem_file.get("copy_dependencies", []): + if set(entry) != {"declaration", "module"}: + raise SystemExit( + "each `copy_dependencies` entry must contain exactly " + "`declaration` and `module`" + ) + relative = pathlib.Path(entry["module"]) + if ( + relative.is_absolute() + or ".." in relative.parts + or not relative.parts + or relative.parts[0] not in FC_SOURCE_TREES + ): + raise SystemExit( + f"copy dependency module must stay under a source tree: {relative}" + ) + path = fc_source.ROOT / relative + if not path.is_file() or relative.suffix != ".lean": + raise SystemExit(f"copy dependency module does not exist: {relative}") + module = module_name(relative) + facts = elaborator_facts(module, entry["declaration"]) + records.extend(facts.dependencies) + records.append( + { + "name": facts.name, + "module": module, + "range": facts.range, + } + ) + generated.extend(facts.generated_dependencies) + return records, generated + + +def merge_dependency_records(*groups): + """Deduplicate topologically ordered dependency records, fail closed.""" + merged, seen = [], {} + for group in groups: + for record in group: + name = record["name"] + if name in seen: + if seen[name] != record: + raise SystemExit(f"conflicting dependency records for {name}") + continue + seen[name] = record + merged.append(record) + return merged + + +def load_manifest(problem_id): + """Read the rare source-boundary facts Lean cannot select by itself. + + When two files declare the same name, nothing in the Lean environment says + which one was meant, so the importer refuses until a module is named. + `copy_dependencies` is the other exceptional field: it names a theorem + used only in copied source proof text when opaque-value erasure removes + the reference from Lean's compiled dependency graph. + + `leanprover/lean-eval` keeps one TOML per problem, and the reason is worth + copying: two pull requests adding different problems never touch the same + file. + + id the filename stem, and the workspace directory name + declaration the Lean name, which need not be unique across the repository + module the file declaring it, relative to the repository root + copy_dependencies exact declaration/module pairs to copy before the + environment-derived closure + + Anything Formal Conjectures already states stays where it is stated. The + source citation is read from the module docstring rather than copied here, + because a copy can drift from the docstring the repository maintains. An + ambiguous answer-slot type is a `--answer-type` argument: it is rare, and + a field no problem uses is a format nobody can check. + """ + path = manifest_dir() / f"{problem_id}.toml" + if not path.exists(): + return {} + with path.open("rb") as handle: + data = tomllib.load(handle) + if data.get("id") != problem_id: + raise SystemExit( + f"{path} declares id {data.get('id')!r}, but its filename says " + f"{problem_id!r}; the two must agree" + ) + if "declaration" not in data: + raise SystemExit(f"{path} has no `declaration` field") + unknown = sorted(set(data) - {"id", "declaration", "module", "copy_dependencies"}) + if unknown: + raise SystemExit( + f"{path} has keys nothing reads: {', '.join(unknown)}; a field no " + "code consumes is a record nobody can check" + ) + return data + + +def manifest_ids(): + return sorted(p.stem for p in manifest_dir().glob("*.toml")) + + +def closure_region( + dependencies, generated, declaration, opened_namespaces=(), target_name=None +): + """A declaration's FC-local closure, copied, needing Mathlib and nothing else. + + lean-eval vendors problems, so a generated Challenge cannot fetch this + repository at evaluation time and has to stand on Mathlib alone. That + rules out importing the problem's own module, and brings back the failure + modes an import does not have: file-scoped `open` and `variable` lost, + `local notation` unrecognised, a namespace swallowing what follows. + + So each declaration is emitted inside its own `section`, carrying the + preamble in force where it was written and reopening the namespace it was + written in. That is a construction, not a proof, and the only check that + covers every one of those failure modes at once is elaborating the + marked-up module, which `--verify` does. + """ + copied = [dep["name"] for dep in dependencies] + # The statement's own `match` and `proof` auxiliaries have the statement + # as their ancestor, and the statement is restated in the workspace, so + # re-elaborating it regenerates them; only an auxiliary of something not + # being copied at all is unreachable. + ancestors = copied + ([target_name] if target_name else []) + orphans = [ + name + for name in generated + if not any(name.startswith(parent + ".") for parent in ancestors) + ] + if orphans: + raise SystemExit( + f"{declaration}: {len(orphans)} elaborator-generated constant(s) " + "have no copied ancestor, so copying the closure would not " + f"reproduce them: {', '.join(orphans[:5])}" + ) + + # A constructor, a `where` auxiliary and a `_sparseCasesOn` all carry a + # source range inside the declaration that produces them, so copying them + # in their own right either duplicates a declaration or slices a fragment + # of one. `MonochromaticQuantumGraph.EdgeN.mk` covers line 88 of a + # structure spanning 83 to 93; `pmSumListAux._sparseCasesOn_1` has exactly + # its parent's range. Copying the outer declaration reproduces both. + def covered_by_another(dep): + inner = dep["range"] + for other in dependencies: + if other is dep or other["module"] != dep["module"]: + continue + outer = other["range"] + if outer is None or inner is None: + continue + if not ( + outer["startLine"] <= inner["startLine"] + and outer["endLine"] >= inner["endLine"] + ): + continue + same_span = ( + outer["startLine"] == inner["startLine"] + and outer["endLine"] == inner["endLine"] + ) + # A tie on the span is broken by name: the parent is the prefix. + if not same_span or len(other["name"]) < len(dep["name"]): + return True + return False + + subsumed = [dep["name"] for dep in dependencies if covered_by_another(dep)] + dependencies = [dep for dep in dependencies if dep["name"] not in subsumed] + + blocks, provenance, records = [], [], [] + # `open X` on a namespace nothing has declared yet is an error, and a + # copied preamble may open a namespace whose declaring block comes later + # in the copy, or never: with the problem's module no longer imported, + # only the copy itself can make a name exist. An empty namespace block + # up front is enough, and creating one that a later declaration fills is + # harmless. This covers the statement's own namespace stack and every + # namespace a copied preamble opens. + created = [] + # One read and preamble parse per dependency; the namespace pre-creation + # and the copied blocks below both consume the same tuple, so the two + # can never disagree about what a dependency's preamble says. + sliced = [] + for dep in dependencies: + if dep["range"] is None: + sliced.append(None) + continue + dep_path = module_source_path(dep["module"]) + dep_lines = dep_path.read_text(encoding="utf-8").split("\n") + dep_text, dep_start = slice_range(dep_lines, dep["range"]) + dep_preamble, dep_namespaces = file_scoped_preamble(dep_lines, dep_start) + sliced.append((dep_path, dep_text, dep_preamble, dep_namespaces)) + for entry in dep_preamble: + words = entry.split("\n")[0].split() + if not words or words[0] != "open": + continue + for word in words[1:]: + if word == "scoped": + continue + if not re.fullmatch(r"[\w.«»]+", word): + break + created.append(word) + created.extend( + ".".join(dep_namespaces[: depth + 1]) + for depth in range(len(dep_namespaces)) + ) + created.extend( + ".".join(opened_namespaces[: depth + 1]) + for depth in range(len(opened_namespaces)) + ) + seen_namespaces = set() + for namespace in created: + if namespace in seen_namespaces: + continue + seen_namespaces.add(namespace) + blocks.append(f"namespace {namespace}\nend {namespace}") + for dep, cut in zip(dependencies, sliced): + if cut is None: + raise SystemExit(f"{declaration}: {dep['name']} has no source range") + path, text, preamble, namespaces = cut + body = strip_fc_attributes(text).strip("\n") + if not body: + raise SystemExit(f"{declaration}: {dep['name']} sliced to nothing") + namespace = ".".join(namespaces) + chunk = [ + f"-- {dep['name']}, from {path.relative_to(fc_source.ROOT)}", + "noncomputable section", + ] + chunk += preamble + if namespace: + chunk.append(f"namespace {namespace}") + chunk += ["", body, ""] + if namespace: + chunk.append(f"end {namespace}") + chunk.append("end") + blocks.append("\n".join(chunk)) + provenance.append((dep["name"], body)) + records.append( + { + "declaration": dep["name"], + "module": dep["module"], + "path": str(path.relative_to(fc_source.ROOT)), + "range": dep["range"], + "content_sha256": sha256_text(body), + } + ) + + listing = "\n".join(f"* `{name}`" for name, _ in provenance) + return ( + "/-!\n" + f"The Formal Conjectures declarations `{declaration}` needs, copied so\n" + "that the statement requires Mathlib and nothing else. Dependencies\n" + "come before the declarations that use them:\n\n" + f"{listing}\n" + "-/\n\n" + "\n\n".join(blocks) + "\n" + ), provenance, records + + +def source_record( + declaration, + module, + source_path, + fc_rev, + copied_records, + original, + original_range, + mathlib_rev, +): + """Where the copied statement and its dependencies came from. + + lean-eval#536 requires the manifest to record the FC source commit and + declaration id, and it is the FC side that has to supply them: the + generator sees a Lean module, not a repository. They are also what makes + the importer's regeneration duty possible — when Formal Conjectures fixes + a misformalisation upstream, this record says which problem to redo. + + Each copied dependency is recorded as the slice that was actually + emitted — declaration, module, path, range and a digest of the copied + text — and the statement itself as its range and digest. The original + text is not carried: `pins` holds every recorded path to `commit`, so + range plus digest identify the bytes exactly, and a trusted-statement + record has no business shipping the source's proof body into a benchmark + workspace. + """ + blob = subprocess.run( + ["git", "-C", str(fc_source.ROOT), "rev-parse", f"{fc_rev}:{source_path}"], + capture_output=True, + text=True, + check=False, + timeout=GIT_TIMEOUT_SECONDS, + ) + # An empty digest beside a real commit reads as "recorded", so a failure + # here has to be one. `pins` already proved the path is tracked at this + # revision, which is why this is a refusal and not a fallback. + if blob.returncode != 0 or not blob.stdout.strip(): + raise SystemExit( + f"cannot resolve {source_path} at {fc_rev[:12]}: " + f"{blob.stderr.strip() or 'no object returned'}" + ) + return SourceRecord( + repository=SOURCE_REPOSITORY, + commit=fc_rev, + path=str(source_path), + blob_sha=blob.stdout.strip(), + module=module, + declaration=declaration, + copied_dependencies=tuple(copied_records), + original_range=dict(original_range), + original_sha256=sha256_text(original), + lean_toolchain=(fc_source.ROOT / "lean-toolchain").read_text(encoding="utf-8").strip(), + mathlib_revision=mathlib_rev, + ) + + +def locate_target(problem, module=None): + """Find the declaration and ask the elaborated environment about it. + + Returns the problem file, the qualified FC declaration, the source path, + the FC module name, the module docstring, and the elaborator facts with + the problem file's explicit copy dependencies merged in. + """ + problem_file, declaration, located = _resolve(problem, module) + path, _imports, module_doc, _body = located + fc_module = module_name(path.relative_to(fc_source.ROOT)) + facts = elaborator_facts(fc_module, declaration) + if facts.range is None: + raise SystemExit(f"{declaration}: no source range recorded") + explicit_dependencies, explicit_generated = explicit_copy_dependencies(problem_file) + facts = dataclasses.replace( + facts, + dependencies=tuple( + merge_dependency_records(explicit_dependencies, list(facts.dependencies)) + ), + generated_dependencies=tuple( + dict.fromkeys(explicit_generated + list(facts.generated_dependencies)) + ), + ) + return problem_file, declaration, path, fc_module, module_doc, facts + + +def restate(original, declaration, facts, answer_type=None): + """Turn the sliced declaration into the workspace statement. + + Strips decorations, replaces the proof with `sorry`, flattens a dotted + name to its slug, hoists every `answer(sorry)` into a hole and unwraps + the answers a solved statement carries. Returns the statement, the name + it declares, the name it declared in the source, and the holes. + """ + statement = strip_decorations(original) + statement = replace_proof_with_sorry(statement) + declared = None + for line in statement.split("\n"): + dm = DECL_START.match(line) + if dm: + declared = re.match(r"\s*([\w.«»]+)", line[dm.end() :]).group(1) + break + if declared is None: + raise SystemExit(f"{declaration}: no declaration line in the slice") + original_declared = declared + if "." in declared: + # The generator anchors on the declaration's last name component — + # its own sources always declare a plain identifier inside a + # namespace — so a dotted name like `erdos_100.variants.strong` + # would come out as `theorem strong`, and `parts.i` as `theorem i`. + # Restate the declaration under its slug instead: single identifier, + # still meaningful, and the provenance sidecar records the FC name. + declared, statement = flatten_declared_name(declared, statement) + statement, holes = hoist_answers( + statement, declared, list(facts.answer_types), answer_type + ) + # A `research solved` statement carries its answer rather than a `sorry` + # slot, so nothing above removed it and `answer(` would reach a workspace + # that cannot parse it. + statement = unwrap_answers(statement) + return statement, declared, original_declared, holes + + +def explicit_arguments(facts, declared): + """The explicit binders the Solution adapter applies by name.""" + args = [b["name"] for b in facts.binders if b["explicit"]] + bad = [a for a in args if "✝" in a or "._" in a] + if bad: + raise SystemExit( + f"{declared} has inaccessible explicit binders {bad}; the " + "Solution adapter cannot apply them by name" + ) + return args + + +def scope_region(namespaces_at_target, copied, preamble): + """The `open`s and file-scoped preamble the statement elaborates under.""" + # `open A`, then `open A.B`: opening the inner namespace does not open the + # outer one, and a statement may name siblings from either. With nothing + # copied there are no siblings to name and nothing declares the + # namespace, so an open would be an unresolvable orphan in a generated + # file that has no ChallengeDeps to import. + opens = ( + [ + f"open {'.'.join(namespaces_at_target[: i + 1])}" + for i in range(len(namespaces_at_target)) + ] + if copied + else [] + ) + return "\n".join(opens + localise_notation(preamble)) + + +def place_notations(dependencies, scope_text, statement, copied): + """Copy the FC notation commands the text needs, on the right side of the closure. + + Notation is text, not a constant: a statement or copied declaration + spelled with an FC-defined token needs the defining command copied too, + and the elaborated closure cannot say so. + """ + # Namespaces the module opens, at its scope and inside every copied + # block: a scoped notation can only have been in force where one of + # these opens it. + opened_for_notation = set() + for line in (dependencies + "\n" + scope_text).split("\n"): + words = line.split() + if words[:1] == ["open"]: + opened_for_notation.update(w for w in words[1:] if w != "scoped") + notations = notation_blocks( + [dependencies, scope_text, statement], opened_for_notation + ) + if not notations: + return dependencies, [] + # A notation whose right-hand side names a copied declaration must + # come after the block declaring it; every other notation comes + # first, because copied declarations may use its token textually. A + # single notation needing both would need interleaving; none does, + # and `--verify` is what says so. + copied_last_components = {name.rsplit(".", 1)[-1] for name, _ in copied} + before, after = [], [] + for block, _path in notations: + rhs = block.split("=>", 1)[-1] + names = set(re.findall(r"[\w«»'.]+", rhs)) + names |= {name.rsplit(".", 1)[-1] for name in names} + if names & copied_last_components: + after.append(block) + else: + before.append(block) + if before: + dependencies = "\n\n".join(before) + "\n\n" + dependencies + if after: + dependencies = dependencies + "\n\n" + "\n\n".join(after) + return dependencies, [path for _, path in notations] + + +def _resolve(problem, module=None): + """The problem file, declaration and source location one import works on.""" + problem_file = load_manifest(problem) + declaration = problem_file.get("declaration", problem) + # An argument given on the command line is explicit, so it wins over the + # problem file; the file is the durable record of the same choice. + module = module or problem_file.get("module") + located = find_declaration(declaration, module) + return problem_file, declaration, located + + +def statement_pair(problem): + """The `(module, declaration)` pair `import_problem` will ask the elaborator about.""" + _, declaration, (path, _imports, _doc, _body) = _resolve(problem) + return module_name(path.relative_to(fc_source.ROOT)), declaration + + +def import_problem(problem, answer_type=None, module=None): + """Map one declaration to a marked-up module and a manifest. + + Importing a closure out of a repository full of `sorry` is safe because + Comparator checks axioms. A solution closing the goal with a copied + statement reports `sorryAx`, which `permitted_axioms` does not allow. + """ + problem_file, declaration, path, fc_module, module_doc, facts = locate_target( + problem, module + ) + source_lines = path.read_text(encoding="utf-8").split("\n") + original, lo = slice_range(source_lines, facts.range) + preamble, namespaces_at_target = file_scoped_preamble(source_lines, lo) + dependencies, copied, copied_records = closure_region( + list(facts.dependencies), + list(facts.generated_dependencies), + declaration, + namespaces_at_target, + target_name=facts.name, + ) + statement, declared, original_declared, holes = restate( + original, declaration, facts, answer_type + ) + args = explicit_arguments(facts, declared) + scope_text = scope_region(namespaces_at_target, copied, preamble) + dependencies, notation_paths = place_notations( + dependencies, scope_text, statement, copied + ) + marked_up = MarkedUpModule( + dependencies=dependencies, + scope=scope_text, + holes="\n\n".join(hole.declaration() for hole in holes), + statement=statement, + dependency_declarations=tuple(copied), + ) + # The FC name, under the namespaces the source declared it in; the + # workspace statement may carry the flattened `declared` instead, and + # this is what ties the two together. + qualified = ".".join(namespaces_at_target + [original_declared]) + # Every file whose text reached the workspace is held to the one source + # revision: the statement's own file, each copied dependency's, and each + # copied notation command's. The toolchain and manifest are deliberately + # not among them. They are the environment the facts were read in, which + # the record states as an observation rather than as a claim about the + # pinned commit, and holding them to the merge base would make a + # toolchain bump — the change that most needs this check to run — the one + # change that cannot pass it. + read_paths = ( + [path.relative_to(fc_source.ROOT)] + + [record["path"] for record in copied_records] + + list(notation_paths) + ) + mathlib_rev, fc_rev = pins(read_paths) + source_url = docstring_reference(module_doc) + if not source_url: + print( + f"{declaration}: the module docstring has no *Reference:* link; " + "the provenance sidecar will carry no source_url", + file=sys.stderr, + ) + manifest = ProblemManifest( + # The default id is the qualified name: two modules declaring + # `conjecture` in different namespaces must not share a workspace. + id=problem_file.get("id", qualified), + theorem=declared, + qualified_theorem=qualified, + apply_arguments=tuple(args), + holes=tuple(holes), + permitted_axioms=PERMITTED_AXIOMS, + source=source_record( + qualified, + fc_module, + path.relative_to(fc_source.ROOT), + fc_rev, + copied_records, + original, + facts.range, + mathlib_rev, + ), + source_url=source_url, + category=facts.category or "", + ) + return marked_up, manifest + + +def elaborate(marked_up): + """Elaborate the marked-up module against this checkout's Mathlib. + + Copying a closure is a construction, and its failure modes are the ones + Lean sees and a reader does not: a lost `open`, an unrecognised + `local notation`, a namespace that no longer exists because nothing + declares it any more. Each of those is a clean build away from being + caught and a long review away from being spotted. + + The check runs here rather than on a generated workspace because the + module is what this repository hands over: an FC-side defect should fail + on the FC side, not in lean-eval's CI. It is offline, and it runs at this + repository's Lean and Mathlib, which are the manifest's `source` pins and + not its `target` pins: a module that elaborates here is not thereby known + to elaborate at LeanEval's toolchain, and only a build there settles that. + It checks elaboration, not a lakefile; a Comparator run exercises the + build. + """ + with tempfile.NamedTemporaryFile( + "w", suffix=".lean", delete=False, encoding="utf-8" + ) as handle: + handle.write(marked_up.render()) + combined = handle.name + try: + proc = subprocess.run( + ["lake", "env", "lean", combined], + capture_output=True, + text=True, + cwd=fc_source.ROOT, + check=False, + timeout=LEAN_TIMEOUT_SECONDS, + ) + finally: + pathlib.Path(combined).unlink(missing_ok=True) + output = (proc.stdout + proc.stderr).replace(combined, "Problem") + # Only errors fail the check. The target statement's proof is `sorry` by + # construction and each `answer(sorry)` hole is one the solver fills, so + # those warnings are the importer working. Linter warnings such as + # `unused variable` come from the copied source and say nothing about + # whether the copy is faithful. + errors = lean_errors(output) + if proc.returncode != 0 or errors: + raise SystemExit( + "the marked-up module does not elaborate:\n" + + "\n".join(errors or output.splitlines()[-10:]) + ) + return 0 + + +def validate(): + """Check every FC problem file resolves to exactly one declaration. + + Run this rather than discovering a stale `module` field when someone + imports the problem months later. + """ + bad = 0 + for problem_id in manifest_ids(): + try: + problem_file = load_manifest(problem_id) + declaration = problem_file["declaration"] + path, _i, _d, _b = find_declaration(declaration, problem_file.get("module")) + elaborator_facts(module_name(path.relative_to(fc_source.ROOT)), declaration) + except SystemExit as exc: + print(f"{problem_id}: {exc}", file=sys.stderr) + bad += 1 + continue + print(f"{problem_id}: {declaration} in {path.relative_to(fc_source.ROOT)}") + if bad: + print(f"{bad} problem file(s) do not resolve", file=sys.stderr) + return 1 if bad else 0 diff --git a/comparator/adapter/fc_source.py b/comparator/adapter/fc_source.py new file mode 100644 index 0000000000..de9258b766 --- /dev/null +++ b/comparator/adapter/fc_source.py @@ -0,0 +1,1095 @@ +#!/usr/bin/env python3 +"""Reading Formal Conjectures source. + +Everything here answers questions about this repository's own Lean files: +where a declaration is, which file-scoped directives were in force where it +was written, which FC-defined notation it uses, where its `answer(sorry)` +slots are and what types the elaborated environment gives them, and which +pins the text was read at. Nothing here knows what a workspace, a request or +a manifest is; `fc_leaneval_importer.py` assembles those from these answers. +""" + + +import dataclasses +import functools +import json +import pathlib +import re +import subprocess +import sys + +from limits import ( + BATCH_TIMEOUT_PER_PAIR_SECONDS, + GIT_TIMEOUT_SECONDS, + LEAN_TIMEOUT_SECONDS, +) + + +def slug(name): + """A Lake package name and directory name for a problem id. + + A Lake package name is an identifier, so the dots in a qualified + declaration cannot go into one verbatim. + """ + return re.sub(r"[^0-9A-Za-z_]", "_", name) + + +@dataclasses.dataclass(frozen=True) +class DefinitionHole: + """One `answer(sorry)` slot, hoisted into a definition the solver fills. + + `name` is the unqualified definition name as it appears in the module's + `holes` region; `type` is the type the elaborated environment reported for + the slot, which surface syntax does not carry. + """ + + name: str + type: str + + def declaration(self): + return f"noncomputable def {self.name} : {self.type} := sorry" + + +ROOT = pathlib.Path(__file__).resolve().parent.parent.parent + +# The trees this repository's own Lean lives in. `Extract.lean`'s `isFCLocal` +# tests the same set with a `FormalConjectures` module-name prefix, so a +# declaration Lean calls FC-local is one of these, and everything here that +# asks "is this ours" asks it the same way. +FC_SOURCE_TREES = ( + "FormalConjectures", + "FormalConjecturesForMathlib", + "FormalConjecturesUtil", +) + +# Problem statements live in the first tree; the other two are the support +# layer that statements are written against. +PROBLEM_TREE = FC_SOURCE_TREES[0] + + +def source_dirs(root): + """The trees problem statements live in, under `root`. + + A function rather than a constant because every cache below is keyed on + the root it read, and a module-level list derived from `ROOT` at import + would not follow a root that moved. + """ + return [root / PROBLEM_TREE] + +DECL_START = re.compile( + # `local notation` and `scoped notation` carry the modifier before the + # keyword. Without them here, Erdos 125's `local notation "A" => ...` typed + # as nothing and was dropped, and its statements lost the sets they name. + r"^(?:noncomputable\s+|private\s+|protected\s+|local\s+|scoped\s+)*" + r"(theorem|lemma|def|abbrev|structure|inductive|instance|notation)\s", +) + +KEEP_LOOSE = re.compile( + # `local notation`, `local macro` and friends scope to the file exactly + # like `open` does, and a statement that names what they define does not + # parse without them. `noncomputable section` is a section for the scope + # stack and a compilation mode for everything inside it. + r"^(?:(?:local|scoped)\s+)?" + r"(open|variable|universe|section|namespace|end|attribute|set_option" + r"|omit|include" + r"|notation|postfix|prefix|infixl|infixr|infix|macro|syntax|macro_rules)\b" + r"|^noncomputable section\b" +) + +@dataclasses.dataclass(frozen=True) +class FactsRecord: + """One declaration's elaborator facts, held to the payload the extractor emits. + + The fourth JSON boundary in the adapter, made as strict as the other + three: the provenance sidecar, the problem files and the failure ledger + all refuse keys nothing reads, and the extractor payload now does too, so + a drift between `comparator_facts` and this side fails at the seam + instead of surfacing as a missing default somewhere downstream. + """ + + declaration: str + name: str + category: str + range: dict + binders: tuple + answer_types: tuple + dependencies: tuple + generated_dependencies: tuple + + PAYLOAD_KEYS = frozenset( + { + "declaration", + "name", + "category", + "range", + "binders", + "answerTypes", + "dependencies", + "generatedDependencies", + } + ) + BINDER_KEYS = frozenset({"name", "explicit"}) + DEPENDENCY_KEYS = frozenset({"name", "module", "range"}) + + @classmethod + def from_payload(cls, payload, declaration): + unknown = sorted(set(payload) - cls.PAYLOAD_KEYS) + missing = sorted(cls.PAYLOAD_KEYS - set(payload)) + if unknown or missing: + raise SystemExit( + f"comparator_facts {declaration}: payload keys do not match the " + f"wire format (unknown: {unknown or 'none'}, " + f"missing: {missing or 'none'})" + ) + for binder in payload["binders"]: + if set(binder) != cls.BINDER_KEYS: + raise SystemExit( + f"comparator_facts {declaration}: malformed binder {binder}" + ) + for dep in payload["dependencies"]: + if set(dep) != cls.DEPENDENCY_KEYS: + raise SystemExit( + f"comparator_facts {declaration}: malformed dependency {dep}" + ) + return cls( + declaration=payload["declaration"], + name=payload["name"], + category=payload["category"], + range=payload["range"], + binders=tuple(payload["binders"]), + answer_types=tuple(payload["answerTypes"]), + dependencies=tuple(payload["dependencies"]), + generated_dependencies=tuple(payload["generatedDependencies"]), + ) + + +_FACTS_CACHE = {} + + +def prefetch_elaborator_facts(pairs): + """Fill the facts cache from one batched extractor run. + + `pairs` are `(module, declaration)` tuples. The Mathlib import dominates + a `comparator_facts` launch, so a batch pays it once for the whole set. + A pair the batch reports an error for is left out of the cache: the + caller's own `elaborator_facts` call re-runs it singly and fails with + exactly the message a single run always produced. + """ + wanted = [pair for pair in dict.fromkeys(pairs) if pair not in _FACTS_CACHE] + if not wanted: + return + try: + proc = subprocess.run( + ["lake", "exe", "comparator_facts", "--batch"], + input="".join( + json.dumps({"module": module, "declaration": declaration}) + "\n" + for module, declaration in wanted + ), + capture_output=True, + text=True, + cwd=ROOT, + timeout=LEAN_TIMEOUT_SECONDS + + BATCH_TIMEOUT_PER_PAIR_SECONDS * len(wanted), + ) + except subprocess.TimeoutExpired: + # The batch is an optimisation; the per-declaration path is the + # arbiter of what fails and how it is reported. It is still worth + # saying so: a collapsed batch re-runs the whole set one declaration + # at a time, which is otherwise visible only as a job that takes + # hours instead of minutes. + print( + f"comparator_facts --batch: no answer for {len(wanted)} pairs " + "within the timeout; falling back to one run per declaration", + file=sys.stderr, + ) + return + if proc.returncode != 0: + print( + f"comparator_facts --batch failed for {len(wanted)} pairs; " + "falling back to one run per declaration: " + f"{proc.stderr.strip().splitlines()[-1] if proc.stderr.strip() else 'no output'}", + file=sys.stderr, + ) + return + requested = set(wanted) + for line in proc.stdout.splitlines(): + if not line.startswith("{"): + # `lake` progress lines share stdout with the payload; anything + # non-JSON is theirs. Error entries are also left uncached, so + # the single re-run reproduces the exact message. + continue + entry = json.loads(line) + key = (entry["module"], entry["declaration"]) + if key not in requested: + raise SystemExit( + f"comparator_facts --batch answered for {key[1]} in {key[0]}, " + "which nothing asked about" + ) + if "facts" in entry: + _FACTS_CACHE[key] = entry["facts"] + + +def elaborator_facts(module, declaration): + """What the elaborated environment knows about a declaration. + + Runs `lake exe comparator_facts`, which imports the module and reports the + declaration's source range, its binders with real explicitness, and the + inferred type of each `answer(sorry)` slot. Every one of these used to be + reconstructed from text, and each reconstruction had failure modes the + elaborator does not. A batch import fills `_FACTS_CACHE` first, so a set + run pays the Mathlib import once. + """ + cached = _FACTS_CACHE.get((module, declaration)) + if cached is not None: + return FactsRecord.from_payload(cached, declaration) + try: + proc = subprocess.run( + ["lake", "exe", "comparator_facts", module, declaration], + capture_output=True, + text=True, + cwd=ROOT, + timeout=LEAN_TIMEOUT_SECONDS, + ) + except subprocess.TimeoutExpired: + raise SystemExit( + f"comparator_facts {declaration}: no answer within " + f"{LEAN_TIMEOUT_SECONDS // 60} minutes" + ) from None + if proc.returncode != 0: + raise SystemExit( + f"comparator_facts {declaration}: " + f"{proc.stderr.strip() or proc.stdout.strip()}" + ) + out = proc.stdout + if "{" not in out: + raise SystemExit(f"comparator_facts {declaration}: no JSON in output") + return FactsRecord.from_payload(json.loads(out[out.index("{") :]), declaration) + +def file_scoped_preamble(lines, start_line): + """Directives in force at `start_line`, and the namespace stack there. + + Lean scopes `open`, `variable`, `universe`, `set_option` and notation to + the file, so the marked-up module has to restate them; nothing in the + olean records them. A directive counts only if it precedes the statement + and its scope still encloses it. + """ + stack, preamble, depth = [], [], 0 + lines = lines[: start_line - 1] + index = 0 + while index < len(lines): + line = lines[index] + if depth == 0 and KEEP_LOOSE.match(line) and not line.rstrip().endswith(" in"): + kind = line.split()[0] + if kind == "noncomputable": + # `noncomputable section [name]` opens a section. + kind = "section" + parts = line.split(None, 2) + name = parts[2].strip() if len(parts) > 2 else None + else: + parts = line.split(None, 1) + name = parts[1].strip() if len(parts) > 1 else None + if kind in ("namespace", "section"): + stack.append((kind, name, line)) + elif kind == "end": + if stack and ( + stack[-1][1] == name or (name is None and stack[-1][0] == "section") + ): + stack.pop() + else: + # A `macro` or `notation` body may continue on indented + # lines; a single kept line would be broken syntax. + text = [line] + while index + 1 < len(lines) and ( + lines[index + 1][:1].isspace() and lines[index + 1].strip() + ): + index += 1 + text.append(lines[index]) + preamble.append(("\n".join(text), list(stack))) + code = line + if depth == 0: + # A `/-` inside a string or after `--` is not a comment opener; + # inside an open block comment the raw line is what counts. + code = re.sub(r'"(?:[^"\\]|\\.)*"', '""', code) + # `--` opens a line comment unless it is the tail of the + # doc-comment opener `/--`. + m = re.search(r"(? 1: + raise SystemExit( + f"{basename!r} is ambiguous: " + + ", ".join(str(h.relative_to(ROOT)) for h in hits) + + "; pass --module to choose one, or record the choice in " + "comparator/problems/.toml" + ) + return _read_source(hits[0]) + +def _read_source(path): + """Return (path, imports, module docstring, body after the licence header). + + The docstring is read but not removed. It sits below the imports rather + than at the top, so it is found by searching; the body deliberately still + contains it, because `strip_decorations` removes docstrings per + declaration and the generated files are compared byte for byte. + """ + original = path.read_text(encoding="utf-8") + text = re.sub(r"\A/-.*?-/\s*", "", original, flags=re.DOTALL) + found = re.search(r"/-!.*?-/", text, flags=re.DOTALL) + doc = found.group(0) if found else "" + imports = re.findall(r"^import\s+(\S+)", original, re.MULTILINE) + return path, imports, doc, text + +def strip_decorations(block_text): + """Remove the docstring, line comments and attributes from a declaration. + + These interleave. Erdos 918 puts a `--` formalisation note between its + docstring and its `@[category ...]` line, and one anchored pass each left + the attribute in place. `@[category research open, AMS 5]` then reached the + marked-up module, where the workspace has no such attribute, and Lean + parsed as far as the `open` inside it before giving up. + """ + # `open X in` binds to the declaration and has to survive, but it sits + # above the docstring, so stripping anchored at the start would stop dead + # on it. + prefix = "" + m = re.match(r"\A\s*(open\b[^\n]*\bin)\n", block_text) + if m: + prefix = m.group(1) + "\n" + block_text = block_text[m.end() :] + while True: + stripped = re.sub(r"\A\s*/--.*?-/\s*", "", block_text, flags=re.DOTALL) + stripped = re.sub(r"\A\s*--[^\n]*\n", "", stripped) + stripped = re.sub(r"\A\s*@\[[^\]]*\]\s*", "", stripped, flags=re.DOTALL) + if stripped == block_text: + return prefix + stripped + block_text = stripped + +# Attributes this repository defines. A generated workspace requires Mathlib +# and nothing else, so these have to go; everything else has to stay. +FC_ATTRIBUTES = ("category", "AMS", "formal_proof") + +def strip_fc_attributes(block_text): + """Remove this repository's own attributes from a copied declaration. + + Unlike `strip_decorations`, which clears every attribute off the target + statement, this keeps the rest. A dependency is copied to be elaborated, + not restated, and dropping `simp`, `reducible` or `instance` attributes + changes how the declarations after it in the same closure elaborate. + """ + + def replace(match): + inner = match.group(1) + # Nested brackets mean an argument this simple split would cut in + # half, so leave the whole attribute alone rather than mangle it. + if "[" in inner: + return match.group(0) + kept = [ + part.strip() + for part in inner.split(",") + if part.strip() and part.strip().split()[0] not in FC_ATTRIBUTES + ] + return f"@[{', '.join(kept)}]" if kept else "" + + text = re.sub(r"@\[([^\]]*)\]", replace, block_text) + # An attribute line that emptied out leaves a blank line behind; other + # blank lines are content — a multi-line string may contain one. + return re.sub(r"^[ \t]*\n", "", text, count=1) if text != block_text else text + +def split_module(module): + """The components of a dotted module name, respecting guillemet quoting. + + A guillemet-quoted component may itself contain dots — + `FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture` names the + directory `0912.2382` — so splitting on every dot decodes a path that + does not exist. This is the one place a module name is taken apart; + `module_name` is its inverse and a test holds the pair to that. + """ + parts = re.findall(r"«[^»]*»|[^.«»]+", module) + if ".".join(parts) != module: + raise SystemExit(f"{module!r} is not a well-formed module name") + return [p[1:-1] if p.startswith("«") else p for p in parts] + +def module_source_path(module): + """The file declaring a dotted Lean module name, undoing guillemets.""" + parts = split_module(module) + # Not `with_suffix`: a final component containing a dot would lose its + # tail to the suffix replacement. + path = ROOT.joinpath(*parts[:-1], parts[-1] + ".lean") + if not path.is_file(): + raise SystemExit(f"{module}: no source file at {path}") + return path + +def slice_range(lines, source_range): + """The source text a declaration range covers, and the line it starts on. + + `open X in` binds to the declaration below it but sits above what the + range covers in some toolchains, so it is pulled in when present. + """ + lo, hi = source_range["startLine"], source_range["endLine"] + # Every other field of the payload is held to the wire format; the range + # object is read positionally here, so it says so when it is malformed + # rather than slicing to the end of the line. + if "endColumn" not in source_range: + raise SystemExit(f"source range has no endColumn: {source_range}") + end_column = source_range["endColumn"] + while ( + lo > 1 + and lines[lo - 2].rstrip().endswith(" in") + and KEEP_LOOSE.match(lines[lo - 2]) + ): + lo -= 1 + sliced = lines[lo - 1 : hi] + if end_column is not None and sliced: + sliced = sliced[:-1] + [sliced[-1][:end_column]] + return "\n".join(sliced), lo + +NOTATION_COMMAND = re.compile( + r"^(?:@\[[^\]]*\]\s*)?(?:scoped\[[\w.«»]+\]\s+)?(?:scoped\s+)?" + r"(?:notation[0-9]*|postfix|prefix|infixl|infixr|infix)[:\s]" +) + +@functools.lru_cache(maxsize=4) +def fc_notation_commands(root): + """Every exportable notation command an FC module defines, with its token. + + A notation is not a constant, so the elaborated closure never reports it: + a statement written as `ℝ²` names `EuclideanSpace ℝ (Fin 2)` in the + environment and `ℝ²` only in its text. The copy carries the text, so the + commands that make such tokens parse have to be found at the text layer. + `local` notations are file-scoped at their origin and cannot be in force + in a problem file, so they are not candidates. + + Returns `[(tokens, command, scope, shared, path)]`, where `tokens` are + the command's distinctive string literals, `scope` is the namespace a + `scoped` command needs restated around it, and `path` is the defining + file relative to ROOT — a copied command's text is a read source input, + so the snapshot check needs to know where it came from. + """ + commands = [] + # Support trees first, then the problems tree. The order decides the + # order copied notation appears in a generated module, so it is fixed + # rather than incidental. + support = [tree for tree in FC_SOURCE_TREES if tree != PROBLEM_TREE] + for src in [root / tree for tree in support] + source_dirs(root): + for path in sorted(src.rglob("*.lean")): + lines = path.read_text(encoding="utf-8").split("\n") + for index, line in enumerate(lines): + if not NOTATION_COMMAND.match(line): + continue + text = [line] + follow = index + 1 + while follow < len(lines) and ( + lines[follow][:1].isspace() and lines[follow].strip() + ): + text.append(lines[follow]) + follow += 1 + command = "\n".join(text) + # A command's distinctive tokens decide whether a module + # uses it: `J(` or `α(` says something, the closing `")"` + # matches every text. So delimiter-only literals are dropped, + # while ASCII tokens with letters stay candidates — the old + # non-ASCII rule hid `J(`, `L(` and `e` from the shared + # library and their consumers failed to elaborate. + tokens = [ + token + for token in re.findall(r'"([^"]+)"', command) + if any(c.isalnum() or ord(c) > 127 for c in token) + ] + if not tokens: + continue + bracket = re.match(r"^(?:@\[[^\]]*\]\s*)?scoped\[([\w.«»]+)\]", line) + if bracket: + scope = bracket.group(1) + elif re.match(r"^scoped\s", line): + _, namespaces = file_scoped_preamble(lines, index + 1) + scope = ".".join(namespaces) + else: + scope = None + # A global notation in FormalConjecturesForMathlib or + # FormalConjecturesUtil is in force in every problem file, + # which imports both; one in a problem module is not, since + # problem files do not import each other, and the problem + # file's own notations travel with the preamble. + shared = src.name != PROBLEM_TREE + commands.append( + (tokens, command, scope, shared, path.relative_to(root)) + ) + return tuple(commands) + +NOTATION_FAMILY = re.compile(r"^(?:notation[0-9]*|postfix|prefix|infixl|infixr|infix)[:\s]") + +def localise_notation(preamble): + """File-scope the preamble's notation commands, with their set_options. + + The generator reconstructs each workspace file's context by re-extracting + these commands from the module, so a *global* notation ends up declared + both in `ChallengeDeps` and in the file importing it — two identical + notations, and every use becomes ambiguous. `local` keeps each copy to + its own file. A standalone `set_option quotPrecheck false` does not + survive that reconstruction, so a notation that needs it gets it + attached as part of its own command. + """ + precheck_off = any( + entry.split("\n")[0].strip() == "set_option quotPrecheck false" + for entry in preamble + ) + out = [] + for entry in preamble: + if NOTATION_FAMILY.match(entry): + entry = "local " + entry + if precheck_off and re.match(r"^(?:local\s+)?(?:notation|postfix|prefix|infix)", entry): + entry = "set_option quotPrecheck false in\n" + entry + out.append(entry) + return out + +def notation_blocks(module_texts, opened): + """The FC notation commands the module's text uses, as copyable blocks. + + A token match alone over-copies: `⊆` from a modal-logic module matched + every statement about sets. A scoped notation can only have been in + force in the source file if its namespace is among the file's opens, so + `opened` — the namespaces the module's scope and copied preambles open — + gates every scoped command. A global `notation` in a module nothing + imports was never in force either, but the corpus keeps global notation + in the problem file itself, which the preamble already carries, so + unscoped commands from other files are not candidates at all. + + Returns `[(block, path)]`: each copyable block with the file it was read + from, so the caller can hold that file to the source pin. + """ + combined = "\n".join(module_texts) + blocks, seen = [], set() + for tokens, command, scope, shared, path in fc_notation_commands(ROOT): + if scope: + if scope not in opened: + continue + elif not shared: + continue + if command in seen or command in combined: + continue + if not any(token in combined for token in tokens): + continue + seen.add(command) + # A plain `scoped` command needs its namespace restated around it; + # the bracket form carries its own scope. A global command becomes + # `local`: the generator re-extracts it into every file that needs + # it, and a module-crossing global would be declared twice. + if scope and not command.startswith("scoped["): + command = f"namespace {scope}\n{command}\nend {scope}" + elif not scope: + command = "local " + command + blocks.append((command, path)) + return blocks + +def flatten_declared_name(declared, statement): + """Restate a dotted declaration name as its slug, in the statement text. + + Returns `(new_name, new_statement)`. Only the declaring occurrence is + rewritten — a statement does not reference its own name — and the + rewrite is refused rather than guessed if the name cannot be found where + the declaration keyword put it. + """ + flattened = slug(declared) + lines = statement.split("\n") + for index, line in enumerate(lines): + match = DECL_START.match(line) + if not match: + continue + name = re.match(r"\s*([\w.«»]+)", line[match.end() :]) + if name and name.group(1) == declared: + start = match.end() + name.start(1) + lines[index] = line[:start] + flattened + line[start + len(declared) :] + return flattened, "\n".join(lines) + raise SystemExit(f"{declared}: cannot find the declaring occurrence to rename") + +def replace_proof_with_sorry(text): + """Cut the proof body after the top-level `:=`, keeping the statement. + + Only a `:=` at bracket depth zero can start the proof: an autoParam + binder default `(h : Fact P := by norm_num)` and a structure literal + `{ a := b }` both live inside brackets and are statement text. A tactic + proof is the first top-level `:= by`; a term proof leaves a bare + top-level `:=`, and with more than one of those the importer refuses, + as everywhere else it cannot decide. + """ + openers = "([{⟨" + closers = ")]}⟩" + depth = 0 + assigns = [] + i = 0 + while i < len(text): + i, _ = _next_code(text, i) + if i >= len(text): + break + char = text[i] + if char in openers: + depth += 1 + elif char in closers: + depth = max(depth - 1, 0) + elif depth == 0 and text.startswith(":=", i): + j = i + 2 + while j < len(text) and text[j].isspace(): + j += 1 + tactic = text.startswith("by", j) and ( + j + 2 >= len(text) + or not (text[j + 2].isalnum() or text[j + 2] in "_'") + ) + if tactic: + return text[: i].rstrip() + " := by\n sorry" + assigns.append(i) + i = j + continue + i += 1 + if len(assigns) > 1: + raise SystemExit( + "the declaration has a term-mode proof and more than one " + "top-level `:=`, so the start of the proof cannot be read off " + "the text" + ) + if assigns: + return text[: assigns[0]].rstrip() + " := by\n sorry" + return text.rstrip() + " := by\n sorry" + +def _next_code(text, i): + """The first index at or after `i` holding code, skipping comments and strings. + + Whenever the scan is at code, the lexical state is empty by construction, + so no state threads between calls. Returns `(index, unterminated)`, with + `index == len(text)` at the end and `unterminated` reporting a comment or + string still open there. + """ + block_depth = 0 + in_string = False + escaped = False + while i < len(text): + pair = text[i : i + 2] + if block_depth: + if pair == "/-": + block_depth += 1 + i += 2 + elif pair == "-/": + block_depth -= 1 + i += 2 + else: + i += 1 + continue + if in_string: + if escaped: + escaped = False + elif text[i] == "\\": + escaped = True + elif text[i] == '"': + in_string = False + i += 1 + continue + if pair == "/-": + block_depth = 1 + i += 2 + continue + if pair == "--": + newline = text.find("\n", i + 2) + i = len(text) if newline < 0 else newline + 1 + continue + if text[i] == '"': + in_string = True + i += 1 + continue + return i, False + return i, bool(block_depth or in_string) + + +def answer_spans(text): + """Return the source spans of syntactic `answer(...)` calls. + + This small lexer skips strings and nested line/block comments and balances + parentheses, so an answer term may itself contain parentheses. It is not a + Lean parser; malformed or unterminated syntax is refused. + """ + spans = [] + i = 0 + while i < len(text): + i, unterminated = _next_code(text, i) + if i >= len(text): + if unterminated: + raise SystemExit( + "unterminated comment or string while reading answers" + ) + break + if text.startswith("answer", i) and ( + i == 0 or not (text[i - 1].isalnum() or text[i - 1] in "_.'") + ): + j = i + len("answer") + while j < len(text) and text[j].isspace(): + j += 1 + if j < len(text) and text[j] == "(": + depth = 1 + k = j + 1 + while k < len(text) and depth: + k, _ = _next_code(text, k) + if k >= len(text): + break + if text[k] == "(": + depth += 1 + elif text[k] == ")": + depth -= 1 + k += 1 + if depth: + raise SystemExit("unterminated answer(...) term") + spans.append((i, k, text[j + 1 : k - 1])) + i = k + continue + i += 1 + return spans + + +def unwrap_answers(statement): + """Replace any surviving `answer(t)` with `(t)`. + + `answer` is this repository's own elaborator, so a Mathlib-only workspace + cannot parse it. `hoist_answers` removes the `answer(sorry)` slots by + turning them into definition holes; a slot that already carries its answer, + which is how a `research solved` statement is written, is left behind and + used to reach the marked-up module as literal text that does not parse. + + Unwrapping is faithful. In the default `postpone` mode the elaborator + elaborates the term and attaches an annotation + (`FormalConjecturesUtil/Answer.lean`), so `answer(t)` and `t` denote the + same term and only the annotation is lost. The annotation is what marks + which part of the statement was the question, and the manifest records + that instead. + """ + for start, end, argument in reversed(answer_spans(statement)): + statement = statement[:start] + f"({argument.strip()})" + statement[end:] + return statement + +def _ascribed_type(statement, start, end): + """The `T` of `(answer(sorry) : T)`, when the slot is written that way. + + A type ascription is the one place the surface syntax states a slot's + type at its position, and it matters because the elaborated environment + can lose the annotation for exactly this shape: the ascribed term is + applied or rewritten during elaboration and the metadata does not + survive into the stored statement type. + """ + before = statement[:start].rstrip() + if not before.endswith("("): + return None + index = end + while index < len(statement) and statement[index].isspace(): + index += 1 + if index >= len(statement) or statement[index] != ":": + return None + index += 1 + depth, cursor = 1, index + while cursor < len(statement): + char = statement[cursor] + if char == "(": + depth += 1 + elif char == ")": + depth -= 1 + if depth == 0: + ascribed = statement[index:cursor].strip() + return ascribed or None + cursor += 1 + return None + +def hoist_answers(statement, basename, slot_types, override=None): + """Replace each `answer(sorry)` with a named definition hole. + + A slot written `(answer(sorry) : T)` states its own type at its own + position, and that reading wins. For the rest, the types come from the + elaborated environment, where the `answer` elaborator ran with the + expected type in hand; the old surface-syntax guess (an `↔` beside the + slot means `Prop`) survives only as the `--answer-type` override. Unascribed slots of differing types are + refused: the environment reports the types as a set, and matching them + to positions would be a guess. + """ + holes = [] + calls = answer_spans(statement) + selected = [call for call in calls if call[2].strip() == "sorry"] + count = len(selected) + if count == 0: + return statement, holes + types = [None] * count + if override: + types = [override] * count + else: + remaining_env = list(slot_types) + for i, (start, end, _argument) in enumerate(selected): + ascribed = _ascribed_type(statement, start, end) + if ascribed is not None: + types[i] = ascribed + # The environment may have reported this slot too; retire one + # matching entry so the counting below stays honest. + if ascribed in remaining_env: + remaining_env.remove(ascribed) + remaining = [i for i in range(count) if types[i] is None] + # Under the default `alwaysTrue` setting, the `answer` elaborator + # erases a slot to `True` if and only if its expected type is `Prop` + # (FormalConjecturesUtil/Answer.lean). So a slot the environment + # carries no annotation for is a `Prop` slot by the elaborator's own + # rule, not by guesswork, and no postpone build is needed. + missing = len(remaining) - len(remaining_env) + if not remaining: + # Every slot stated its own type. An environment entry that + # survived is one of those same slots spelled the way the + # elaborator prints types, not an extra slot to place. + pass + elif missing == len(remaining): + for i in remaining: + types[i] = "Prop" + elif missing == 0 and remaining and len(set(remaining_env)) == 1: + for i in remaining: + types[i] = remaining_env[0] + elif missing == 0: + raise SystemExit( + f"{basename} has {len(remaining)} answer slots of differing " + f"types {remaining_env}; pass --answer-type" + ) + else: + # Some slots are Prop and some are not: which positions are which + # cannot be read off an unordered set, so refuse rather than + # assign. + raise SystemExit( + f"{basename}: {missing} Prop slot(s) and {len(remaining_env)} " + f"typed slot(s) {remaining_env} cannot be matched to " + "positions; pass --answer-type" + ) + replacements = [] + for i, (start, end, _argument) in enumerate(selected): + name = f"{basename}_answer" if count == 1 else f"{basename}_answer_{i + 1}" + holes.append(DefinitionHole(name=name, type=types[i])) + replacements.append((start, end, name)) + for start, end, name in reversed(replacements): + statement = statement[:start] + name + statement[end:] + return statement, holes + +@functools.lru_cache(maxsize=4) +def _base_pins(root): + """The Mathlib revision and the FC merge-base, invariant for one run. + + Only the per-path dirty check in `pins` varies between calls, so the + subprocess and manifest parse run once per batch rather than once per + declaration. + """ + manifest = json.loads((ROOT / "lake-manifest.json").read_text()) + mathlib_rev = next(p["rev"] for p in manifest["packages"] if p["name"] == "mathlib") + merge_base = subprocess.run( + ["git", "-C", str(ROOT), "merge-base", "HEAD", "origin/main"], + capture_output=True, + text=True, + timeout=GIT_TIMEOUT_SECONDS, + ) + if merge_base.returncode != 0 or not merge_base.stdout.strip(): + raise SystemExit("cannot resolve the Formal Conjectures source revision") + return mathlib_rev, merge_base.stdout.strip() + + +def pins(source_paths=None): + """Revisions the workspace's own build can actually fetch. + + The FC pin must be reachable from the upstream repository the lakefile + names, so it is the merge-base with `origin/main`, not HEAD: a local + branch commit would generate a workspace whose build fails at fetch time. + The importer stops if any file it read differs from that revision — + `source_paths` is every file whose text reached the workspace, not just + the statement's own — so the record names one revision and the copied + text all comes from it. A path the revision does not track fails too: + `git diff` is silent about untracked files, so tracking is checked first. + """ + mathlib_rev, fc_rev = _base_pins(ROOT) + if source_paths is not None: + if isinstance(source_paths, (str, pathlib.Path)): + source_paths = [source_paths] + paths = sorted({str(path) for path in source_paths}) + tracked = subprocess.run( + ["git", "-C", str(ROOT), "ls-tree", "-r", "--name-only", fc_rev, "--"] + + paths, + capture_output=True, + text=True, + timeout=GIT_TIMEOUT_SECONDS, + ) + if tracked.returncode != 0: + raise SystemExit(f"cannot list {fc_rev[:12]}: {tracked.stderr.strip()}") + missing = sorted(set(paths) - set(tracked.stdout.split("\n"))) + if missing: + raise SystemExit( + f"{', '.join(missing)}: not tracked at pinned revision " + f"{fc_rev[:12]}; land the source on upstream main before " + "generating" + ) + comparison = subprocess.run( + ["git", "-C", str(ROOT), "diff", "--quiet", fc_rev, "--"] + paths, + timeout=GIT_TIMEOUT_SECONDS, + ) + if comparison.returncode not in (0, 1): + raise SystemExit(f"cannot compare {', '.join(paths)} with {fc_rev[:12]}") + if comparison.returncode == 1: + changed = subprocess.run( + ["git", "-C", str(ROOT), "diff", "--name-only", fc_rev, "--"] + paths, + capture_output=True, + text=True, + timeout=GIT_TIMEOUT_SECONDS, + ) + raise SystemExit( + f"{changed.stdout.strip() or ', '.join(paths)} differs from " + f"pinned revision {fc_rev[:12]}; land the source on upstream " + "main before generating" + ) + return mathlib_rev, fc_rev + + +def importer_state(): + """The commit this importer ran as, and whether its own files were edited. + + The generated record separates two questions the source pin cannot answer: + which adapter produced the artifact (HEAD, not the merge-base — the + adapter itself is allowed to be branch work), and whether that adapter was + running with uncommitted edits under `comparator/`. + """ + head = subprocess.run( + ["git", "-C", str(ROOT), "rev-parse", "HEAD"], + capture_output=True, + text=True, + timeout=GIT_TIMEOUT_SECONDS, + ) + if head.returncode != 0 or not head.stdout.strip(): + raise SystemExit("cannot resolve the importer's own commit") + status = subprocess.run( + ["git", "-C", str(ROOT), "status", "--porcelain", "--", "comparator"], + capture_output=True, + text=True, + timeout=GIT_TIMEOUT_SECONDS, + ) + # Empty output means a clean tree, and a failed command also produces + # empty output. Reporting the reassuring answer for both would make the + # field worth less than not recording it. + if status.returncode != 0: + raise SystemExit( + f"cannot tell whether the importer is dirty: " + f"{status.stderr.strip() or 'git status failed'}" + ) + return head.stdout.strip(), bool(status.stdout.strip()) diff --git a/comparator/adapter/known_failures.py b/comparator/adapter/known_failures.py new file mode 100644 index 0000000000..5204730b30 --- /dev/null +++ b/comparator/adapter/known_failures.py @@ -0,0 +1,93 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""The known-failures ledger: `comparator/known_failures.toml`, its loader and its gate. + +Both stages read the ledger — the source-side set run and the target-side +compile — and each matches it exactly: an unexpected failure and a silently +fixed one both fail. Format, loader and comparison live here so the two +stages cannot drift into disagreeing about what the ledger means, and so +neither command has to import the other to read it. +""" + +import sys +import tomllib + +KNOWN_KEYS = frozenset({"declaration", "stage", "reason", "workspace"}) + + +def load_known_failures(path): + """The recorded failures, `{declaration: {stage, reason}}`. + + Strict like every other boundary here: a key nothing reads is refused + rather than carried, and a declaration recorded twice is refused rather + than last-one-wins — a shadowed entry would quietly defeat the exact + match the gates promise. + """ + with open(path, "rb") as handle: + data = tomllib.load(handle) + failures = {} + for entry in data.get("failure", []): + for field in ("declaration", "stage", "reason"): + if field not in entry: + raise SystemExit(f"{path}: a failure entry has no `{field}`") + unknown = sorted(set(entry) - KNOWN_KEYS) + if unknown: + raise SystemExit( + f"{path}: {entry['declaration']} has unknown keys: " + f"{', '.join(unknown)}" + ) + if entry["stage"] not in ("source", "target"): + raise SystemExit( + f"{path}: {entry['declaration']} has stage {entry['stage']!r}; " + "expected source or target" + ) + if entry["stage"] == "target" and "workspace" not in entry: + raise SystemExit( + f"{path}: {entry['declaration']} is a target failure without a " + "`workspace`; the target gate matches by workspace id" + ) + if entry["declaration"] in failures: + raise SystemExit( + f"{path}: {entry['declaration']} is recorded twice" + ) + failures[entry["declaration"]] = entry + return failures + + +def expected_failures(recorded, stage, key): + """The names the ledger expects to fail at `stage`, read from `key`.""" + return {entry[key] for entry in recorded.values() if entry["stage"] == stage} + + +def gate(recorded, actual, stage, key): + """Whether the observed failures are exactly the recorded ones. + + Both directions fail. An unexpected failure is the obvious one; a + recorded failure that no longer happens is the one a gate without this + check would never mention, and a ledger nobody prunes stops describing + the run it guards. + """ + expected = expected_failures(recorded, stage, key) + unexpected = sorted(set(actual) - expected) + fixed = sorted(expected - set(actual)) + for name in unexpected: + print(f"unexpected {stage} failure: {name}", file=sys.stderr) + for name in fixed: + print( + f"{name} is recorded as a known {stage} failure but did not fail; " + "remove it from the record", + file=sys.stderr, + ) + return not (unexpected or fixed) diff --git a/comparator/adapter/leaneval_generator_cli.py b/comparator/adapter/leaneval_generator_cli.py new file mode 100644 index 0000000000..3f335aa9f7 --- /dev/null +++ b/comparator/adapter/leaneval_generator_cli.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Run the pinned `lean-eval-generator` binary on a schema-version-1 request. + +`leanprover/lean-eval#536` extracts lean-eval's generator core into +`leanprover/lean-eval-generator`, a deterministic Lean CLI: one JSON request +on stdin, one JSON response on stdout, diagnostics on stderr. This module is +the plumbing that runs it and the context directory it expects; everything +the request and response mean lives in `comparator/adapter/leaneval_interface.py`, and +the pinned revision lives in `comparator/tools.toml` under `[generator]`. + +The binary is found through `LEAN_EVAL_GENERATOR_BIN` or `PATH`. Building it +is cheap — the package depends on nothing — so CI clones the pinned revision +and runs `lake build`; `comparator/README.md` shows the same for a local run. + +The context root exists because the schema-version-1 contract still resolves two things +from a benchmark checkout rather than from the request: the module source +(which must byte-match the request's `moduleContent`) and each declaration's +span from compiled `.ilean` metadata. This consumer is not a benchmark +checkout, so it materialises a minimal one: the rendered module at +`/.lean`, and a synthesised `.ilean` carrying exactly the spans +`build_problem` computed. It can do that honestly because it rendered the +module; nothing is guessed. +""" + +import json +import os +import pathlib +import shutil +import subprocess + +from limits import LEAN_TIMEOUT_SECONDS +from leaneval_interface import parse_response + +BINARY_ENV = "LEAN_EVAL_GENERATOR_BIN" +BINARY_NAME = "lean-eval-generator" + + +def binary(): + """The pinned generator executable, from the environment or PATH.""" + named = os.environ.get(BINARY_ENV) + if named: + path = pathlib.Path(named) + if not path.is_file(): + raise SystemExit(f"{BINARY_ENV}={named}: no such file") + return str(path) + found = shutil.which(BINARY_NAME) + if found: + return found + raise SystemExit( + f"no `{BINARY_NAME}` on PATH and {BINARY_ENV} is not set; build the " + "revision pinned under [generator] in comparator/tools.toml and " + "point either at it" + ) + + +def context_files(problems): + """The minimal benchmark checkout for a request, as `{path: content}`. + + `problems` are `(problem, ilean_decls)` pairs from `build_problem`. Each + module lands at `.lean` — the byte-match the generator enforces + against `moduleContent` — and its spans at the `.ilean` path the + generator reads. This is the one statement of that layout; whoever puts + the files on disk decides where the root lives. + """ + files = {} + for problem, ilean in problems: + module = problem["moduleName"] + files[f"{module}.lean"] = problem["moduleContent"] + files[f".lake/build/lib/lean/{module}.ilean"] = ( + json.dumps({"version": 1, "module": module, "decls": ilean}) + "\n" + ) + return files + + +def generate(request_text, cwd=None, expected_ids=None): + """The generator's verified file maps for one request. + + Takes the request as its exact serialised bytes, not a dict: the string + piped to the binary is the same string `--emit-import` writes and the + sidecar digests, so "the exact bytes crossing the seam" is a fact rather + than a paraphrase. The request's `contextRoot` stays the relative + `context`, resolved against `cwd`. With `expected_ids`, the response must + cover exactly those workspaces. Returns `{problem_id: {path: content}}`. + """ + try: + proc = subprocess.run( + [binary()], + input=request_text, + capture_output=True, + text=True, + cwd=cwd, + # The generator is deterministic and does no I/O beyond the + # context root, so a run that has not answered by now is stuck. + timeout=LEAN_TIMEOUT_SECONDS, + ) + except subprocess.TimeoutExpired: + raise SystemExit( + "lean-eval-generator did not answer within " + f"{LEAN_TIMEOUT_SECONDS // 60} minutes" + ) from None + if proc.returncode != 0: + raise SystemExit( + f"lean-eval-generator failed:\n{proc.stderr.strip() or proc.stdout.strip()}" + ) + return parse_response(proc.stdout, expected_ids=expected_ids) diff --git a/comparator/adapter/leaneval_interface.py b/comparator/adapter/leaneval_interface.py new file mode 100644 index 0000000000..81b6dcb412 --- /dev/null +++ b/comparator/adapter/leaneval_interface.py @@ -0,0 +1,793 @@ +#!/usr/bin/env python3 +"""The one interface between the Formal Conjectures importer and the generator. + +`leanprover/lean-eval#536` splits this work in two, and the generator half now +exists: `leanprover/lean-eval-generator` is a deterministic Lean CLI with a +versioned JSON contract, pinned in `comparator/tools.toml`. The consumer sends +one request on stdin — target pins, templates, and per problem a Lean module +with resolved hole ranges — and receives the complete workspace file map with +a SHA-256 digest per file. The Formal Conjectures side owns an importer that +maps FC declarations and metadata to that request. The FC importer does not +fork the generation logic. + +This module is that seam, and nothing else. It holds the values that cross it +and the code that turns them into contract JSON: + + MarkedUpModule one Mathlib-only Lean module, in four internal regions + ProblemManifest the facts about the problem that the module's text does + not carry, including the FC source commit and the FC + declaration id; written beside the generated workspace + as `fc-provenance.json`, because the schema-version-1 contract has no + provenance fields of its own + build_request (module, manifest) pairs -> the schema-version-1 request object + parse_response response text -> file maps, digests checked + +`comparator/adapter/fc_leaneval_importer.py` produces the pairs. +`comparator/adapter/leaneval_generator_cli.py` runs the pinned binary. Nothing on the FC +side decides a workspace file's contents any more. + +## Why one module rather than a bag of strings + +The generator's job includes the import and scope fidelity work from +lean-eval#531: deciding which generated file imports which, and where the +file-scoped `open`, `variable` and notation have to be restated so that the +same statement text elaborates in Challenge, Submission and Solution alike. +That decision belongs to the generator, so the importer must not pre-split the +source. It emits one module that elaborates on its own against Mathlib, and +the generator slices it by the hole ranges the request carries. + +Emitting one module also gives the importer a check it could not otherwise +have: the module it is about to hand over is exactly the text it can elaborate +locally (`--verify`), so a copied closure that has lost an `open` fails on the +FC side rather than in lean-eval's CI. For the same reason the module carries +no `@[eval_problem]` markers: that attribute does not exist outside lean-eval, +and the ranges in the request already say where the holes are. + +The regions, in the order they are rendered: + + dependencies the FC-local closure of the statement, copied, Mathlib-only + scope the `open` and file-scoped directives the statement needs + holes one `noncomputable def : := sorry` per + `answer(sorry)` slot the importer hoisted + statement the target statement, its proof replaced by `sorry` + +The regions are an internal structure. What crosses the seam is the rendered +module inside the request, byte for byte. +""" + +import dataclasses +import hashlib +import json +import re + +from fc_source import DefinitionHole, slug + +REGIONS = ("dependencies", "scope", "holes", "statement") + +# Faithful for this corpus, not a convenience: every problem file under +# FormalConjectures/ imports exactly `FormalConjecturesUtil`, which +# `public import`s all of Mathlib, so each statement already elaborates +# under the full library and no file carries a narrow or third-party +# import this header could widen away. The FC-local layer — the one part +# of the source environment this header drops — travels as the copied +# closure, and `--verify` elaborates under exactly this header. The +# remaining source-versus-target gap is the Mathlib revision, which the +# sidecar records on both sides and the cross-pin CI job builds. +MODULE_PREAMBLE = "import Mathlib\n" + +MANIFEST_SCHEMA_VERSION = 1 + + +def lean_errors(output): + """The error lines of a Lean build's output. + + Only errors fail a check: `sorry` warnings are the importer working, and + linter warnings come from copied source. The predicate lives here because + the source-side elaboration gate and the target-side compile gate must + agree on what a failing build is. + """ + return [line for line in output.splitlines() if "error:" in line] + + +def sha256_text(text): + """The digest the generator response uses: SHA-256 of the UTF-8 bytes.""" + return hashlib.sha256(text.encode("utf-8")).hexdigest() + + +def dump_json(obj, sort_keys=False): + """The one JSON serialisation every artifact here uses: readable, UTF-8, newline-terminated.""" + return json.dumps(obj, indent=2, ensure_ascii=False, sort_keys=sort_keys) + "\n" + +# The generator's frozen wire format; `schemas/request-v1.schema.json` and +# `response-v1.schema.json` in the pinned revision are normative. +CONTRACT_VERSION = 1 + + +@dataclasses.dataclass(frozen=True) +class SourceRecord: + """Where the marked-up module's text came from. + + lean-eval#536 requires that each manifest record the FC source commit and + declaration id. Neither is recoverable from the Lean text, and neither is + something the generator can supply: the generator sees a module, not a + repository. So they cross the seam here, and the generator's only duty is + to carry them into the workspace unaltered. + + `lean_toolchain` and `mathlib_revision` are Formal Conjectures' own, and + are not the pins the workspace is built with. They are here because the + hole types in the manifest were read from an environment elaborated at + them, so a reader comparing them with `TargetRecord` can see whether the + types were read where they will be used. + + `copied_dependencies` holds one record per emitted slice — declaration, + module, path, source range and a digest of the copied text — and the + statement itself travels as `original_range` plus `original_sha256` + rather than as text: with every recorded path held to `commit`, range and + digest identify the bytes exactly, and the record never carries the + source's proof body into a workspace. + """ + + repository: str + commit: str + path: str + blob_sha: str + module: str + declaration: str + copied_dependencies: tuple + original_range: dict + original_sha256: str + lean_toolchain: str + mathlib_revision: str + + +@dataclasses.dataclass(frozen=True) +class ProducerRecord: + """What produced one generated workspace, as it was at generation time. + + Immutable output deserves a record of its producers: the importer commit + (and whether `comparator/` carried uncommitted edits), the pinned + generator with its contract version, and the target pins the workspace + was generated for. These describe this artifact; the consumer's live + regime stays the consumer's, and `TargetRecord` remains the request-side + statement of it. + """ + + importer_commit: str + importer_dirty: bool + generator_repository: str + generator_rev: str + contract_version: int + target_lean_toolchain: str + target_mathlib_revision: str + target_comparator: str + target_lean4export: str + + def to_json_object(self): + return { + "importer": { + "commit": self.importer_commit, + "dirty": self.importer_dirty, + }, + "generator": { + "repository": self.generator_repository, + "rev": self.generator_rev, + "contract_version": self.contract_version, + }, + "target": { + "lean_toolchain": self.target_lean_toolchain, + "mathlib_revision": self.target_mathlib_revision, + "comparator": self.target_comparator, + "lean4export": self.target_lean4export, + }, + } + + @classmethod + def from_json_object(cls, payload): + sections = { + "importer": {"commit", "dirty"}, + "generator": {"repository", "rev", "contract_version"}, + "target": { + "lean_toolchain", + "mathlib_revision", + "comparator", + "lean4export", + }, + } + unknown = sorted(set(payload) - set(sections)) + if unknown: + raise SystemExit(f"producer record has unknown keys: {', '.join(unknown)}") + for section, keys in sections.items(): + entries = payload.get(section, {}) + unknown = sorted(set(entries) - keys) + if unknown: + raise SystemExit( + f"producer {section} has unknown keys: {', '.join(unknown)}" + ) + missing = sorted( + f"{section}.{key}" + for section, keys in sections.items() + for key in keys + if key not in payload.get(section, {}) + ) + if missing: + raise SystemExit( + f"producer record has no {', '.join(missing)}" + ) + importer = payload["importer"] + generator = payload["generator"] + target = payload["target"] + return cls( + importer_commit=importer["commit"], + importer_dirty=bool(importer["dirty"]), + generator_repository=generator["repository"], + generator_rev=generator["rev"], + contract_version=generator["contract_version"], + target_lean_toolchain=target["lean_toolchain"], + target_mathlib_revision=target["mathlib_revision"], + target_comparator=target["comparator"], + target_lean4export=target["lean4export"], + ) + + +@dataclasses.dataclass(frozen=True) +class TargetRecord: + """The pins a generated workspace is built and checked with. + + These belong to whoever consumes the generator: lean-eval#536 says + LeanEval "remains the trusted statement repository and supplies the pin + regime and CI". So they are an argument to `generate`, not a field of the + manifest — a manifest carrying them would be Formal Conjectures asserting + another repository's regime, and would go stale the moment that repository + bumped anything, with nothing here to notice. + + Formal Conjectures keeps the full pin set under `[target]` in + `comparator/tools.toml`; this record carries only the two fields the schema-version-1 + request consumes. The comparator and lean4export pins are read from the + TOML directly by the CI job that runs them. + """ + + lean_toolchain: str + mathlib_revision: str + mathlib_git: str = "https://github.com/leanprover-community/mathlib4.git" + + +@dataclasses.dataclass(frozen=True) +class ImportPolicy: + """LeanEval-side catalog policy, stated explicitly per import run. + + Group, lifecycle status, visibility, statement revision, submitter and + tags are the consumer's decisions, not source facts; the schema-version-1 + request happens to require them inline, so the command constructs a + policy and hands it in rather than this module hard-coding one. An empty + `group` means "derive from the category" via `CATEGORY_GROUPS`. + """ + + group: str + status: str + visible: bool + statement_revision: int + submitter: str + tags: tuple + + +@dataclasses.dataclass(frozen=True) +class ProblemManifest: + """What the marked-up module's text does not say. + + `theorem` is the statement's own unqualified name, which the generator + needs for the Solution adapter, and `qualified_theorem` is that name under + the namespace the scope region reopens, which is what Comparator checks. + `apply_arguments` are the statement's explicit declaration parameters, in + order: the Solution adapter applies them by name, and `∀` binders in the + conclusion are not among them. + """ + + id: str + theorem: str + qualified_theorem: str + apply_arguments: tuple + holes: tuple + permitted_axioms: tuple + source: SourceRecord + source_url: str = "" + # The `@[category ...]` tag as the source spells it: `research open`, + # `research solved`, `textbook` or `test`. lean-eval keeps open + # conjectures out of its evaluation set, so which group a problem joins + # is decided by this and nothing else; recording the raw tag rather than + # the mapped group keeps the mapping in one place, beside the request. + category: str = "" + # Digests bind the record to bytes: the exact `moduleContent` that crossed + # the seam, and every generated file the response returned for it. With + # them a workspace carries its own chain — FC commit → module bytes → + # generated bytes — and a reader can check each link without this + # repository. The sidecar is the schema-version-1 provenance boundary by design + # (lean-eval-generator keeps its wire format frozen), so it has to be + # strict and deterministic as well: unknown keys are refused on load and + # serialisation is key-sorted. + module_sha256: str = "" + file_sha256: tuple = () + # The exact request bytes that crossed the seam, as their digest: with + # it, "the emitted request is what generation ran" is checkable. + request_sha256: str = "" + # What produced the artifact — importer commit, pinned generator, target + # pins — bound at generation time like the digests, absent before it. + producer: ProducerRecord = None + + def with_digests(self, module_sha256, files, request_sha256=""): + """The same manifest, bound to the request, module bytes and files.""" + return dataclasses.replace( + self, + module_sha256=module_sha256, + file_sha256=tuple(sorted((path, digest) for path, digest in files.items())), + request_sha256=request_sha256, + ) + + def with_producer(self, producer): + """The same manifest, naming what produced the artifact.""" + return dataclasses.replace(self, producer=producer) + + def __post_init__(self): + for field in ("id", "theorem", "qualified_theorem"): + if not getattr(self, field): + raise SystemExit(f"manifest has no {field}") + # lean-eval#536 names these two explicitly, and a manifest without + # them cannot be traced back to a revision of this repository or + # regenerated when FC fixes a misformalisation upstream. + if not self.source.commit: + raise SystemExit(f"manifest {self.id} records no FC source commit") + if not self.source.declaration: + raise SystemExit(f"manifest {self.id} records no FC declaration id") + + + def to_json_object(self): + payload = { + "schema_version": MANIFEST_SCHEMA_VERSION, + "id": self.id, + "theorem": self.theorem, + "qualified_theorem": self.qualified_theorem, + "category": self.category, + "apply_arguments": list(self.apply_arguments), + "holes": [dataclasses.asdict(hole) for hole in self.holes], + "permitted_axioms": list(self.permitted_axioms), + "source": { + **dataclasses.asdict(self.source), + "copied_dependencies": list(self.source.copied_dependencies), + }, + } + if self.source_url: + payload["source_url"] = self.source_url + if self.module_sha256: + payload["digests"] = { + "module": self.module_sha256, + "files": dict(self.file_sha256), + } + if self.request_sha256: + payload["digests"]["request"] = self.request_sha256 + if self.producer is not None: + payload["producer"] = self.producer.to_json_object() + return payload + + KNOWN_KEYS = frozenset( + { + "schema_version", "id", "theorem", "qualified_theorem", "category", + "apply_arguments", "holes", "permitted_axioms", "source", + "source_url", "digests", "producer", + } + ) + + @classmethod + def from_json_object(cls, payload): + version = payload.get("schema_version") + if version != MANIFEST_SCHEMA_VERSION: + raise SystemExit( + f"manifest schema version {version!r} is not " + f"{MANIFEST_SCHEMA_VERSION}" + ) + unknown = sorted(set(payload) - cls.KNOWN_KEYS) + if unknown: + raise SystemExit(f"provenance record has unknown keys: {', '.join(unknown)}") + source = dict(payload["source"]) + source["copied_dependencies"] = tuple(source["copied_dependencies"]) + copied_keys = {"declaration", "module", "path", "range", "content_sha256"} + for entry in source["copied_dependencies"]: + unknown = sorted(set(entry) - copied_keys) + if unknown: + raise SystemExit( + f"a copied dependency has unknown keys: {', '.join(unknown)}" + ) + unknown = sorted(set(source) - {f.name for f in dataclasses.fields(SourceRecord)}) + if unknown: + raise SystemExit(f"provenance source has unknown keys: {', '.join(unknown)}") + digests = dict(payload.get("digests", {})) + unknown = sorted(set(digests) - {"module", "files", "request"}) + if unknown: + raise SystemExit(f"provenance digests have unknown keys: {', '.join(unknown)}") + return cls( + id=payload["id"], + theorem=payload["theorem"], + qualified_theorem=payload["qualified_theorem"], + apply_arguments=tuple(payload["apply_arguments"]), + holes=tuple(DefinitionHole(**hole) for hole in payload["holes"]), + permitted_axioms=tuple(payload["permitted_axioms"]), + source=SourceRecord(**source), + source_url=payload.get("source_url", ""), + category=payload.get("category", ""), + module_sha256=digests.get("module", ""), + file_sha256=tuple(sorted(dict(digests.get("files", {})).items())), + request_sha256=digests.get("request", ""), + producer=( + ProducerRecord.from_json_object(payload["producer"]) + if "producer" in payload + else None + ), + ) + + def to_json(self): + # Key-sorted: the same record always serialises to the same bytes. + return dump_json(self.to_json_object(), sort_keys=True) + + @classmethod + def from_json(cls, text): + return cls.from_json_object(json.loads(text)) + + +@dataclasses.dataclass(frozen=True) +class MarkedUpModule: + """One Mathlib-only Lean module, in the four labelled regions. + + `dependency_declarations` names each copied declaration and the exact + text the dependencies region carries for it, in order. The contract wants + a source span per declaration, and only the renderer knows which bytes + belong to which copied name. + """ + + dependencies: str + scope: str + holes: str + statement: str + dependency_declarations: tuple = () + + def __post_init__(self): + # Rendering separates the regions itself, so leading and trailing + # blank lines are not part of a region's content. + for name in REGIONS: + object.__setattr__(self, name, getattr(self, name).strip("\n")) + + def regions(self): + return {name: getattr(self, name) for name in REGIONS} + + def render(self): + """The module as handed over: plain Lean, no markers of any kind.""" + parts = [MODULE_PREAMBLE] + for body in self.regions().values(): + body = body.strip("\n") + if body: + parts.append("\n" + body + "\n") + return "".join(parts) + + +# The `@[category ...]` tags that name a problem, and the lean-eval group +# each belongs to. `research open` is the point of the FC import and goes to +# the open-conjectures display; everything already settled — solved research, +# textbook and test statements — is evaluation material. `API` declarations +# and untagged ones are not problems and are refused. +CATEGORY_GROUPS = { + "research open": "open-conjectures", + "research solved": "formalization-evaluation", + "textbook": "formalization-evaluation", + "test": "formalization-evaluation", +} + + +def problem_group(manifest): + """The lean-eval problem group for an imported declaration's category.""" + group = CATEGORY_GROUPS.get(manifest.category) + if group is None: + raise SystemExit( + f"{manifest.id}: category {manifest.category!r} is not a " + "problem category; expected one of " + + ", ".join(sorted(CATEGORY_GROUPS)) + ) + return group + + +def module_declarations(marked_up, manifest): + """Every declaration in the rendered module, in order. + + Returns `(name, body, kind, explicit_parameters)` tuples: the copied + dependencies first, then the hoisted answer holes, then the statement. + The generator needs a span for each — holes to slice, dependencies to + keep or drop per generated file — and the bodies are what the spans are + computed from. + """ + declarations = [ + (name, body, "helper", None) + for name, body in marked_up.dependency_declarations + ] + declarations += [ + (hole.name, hole.declaration(), "def", None) for hole in manifest.holes + ] + # `open X in` prefix lines travel inside the statement slice, but the + # span the generator receives must start at the declaration keyword: + # the generator re-attaches whatever sits between the previous span and + # this one as the declaration's prefix, and a prefix hidden inside the + # span would be dropped from the reconstructed files. + statement = marked_up.statement + lines = statement.split("\n") + start = 0 + while start < len(lines) - 1 and lines[start].rstrip().endswith(" in"): + start += 1 + declarations.append( + ( + manifest.theorem, + "\n".join(lines[start:]), + "theorem", + list(manifest.apply_arguments), + ) + ) + return declarations + + +def _positions(text): + """Codepoint offset of the start of each 1-indexed line.""" + starts = [0] + for line in text.split("\n")[:-1]: + starts.append(starts[-1] + len(line) + 1) + return starts + + +def _utf16_column(line_text, column): + """The UTF-16 code-unit column for a codepoint column. + + `.ilean` files store LSP ranges, and LSP counts UTF-16 code units; a + supplementary-plane character (𝔽, 𝕜) earlier in the line makes the two + disagree. + """ + return sum(2 if ord(c) > 0xFFFF else 1 for c in line_text[:column]) + + +def declaration_spans(module_text, declarations): + """A source span for each declaration, located by its exact text. + + The renderer wrote every declaration into the module verbatim, so each + body appears in the text; a body appearing more than once would make the + span a guess, and is refused. Lines are 1-indexed. `codepoint` columns + are what the contract's `resolvedHoles` carry; `utf16` columns are what + an `.ilean` carries. + """ + line_starts = _positions(module_text) + lines = module_text.split("\n") + + def line_of(offset): + low, high = 0, len(line_starts) - 1 + while low < high: + mid = (low + high + 1) // 2 + if line_starts[mid] <= offset: + low = mid + else: + high = mid - 1 + return low + + spans = [] + for name, body, kind, explicit in declarations: + body = body.strip("\n") + first = module_text.find(body) + if first < 0: + raise SystemExit(f"{name}: declaration text not found in the module") + if module_text.find(body, first + 1) >= 0: + raise SystemExit( + f"{name}: declaration text appears more than once in the module" + ) + end = first + len(body) + start_line, end_line = line_of(first), line_of(end) + start_col = first - line_starts[start_line] + end_col = end - line_starts[end_line] + spans.append( + { + "name": name, + "kind": kind, + "explicitParameters": explicit, + "startLine": start_line + 1, + "startColumn": start_col, + "endLine": end_line + 1, + "endColumn": end_col, + "utf16StartColumn": _utf16_column(lines[start_line], start_col), + "utf16EndColumn": _utf16_column(lines[end_line], end_col), + } + ) + return spans + + +def build_problem(marked_up, manifest, policy): + """One problem entry of the schema-version-1 request, and its `.ilean` declaration map. + + The module name is a single identifier on purpose: the generator resolves + module names to paths by splitting on every dot, guillemets included, so + a dotted or quoted name would trip the same decoder defect this + repository fixed on its own side. + + `policy` is the LeanEval-side intake policy: a frozen set's explicit + `group` overrides the category-derived one, because the list is + immutable while its members keep getting solved, and the category rides + along as a tag. The category is still validated either way — a + declaration that is not a problem has no business in any group. + + Returns `(problem, ilean_decls)`. The `.ilean` payload exists because the + generator reads helper-declaration spans from compiled metadata it + expects to find under the context root; this consumer synthesises that + metadata from the spans it computed, which it can do exactly because it + rendered the module. + """ + module_name = slug(manifest.id) + text = marked_up.render() + spans = declaration_spans(text, module_declarations(marked_up, manifest)) + resolved, ilean = [], {} + for span in spans: + # `.ilean` lines are 0-indexed; `loadIleanDeclRanges` adds one back. + ilean[span["name"]] = [ + span["startLine"] - 1, + span["utf16StartColumn"], + span["endLine"] - 1, + span["utf16EndColumn"], + ] + if span["kind"] == "helper": + continue + resolved.append( + { + "declarationName": span["name"], + "module": module_name, + "startLine": span["startLine"], + "startColumn": span["startColumn"], + "endLine": span["endLine"], + "endColumn": span["endColumn"], + "explicitParameters": span["explicitParameters"], + "sameModuleDependencies": ( + [name for name, _ in marked_up.dependency_declarations] + if span["kind"] == "theorem" + else [] + ), + "holeDependentDependencies": [], + "kind": span["kind"], + } + ) + category_group = problem_group(manifest) + problem = { + "id": slug(manifest.id), + "title": manifest.qualified_theorem, + "group": policy.group or category_group, + "status": policy.status, + "visible": policy.visible, + "statementRevision": policy.statement_revision, + "tags": list(policy.tags) + [manifest.category.replace(" ", "-")], + "moduleName": module_name, + "holes": [entry["declarationName"] for entry in resolved], + "submitter": policy.submitter, + "notes": None, + "source": manifest.source_url or None, + "informalSolution": None, + "moduleContent": text, + "resolvedHoles": resolved, + } + return problem, ilean + + +def build_request(problems, target, workspace_test, context_root): + """The complete schema-version-1 request for a batch of `(problem, ilean)` pairs. + + `problems` are the entries `build_problem` returned; the ilean halves go + to whoever writes the context root, not into the request. Ids must be + unique across the batch — two problems generating into one directory is + the collision the qualified default id exists to prevent. + """ + seen = set() + for problem in problems: + if problem["id"] in seen: + raise SystemExit(f"duplicate workspace id {problem['id']!r}") + seen.add(problem["id"]) + return { + "schemaVersion": CONTRACT_VERSION, + "contextRoot": str(context_root), + "leanToolchain": target.lean_toolchain, + "mathlib": { + "name": "mathlib", + "git": target.mathlib_git, + "rev": target.mathlib_revision, + }, + "templates": {"workspaceTest": workspace_test}, + "problems": problems, + } + + +def safe_workspace_path(path): + """A response path fit to join under a directory, or a refusal. + + The pinned generator is still an external process across a versioned + boundary; a future defect there must fail closed here, not write outside + the staging tree. Strictly relative POSIX, every component a real name: + no absolute paths, no drive letters, no backslashes, no NUL, no empty or + `.`/`..` components — which also makes the supplied spelling its own + normal form, so two spellings of one file cannot slip past the duplicate + check. + """ + if not path or "\x00" in path or "\\" in path: + raise SystemExit(f"response path {path!r} is not a plain relative path") + if path.startswith("/") or re.match(r"^[A-Za-z]:", path): + raise SystemExit(f"response path {path!r} is not relative") + if any(part in ("", ".", "..") for part in path.split("/")): + raise SystemExit(f"response path {path!r} has an empty or dot component") + return path + + +# The provenance sidecar's name inside a workspace. It is this side's file: +# a generator response naming it would silently lose to the sidecar written +# after it, so the response parser refuses it outright. +PROVENANCE_STEM = "fc-provenance" +PROVENANCE_FILE = f"{PROVENANCE_STEM}.json" + + +def parse_response(text, expected_ids=None): + """The generator's file maps, with every byte and identity checked. + + Returns `{problem_id: {path: content}}`. A digest mismatch means the + bytes were damaged in transit or the pinned generator is not the one + this code was written against; either way the workspace cannot be + trusted, so refuse. The same goes for shape: unknown fields, missing + fields, unsafe paths and — when `expected_ids` is given — any mismatch + between the workspaces requested and the workspaces returned. An extra + workspace dropped on the floor is as wrong as a missing one. + """ + try: + payload = json.loads(text) + except json.JSONDecodeError as error: + raise SystemExit(f"generator response is not JSON: {error}") from None + if not isinstance(payload, dict): + raise SystemExit("generator response is not a JSON object") + unknown = sorted(set(payload) - {"schemaVersion", "files"}) + if unknown: + raise SystemExit(f"generator response has unknown keys: {', '.join(unknown)}") + version = payload.get("schemaVersion") + if version != CONTRACT_VERSION: + raise SystemExit( + f"generator response schema version {version!r} is not {CONTRACT_VERSION}" + ) + if "files" not in payload: + raise SystemExit("generator response has no files") + workspaces = {} + for entry in payload["files"]: + unknown = sorted(set(entry) - {"problemId", "path", "sha256", "content"}) + if unknown: + raise SystemExit( + f"a response entry has unknown keys: {', '.join(unknown)}" + ) + missing = sorted({"problemId", "path", "sha256", "content"} - set(entry)) + if missing: + raise SystemExit(f"a response entry has no {', '.join(missing)}") + path = safe_workspace_path(entry["path"]) + if path == PROVENANCE_FILE: + raise SystemExit( + f"{entry['problemId']}: the response names {PROVENANCE_FILE}, " + "which is this side's provenance sidecar" + ) + if sha256_text(entry["content"]) != entry["sha256"]: + raise SystemExit( + f"{entry['problemId']}/{path}: content does not match its digest" + ) + files = workspaces.setdefault(entry["problemId"], {}) + if path in files: + raise SystemExit(f"{entry['problemId']}/{path}: appears twice in response") + files[path] = entry["content"] + if expected_ids is not None: + expected = set(expected_ids) + returned = set(workspaces) + missing = sorted(expected - returned) + extra = sorted(returned - expected) + if missing: + raise SystemExit( + f"the generator returned no files for {', '.join(missing)}" + ) + if extra: + raise SystemExit( + "the generator returned workspaces nothing requested: " + f"{', '.join(extra)}" + ) + return workspaces diff --git a/comparator/adapter/limits.py b/comparator/adapter/limits.py new file mode 100644 index 0000000000..494eda9061 --- /dev/null +++ b/comparator/adapter/limits.py @@ -0,0 +1,34 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""How long the adapter waits for anything it does not control. + +Every subprocess here is bounded, and the bounds are stated once. They live +in their own module because the four callers — source reading, the importer, +the generator plumbing and the target compile — otherwise have no reason to +import one another, and a shared constant is not a reason to grow the +dependency graph. +""" + +# A Lean run that has not answered by now is stuck, not slow: a cold run +# imports Mathlib and may build the extractor first, and that is minutes. +# A hang should end the run, not the day. +LEAN_TIMEOUT_SECONDS = 1800 + +# Each extra pair in a batch shares one environment, so it costs elaboration +# but not another import. +BATCH_TIMEOUT_PER_PAIR_SECONDS = 30 + +# Git here is local and reads the index; a minute means a stuck lock file. +GIT_TIMEOUT_SECONDS = 60 diff --git a/comparator/adapter/make_comparator_workspace.py b/comparator/adapter/make_comparator_workspace.py new file mode 100644 index 0000000000..5bc893edc5 --- /dev/null +++ b/comparator/adapter/make_comparator_workspace.py @@ -0,0 +1,459 @@ +#!/usr/bin/env python3 +"""Import one Formal Conjectures declaration and generate its workspace. + +`leanprover/lean-eval` verifies a submission by building it against a Challenge +module whose statement the maintainers trust, under a config that pins the +permitted axioms. This command produces that shape for one Formal Conjectures +declaration, in the two steps `leanprover/lean-eval#536` separates: + + fc_leaneval_importer FC declaration -> marked-up module + manifest + lean-eval-generator schema-version-1 request -> workspace file map + +The first half is Formal Conjectures'. The second is the pinned +`leanprover/lean-eval-generator` binary — a deterministic Lean CLI with a +versioned JSON contract — run by `comparator/adapter/leaneval_generator_cli.py` at the +revision `comparator/tools.toml` pins. `comparator/adapter/leaneval_interface.py` builds +the request and checks the response. `comparator/OWNERSHIP.md` says exactly +what belongs to which side. This file is the wiring between them and belongs +to neither. + +The marked-up module requires Mathlib and nothing else. lean-eval vendors its +problems, so a Challenge cannot fetch this repository at evaluation time, which +rules out importing the problem's own module. This repository's statements are +not authored self-contained, so the declarations a statement needs are copied +into the module's dependency region, dependencies first, each carrying the +`open`, `variable`, `universe`, `set_option` and `local notation` in force +where it was written. + +Copying is a construction and it can be wrong in ways only Lean sees, so +`--verify` elaborates the marked-up module before you trust it. + +`comparator/README.md` describes the workspace this produces and the pins it +carries; this file does not restate them. + +Lean reports the type of each `answer(sorry)` slot. The importer refuses a case +when it cannot match the reported types to their source positions. + +Usage: + python make_comparator_workspace.py (ID | DECLARATION) [--out DIR] + [--answer-type T] [--module FILE] [--verify] + python make_comparator_workspace.py ID --emit-import DIR + python make_comparator_workspace.py --set NAME [--out DIR] [--verify] + [--report FILE] [--known-failures FILE] + python make_comparator_workspace.py --validate + +`--set` imports every declaration of a `FormalConjectures/Subsets` list, +builds one request for all of them, and writes a per-declaration report. +With `--known-failures`, the run fails unless the failures are exactly the +recorded ones: an unexpected failure and a silently fixed one both count, +because a gate that only ever passes proves nothing. + +`--emit-import` writes the exact bytes that cross the seam — the schema-version-1 request, +with its context directory — and generates no workspace; running the pinned +binary on that request from inside the emitted directory yields the same file +map this command would have written. + +The workspace's own build needs a network fetch of its pinned dependencies, so +this command does not attempt it; generation is offline apart from the +generator binary, and the build belongs to the comparator run. +""" + +import argparse +import json +import pathlib +import re +import shutil +import sys +import tempfile + +from known_failures import gate, load_known_failures +import fc_leaneval_importer as importer +import fc_source +import leaneval_generator_cli as generator_cli +from leaneval_interface import ( + ImportPolicy, + PROVENANCE_FILE, + PROVENANCE_STEM, + build_problem, + build_request, + dump_json, + sha256_text, + slug, +) + + +# The request's context directory, relative to the request file, so an +# emitted seam artifact is self-contained and reproducible from any path. +CONTEXT_DIR = "context" + + +def _write_files(directory, files): + """Materialise a `{relative path: content}` mapping under `directory`. + + Every destination must land inside `directory`: the mapping may contain + paths from a response, and `parse_response` already refuses unsafe ones, + but the writer is the last line and checks for itself. + """ + directory = pathlib.Path(directory) + base = directory.resolve() + for relative, content in files.items(): + destination = directory / relative + if not destination.resolve().is_relative_to(base): + raise SystemExit(f"{relative}: escapes the output directory") + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_text(content, encoding="utf-8") + + +def write_tree(target, files): + """Write a complete directory without overwriting or leaving a partial one. + + Plumbing, and on neither side of the seam: the generator returns a + path-to-content mapping and never touches the filesystem, so putting one + on disk is the command's job whether the mapping is a workspace or the + request this repository hands over. + """ + target = pathlib.Path(target) + if target.exists(): + raise SystemExit(f"refusing to overwrite existing workspace: {target}") + target.parent.mkdir(parents=True, exist_ok=True) + staging = pathlib.Path( + tempfile.mkdtemp(prefix=f".{target.name}.", dir=target.parent) + ) + try: + _write_files(staging, files) + staging.rename(target) + except BaseException: + shutil.rmtree(staging, ignore_errors=True) + raise + return target + + +def import_policy(group=None): + """The intake policy this command submits under, stated in one place. + + Destination group, lifecycle status, visibility, statement revision and + submitter are LeanEval's decisions; the schema-version-1 request requires + them inline, so the command instantiates the draft-intake values + explicitly rather than leaving them as wire-module constants. A real + LeanEval intake would build this from the catalog's own state. + """ + return ImportPolicy( + group=group or "", + status="draft", + visible=True, + statement_revision=1, + submitter="formal-conjectures-importer", + tags=("formal-conjectures",), + ) + + +def _seam(pairs, group=None): + """The request and its `build_problem` outputs for `(marked_up, manifest)` pairs.""" + policy = import_policy(group) + problems = [ + build_problem(marked_up, manifest, policy) + for marked_up, manifest in pairs + ] + target = importer.target_pins() + template = ( + importer.comparator_dir() / "templates" / "WorkspaceTest.lean" + ).read_text(encoding="utf-8") + request = build_request( + [problem for problem, _ in problems], target, template, CONTEXT_DIR + ) + return request, problems + + +def seam_files(pairs, group=None): + """The request and context for `(marked_up, manifest)` pairs, as files. + + This is the artifact the FC importer contributes once lean-eval consumes + the shared generator: the request bytes, the context directory the schema-version-1 + contract still reads, and one provenance record per problem — the FC + source commit and declaration id §10 requires, which the schema-version-1 wire format + has no field for, so they travel beside it rather than through it. + """ + request, problems = _seam(pairs, group=group) + request_text = dump_json(request) + producer = importer.producer_record() + files = {"request.json": request_text} + for path, content in generator_cli.context_files(problems).items(): + files[f"{CONTEXT_DIR}/{path}"] = content + for (problem, _), (_, manifest) in zip(problems, pairs): + # Before generation the record binds the module bytes only; the + # workspace's copy adds the generated files. + bound = manifest.with_digests( + sha256_text(problem["moduleContent"]), + {}, + request_sha256=sha256_text(request_text), + ).with_producer(producer) + files[f"{PROVENANCE_STEM}-{problem['id']}.json"] = bound.to_json() + return request, files + + +def generate_workspaces(pairs, out_dir, group=None, emit_request=None): + """Generate one workspace per pair under `out_dir`, via the pinned binary. + + With `emit_request`, the exact request bytes piped to the binary are also + written to that path — a set audit's artifact should carry the request + that produced it, not just the reports about it. + """ + request, problems = _seam(pairs, group=group) + # One serialisation, used everywhere: the string piped to the binary is + # the string `--emit-import` writes and the sidecar digests. The request + # keeps its relative `contextRoot`; the binary runs with the staging + # directory as its working directory, which is where that root resolves. + request_text = dump_json(request) + staging = pathlib.Path(tempfile.mkdtemp(prefix=".fc-seam.")) + try: + # Only the context crosses to the binary; the request goes on stdin + # and the provenance sidecars belong to the written workspaces, so + # neither is staged here. + _write_files(staging / CONTEXT_DIR, generator_cli.context_files(problems)) + workspaces = generator_cli.generate( + request_text, + cwd=staging, + expected_ids=[p["id"] for p in request["problems"]], + ) + finally: + shutil.rmtree(staging, ignore_errors=True) + if emit_request is not None: + emit_request = pathlib.Path(emit_request) + emit_request.parent.mkdir(parents=True, exist_ok=True) + emit_request.write_text(request_text, encoding="utf-8") + module_content = {p["id"]: p["moduleContent"] for p in request["problems"]} + producer = importer.producer_record() + # Every refusal — digest, identity, sidecar, target-already-exists — + # happens before the first workspace lands, so a refused batch writes + # nothing rather than a prefix of itself. + outputs = [] + for _, manifest in pairs: + problem_id = slug(manifest.id) + workspace = dict(workspaces[problem_id]) + # The provenance sidecar rides in the workspace directory, not in the + # generator's file map: the generator neither knows nor checks it. It + # binds the exact request and module bytes sent and every file + # received. + # The sidecar's `permitted_axioms` is an assertion about the + # generated Comparator config; check it against the config actually + # produced, so the recorded policy cannot drift from the enforced one. + config = json.loads(workspace.get("config.json", "{}")) + generated_axioms = tuple(config.get("permitted_axioms", ())) + if sorted(generated_axioms) != sorted(manifest.permitted_axioms): + raise SystemExit( + f"{problem_id}: the generated config permits axioms " + f"{sorted(generated_axioms)}, but the manifest records " + f"{sorted(manifest.permitted_axioms)}" + ) + bound = manifest.with_digests( + sha256_text(module_content[problem_id]), + {path: sha256_text(content) for path, content in workspace.items()}, + request_sha256=sha256_text(request_text), + ).with_producer(producer) + workspace[PROVENANCE_FILE] = bound.to_json() + outputs.append((pathlib.Path(out_dir) / problem_id, workspace)) + for target, _ in outputs: + if target.exists(): + raise SystemExit(f"refusing to overwrite existing workspace: {target}") + return [write_tree(target, files) for target, files in outputs] + + +def subset_declarations(set_name): + """The declaration list of a `FormalConjectures/Subsets` module. + + The subset files hold one `decl_name% ` per line; the + `decl_name%` elaborator is what guarantees each name resolves, so the + text layer can read the list without re-proving that. + """ + path = fc_source.ROOT / "FormalConjectures" / "Subsets" / f"{set_name}.lean" + if not path.is_file(): + raise SystemExit(f"no subset module at {path}") + names = re.findall( + r"decl_name%\s+([\w.«»]+)", path.read_text(encoding="utf-8") + ) + if not names: + raise SystemExit(f"{path} lists no decl_name% entries") + return names + + + + +def import_set(set_name, out_dir, verify=False, known_failures=None): + """Import a whole subset, generate what imports, and report the rest. + + Returns the report object. Source-side failures — the importer refusing, + or `--verify` elaboration failing — are recorded per declaration rather + than aborting the run, because the whole-set result is the artifact: + lean-eval#536 gates the FC import on this audit being reproducible. + """ + declarations = subset_declarations(set_name) + # One batched extractor run pays the Mathlib import once for the whole + # set. A declaration whose module cannot even be located is skipped here + # and fails in its own import below, exactly as it always did. + statement_pairs = [] + for declaration in declarations: + try: + statement_pairs.append(importer.statement_pair(declaration)) + except SystemExit: + continue + fc_source.prefetch_elaborator_facts(statement_pairs) + pairs, results = [], [] + for declaration in declarations: + try: + marked_up, manifest = importer.import_problem(declaration) + if verify: + importer.elaborate(marked_up) + except SystemExit as failure: + results.append( + { + "declaration": declaration, + "status": "source-failed", + "reason": str(failure), + } + ) + continue + pairs.append((marked_up, manifest)) + results.append( + { + "declaration": declaration, + "id": slug(manifest.id), + "category": manifest.category, + "status": "imported", + } + ) + # The set decides the tab: a frozen list stays advertised whole, with + # solved members marked by their category tag, so every member goes to + # the open-conjectures group (google-deepmind/formal-conjectures#5075). + written = ( + generate_workspaces( + pairs, + out_dir, + group="open-conjectures", + emit_request=pathlib.Path(out_dir) / "request.json", + ) + if pairs + else [] + ) + categories = {} + for entry in results: + if entry["status"] == "imported": + categories[entry["category"]] = categories.get(entry["category"], 0) + 1 + report = { + "set": set_name, + "total": len(declarations), + "imported": len(pairs), + "source_failed": len(declarations) - len(pairs), + "categories": dict(sorted(categories.items())), + "workspaces": [str(path) for path in written], + "declarations": results, + } + if known_failures is not None: + actual = { + entry["declaration"] + for entry in results + if entry["status"] == "source-failed" + } + report["known_failures_match"] = gate( + known_failures, actual, "source", "declaration" + ) + return report + + +def main(argv): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument( + "declaration", + nargs="?", + help="a problem id, or a declaration name such as erdos_940", + ) + ap.add_argument("--out", default=str(fc_source.ROOT / ".comparator")) + ap.add_argument( + "--answer-type", + default=None, + help="type of a non-Prop answer(sorry) slot, for the rare " + "statement whose slots the elaborated environment cannot type apart", + ) + ap.add_argument( + "--module", + default=None, + help="the file declaring it, when more than one does; " + "overrides the problem file's `module`", + ) + ap.add_argument( + "--verify", + action="store_true", + help="elaborate the marked-up module against this checkout's Mathlib " + "before accepting it", + ) + ap.add_argument( + "--emit-import", + default=None, + metavar="DIR", + help="write only the schema-version-1 request and its context, the bytes this " + "repository hands the pinned generator, and generate no workspace", + ) + ap.add_argument( + "--validate", + action="store_true", + help="check every problem file resolves, and import nothing", + ) + ap.add_argument( + "--set", + default=None, + metavar="NAME", + help="import every declaration of FormalConjectures/Subsets/NAME.lean", + ) + ap.add_argument( + "--report", + default=None, + metavar="FILE", + help="with --set: write the per-declaration report here as JSON", + ) + ap.add_argument( + "--known-failures", + default=None, + metavar="FILE", + help="with --set: fail unless the failures are exactly the recorded ones", + ) + args = ap.parse_args(argv) + if args.validate: + return importer.validate() + if args.set: + known = ( + load_known_failures(args.known_failures) + if args.known_failures + else None + ) + report = import_set( + args.set, args.out, verify=args.verify, known_failures=known + ) + text = dump_json(report) + if args.report: + pathlib.Path(args.report).write_text(text, encoding="utf-8") + print(text, end="") + if known is None: + print( + "no --known-failures: this run reports failures but gates nothing", + file=sys.stderr, + ) + if known is not None and not report["known_failures_match"]: + return 1 + return 0 + if not args.declaration: + ap.error("give a declaration, --set, or --validate") + marked_up, manifest = importer.import_problem( + args.declaration, args.answer_type, args.module + ) + if args.verify: + importer.elaborate(marked_up) + if args.emit_import: + _, files = seam_files([(marked_up, manifest)]) + print(write_tree(pathlib.Path(args.emit_import) / slug(manifest.id), files)) + return 0 + for path in generate_workspaces([(marked_up, manifest)], args.out): + print(path) + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/comparator/adapter/test_fc_leaneval_importer.py b/comparator/adapter/test_fc_leaneval_importer.py new file mode 100644 index 0000000000..8588bf2f1e --- /dev/null +++ b/comparator/adapter/test_fc_leaneval_importer.py @@ -0,0 +1,384 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""Offline tests for the Formal Conjectures side of the LeanEval importer. + +Every case here pins a failure the first real workspace build produced, or a +rule whose violation would produce a marked-up module that elaborates but poses +the wrong problem. The build itself is the comparator's job, not these tests'. +""" + +import contextlib +import inspect +import json +import pathlib +import subprocess +import tempfile +import unittest +from unittest import mock + +import fc_leaneval_importer as importer +import fc_source +from fc_leaneval_importer import closure_region, load_manifest +from fc_source import pins, strip_fc_attributes, unwrap_answers + + +class ProblemFileTest(unittest.TestCase): + """An FC problem file supplies what the Lean source cannot.""" + + def setUp(self): + # addCleanup rather than tearDown: a setUp that raises after the + # first line would otherwise leave the root pointing at a directory + # this test is about to delete. + self._dir = tempfile.TemporaryDirectory() + self.addCleanup(self._dir.cleanup) + root = pathlib.Path(self._dir.name) + (root / "comparator" / "problems").mkdir(parents=True) + saved = fc_source.ROOT + self.addCleanup(setattr, fc_source, "ROOT", saved) + fc_source.ROOT = root + + def write(self, name, body): + (importer.manifest_dir() / name).write_text(body) + + def test_absent_problem_file_is_not_an_error(self): + # Most statements need none, and the importer works without one. + self.assertEqual(load_manifest("no_such_problem"), {}) + + def test_fields_are_read(self): + self.write("p.toml", 'id = "p"\ndeclaration = "d"\nmodule = "m.lean"\n') + self.assertEqual(load_manifest("p")["module"], "m.lean") + + def test_unknown_keys_are_refused(self): + # A field no code consumes is a record nobody can check: it reads as + # configuration while silently doing nothing. + self.write("p.toml", 'id = "p"\ndeclaration = "d"\nanswer_type = "ENNReal"\n') + with self.assertRaisesRegex(SystemExit, "keys nothing reads"): + load_manifest("p") + + def test_id_must_match_the_filename(self): + # The filename is what the importer looks up, so a disagreeing `id` + # would silently name a workspace directory nobody asked for. + self.write("p.toml", 'id = "other"\ndeclaration = "d"\n') + with self.assertRaises(SystemExit): + load_manifest("p") + + def test_declaration_is_required(self): + self.write("p.toml", 'id = "p"\n') + with self.assertRaises(SystemExit): + load_manifest("p") + + +class PinTest(unittest.TestCase): + """Every path the importer read is held to the one source revision.""" + + @contextlib.contextmanager + def _pins_repo(self, git_results): + with tempfile.TemporaryDirectory() as tmp: + root = pathlib.Path(tmp) + (root / "lake-manifest.json").write_text( + json.dumps({"packages": [{"name": "mathlib", "rev": "b" * 40}]}), + encoding="utf-8", + ) + # No cache_clear: `_base_pins` is keyed on the root it read, so a + # fixture root and the real one cannot share an entry. + with _root_at(root): + with mock.patch.object( + fc_source.subprocess, "run", side_effect=git_results + ): + yield + + def test_changed_source_is_refused(self): + path = "FormalConjectures/Example.lean" + results = [ + subprocess.CompletedProcess([], 0, stdout="a" * 40 + "\n"), + subprocess.CompletedProcess([], 0, stdout=path + "\n"), + subprocess.CompletedProcess([], 1), + subprocess.CompletedProcess([], 0, stdout=path + "\n"), + ] + with self._pins_repo(results): + with self.assertRaisesRegex(SystemExit, "differs from pinned"): + pins(pathlib.Path(path)) + + def test_a_path_the_revision_does_not_track_is_refused(self): + # `git diff` is silent about untracked files, so a dependency read + # from a file the pinned revision has never seen must fail on the + # tracking check, not pass by omission. + results = [ + subprocess.CompletedProcess([], 0, stdout="a" * 40 + "\n"), + subprocess.CompletedProcess([], 0, stdout="\n"), + ] + with self._pins_repo(results): + with self.assertRaisesRegex(SystemExit, "not tracked at pinned"): + pins(pathlib.Path("FormalConjectures/New.lean")) + + def test_the_toolchain_is_not_held_to_the_pin(self): + # A toolchain bump edits `lean-toolchain` and `lake-manifest.json`. + # Those describe the environment the facts were read in, which the + # record states as an observation. Holding them to the merge base + # would make a bump the one change that cannot pass this check. + import fc_leaneval_importer as importer_module + + source = inspect.getsource(importer_module.import_problem) + self.assertNotIn("lean-toolchain", source) + self.assertNotIn("lake-manifest.json", source) + + def test_a_dirty_dependency_fails_even_with_a_clean_target(self): + # The reviewer's mixed state: target at the pin, dependency edited in + # the working tree. One diff over every read path refuses it. + target = "FormalConjectures/Target.lean" + dep = "FormalConjectures/Dep.lean" + results = [ + subprocess.CompletedProcess([], 0, stdout="a" * 40 + "\n"), + subprocess.CompletedProcess([], 0, stdout=f"{dep}\n{target}\n"), + subprocess.CompletedProcess([], 1), + subprocess.CompletedProcess([], 0, stdout=dep + "\n"), + ] + with self._pins_repo(results): + with self.assertRaisesRegex(SystemExit, "Dep.lean differs from pinned"): + pins([pathlib.Path(target), pathlib.Path(dep)]) + + +@contextlib.contextmanager +def _root_at(directory): + """Point the adapter's root at a fixture tree. + + Every module reads `fc_source.ROOT` rather than a copy of it, and every + cache is keyed on the root it read, so this is the one place a test has + to move and there is nothing to invalidate afterwards. + """ + saved = fc_source.ROOT + fc_source.ROOT = pathlib.Path(directory) + try: + yield fc_source.ROOT + finally: + fc_source.ROOT = saved + + +class MathlibOnlyClosureTest(unittest.TestCase): + """The closure travels with the module, so copying has to be right. + + Each case here is a defect a generated workspace actually had, found by + elaborating it rather than by reading it. + """ + + def test_answer_with_a_value_is_unwrapped(self): + # `answer` is this repository's elaborator. `hoist_answers` removes the + # `answer(sorry)` slots; `conjecture327` is `research solved` and + # carries `answer(False)`, which reached the module verbatim and + # failed to parse against Mathlib alone. + self.assertEqual( + unwrap_answers("theorem t : answer(False) ↔ P := by\n sorry"), + "theorem t : (False) ↔ P := by\n sorry", + ) + + def test_unwrapping_keeps_a_parenthesised_argument_whole(self): + self.assertEqual(unwrap_answers("answer(f (n + 1))"), "(f (n + 1))") + + def test_only_this_repository_s_attributes_are_dropped(self): + # `strip_decorations` clears every attribute off the target statement. + # A copied dependency keeps the rest: dropping `simp` or `reducible` + # changes how the declarations after it in the closure elaborate. + self.assertEqual( + strip_fc_attributes("@[simp, category API, AMS 11]\ntheorem t : P"), + "@[simp]\ntheorem t : P", + ) + self.assertEqual( + strip_fc_attributes("@[category API]\ntheorem t : P"), "theorem t : P" + ) + self.assertEqual( + strip_fc_attributes("@[simp]\ndef f := 1"), "@[simp]\ndef f := 1" + ) + + def test_a_generated_constant_with_no_copied_ancestor_is_refused(self): + with self.assertRaisesRegex(SystemExit, "no copied ancestor"): + closure_region([], ["Foo.bar._proof_1"], "t") + + def test_a_generated_constant_under_a_copied_parent_is_accepted(self): + # `_proof_1` and `.match_1` have no source: copying the parent + # declaration regenerates them, so they are not an error. + deps = [ + { + "name": "Foo.bar", + "module": "FormalConjectures.Example", + "range": {"startLine": 1, "endLine": 1, "endColumn": None}, + } + ] + with ( + mock.patch.object(importer, "module_source_path") as resolve, + tempfile.TemporaryDirectory() as tmp, + _root_at(tmp), + ): + source = pathlib.Path(tmp) / "Example.lean" + source.write_text("def Foo.bar := 1\n", encoding="utf-8") + resolve.return_value = source + out, copied, records = closure_region(deps, ["Foo.bar._proof_1"], "t") + self.assertIn("def Foo.bar := 1", out) + self.assertIn("noncomputable section", out) + self.assertEqual(copied, [("Foo.bar", "def Foo.bar := 1")]) + # The sidecar's record of the same copy: the emitted slice, located + # and digested, so the provenance chain reaches each dependency. + self.assertEqual(len(records), 1) + record = records[0] + self.assertEqual(record["declaration"], "Foo.bar") + self.assertEqual(record["module"], "FormalConjectures.Example") + self.assertEqual(record["path"], "Example.lean") + self.assertEqual(record["range"]["startLine"], 1) + self.assertEqual(len(record["content_sha256"]), 64) + + def test_an_explicit_source_only_dependency_carries_its_closure(self): + facts = fc_source.FactsRecord.from_payload( + { + "declaration": "Foo.opaqueLemma", + "name": "Foo.opaqueLemma", + "category": None, + "range": {"startLine": 2, "endLine": 2, "endColumn": None}, + "binders": [], + "answerTypes": [], + "dependencies": [ + { + "name": "Foo.Predicate", + "module": "FormalConjectures.Example", + "range": {"startLine": 1, "endLine": 1, "endColumn": None}, + } + ], + "generatedDependencies": ["Foo.opaqueLemma._proof_1"], + }, + "Foo.opaqueLemma", + ) + with tempfile.TemporaryDirectory() as tmp, _root_at(tmp): + module = pathlib.Path(tmp) / "FormalConjectures" / "Example.lean" + module.parent.mkdir(parents=True) + module.write_text("def Predicate := True\ntheorem opaqueLemma : Predicate := by trivial\n") + with mock.patch.object(importer, "elaborator_facts", return_value=facts): + records, generated = importer.explicit_copy_dependencies( + { + "copy_dependencies": [ + { + "declaration": "Foo.opaqueLemma", + "module": "FormalConjectures/Example.lean", + } + ] + } + ) + self.assertEqual( + [record["name"] for record in records], + ["Foo.Predicate", "Foo.opaqueLemma"], + ) + self.assertEqual(generated, ["Foo.opaqueLemma._proof_1"]) + + def test_explicit_source_only_dependency_rejects_extra_fields(self): + with self.assertRaisesRegex(SystemExit, "must contain exactly"): + importer.explicit_copy_dependencies( + { + "copy_dependencies": [ + { + "declaration": "Foo.opaqueLemma", + "module": "FormalConjectures/Example.lean", + "guess": True, + } + ] + } + ) + + def test_explicit_source_only_dependency_stays_in_a_source_tree(self): + with self.assertRaisesRegex(SystemExit, "must stay under a source tree"): + importer.explicit_copy_dependencies( + { + "copy_dependencies": [ + { + "declaration": "Foo.opaqueLemma", + "module": "../Elsewhere/Example.lean", + } + ] + } + ) + + def test_a_declaration_inside_another_s_range_is_not_copied_twice(self): + # `EdgeN.mk` covers line 88 of a structure spanning 83 to 93, and + # `pmSumListAux._sparseCasesOn_1` has exactly its parent's range. + # Copying either in its own right duplicated a declaration or sliced a + # fragment of one. + def span(name, lo, hi): + return { + "name": name, + "module": "FormalConjectures.Example", + "range": {"startLine": lo, "endLine": hi, "endColumn": None}, + } + + deps = [ + span("Foo.EdgeN.mk", 2, 2), + span("Foo.EdgeN", 1, 3), + span("Foo.aux._sparseCasesOn_1", 5, 5), + span("Foo.aux", 5, 5), + ] + with ( + mock.patch.object(importer, "module_source_path") as resolve, + tempfile.TemporaryDirectory() as tmp, + _root_at(tmp), + ): + source = pathlib.Path(tmp) / "Example.lean" + source.write_text( + "structure EdgeN where\n u : Nat\n deriving DecidableEq\n" + "\ndef aux := 1\n", + encoding="utf-8", + ) + resolve.return_value = source + out, _copied, _records = closure_region(deps, [], "t") + self.assertIn("Foo.EdgeN`", out) + self.assertNotIn("Foo.EdgeN.mk`", out) + self.assertIn("Foo.aux`", out) + self.assertNotIn("_sparseCasesOn_1`", out) + + def test_an_opened_namespace_no_dependency_declares_is_created(self): + # The statement reopens the namespace stack its target sat in. With + # the problem's module no longer imported, `open Grimm` is an error + # unless something declares that namespace. + out, _copied, _records = closure_region([], [], "grimm_conjecture", ["Grimm"]) + self.assertIn("namespace Grimm\nend Grimm", out) + + def test_namespaces_exist_before_any_copied_block_opens_them(self): + deps = [ + { + "name": "Grimm.helper", + "module": "FormalConjectures.Example", + "range": {"startLine": 1, "endLine": 1, "endColumn": None}, + } + ] + with ( + mock.patch.object(importer, "module_source_path") as resolve, + tempfile.TemporaryDirectory() as tmp, + _root_at(tmp), + ): + source = pathlib.Path(tmp) / "Example.lean" + source.write_text("def Grimm.helper := 1\n", encoding="utf-8") + resolve.return_value = source + out, _copied, _records = closure_region(deps, [], "t", ["Grimm"]) + # The empty block that makes the namespace exist comes before any + # copied block: a copied preamble may `open` it before anything + # declares it. Redundant creation is harmless. + self.assertLess( + out.index("namespace Grimm\nend Grimm"), out.index("def Grimm.helper") + ) + + def test_the_closure_region_does_not_carry_the_import(self): + # `import Mathlib` belongs to the module as a whole, and the generator + # is what decides which emitted file carries it. A region that + # restated it would put an import in the middle of a Lean file. + out, _copied, _records = closure_region([], [], "t") + self.assertNotIn("import", out) + + +if __name__ == "__main__": + unittest.main() diff --git a/comparator/adapter/test_fc_source.py b/comparator/adapter/test_fc_source.py new file mode 100644 index 0000000000..7d68b9029a --- /dev/null +++ b/comparator/adapter/test_fc_source.py @@ -0,0 +1,458 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""Offline tests for reading this repository's own Lean source. + +Every case pins a failure a real import produced, or a rule whose violation +would copy source that elaborates but poses the wrong problem. +""" + +import pathlib +import unittest +from unittest import mock + +import fc_source +from fc_source import ( + answer_spans, + file_scoped_preamble, + hoist_answers, + replace_proof_with_sorry, + strip_decorations, +) + + +class HoistTest(unittest.TestCase): + """Slot types come from the elaborated environment.""" + + def test_slot_takes_the_environment_type(self): + stmt, holes = hoist_answers( + "theorem t : answer(sorry) ↔ ∀ n, n ≤ n := by\n sorry", "t", ["Prop"] + ) + self.assertIn("t_answer", stmt) + self.assertEqual( + holes[0].declaration(), "noncomputable def t_answer : Prop := sorry" + ) + + def test_erased_slot_is_prop_by_the_elaborators_rule(self): + # The default `alwaysTrue` setting erases a slot iff its expected + # type is Prop, so a missing annotation names the type exactly. + _, holes = hoist_answers("theorem t : answer(sorry) ↔ P := by\n sorry", "t", []) + self.assertEqual( + holes[0].declaration(), "noncomputable def t_answer : Prop := sorry" + ) + + def test_mixed_prop_and_typed_slots_are_refused(self): + with self.assertRaises(SystemExit): + hoist_answers( + "theorem t : answer(sorry) ∧ (answer(sorry) = 3) := by\n sorry", + "t", + ["Nat"], + ) + + def test_non_prop_type_is_read_not_guessed(self): + _, holes = hoist_answers( + "theorem t : sSup S = answer(sorry) := by\n sorry", "t", ["ENNReal"] + ) + self.assertEqual(holes[0].type, "ENNReal") + + def test_override_wins(self): + _, holes = hoist_answers( + "theorem t : sSup S = answer(sorry) := by\n sorry", "t", ["ENNReal"], "ℝ" + ) + self.assertEqual(holes[0].type, "ℝ") + + def test_differing_slot_types_are_refused(self): + # Matching types to positions would be a guess. + with self.assertRaises(SystemExit): + hoist_answers( + "theorem t : answer(sorry) = answer(sorry) := by\n sorry", + "t", + ["Nat", "Int"], + ) + + def test_no_slot_is_left_alone(self): + stmt, holes = hoist_answers("theorem t : True := by\n sorry", "t", []) + self.assertEqual(holes, []) + + def test_fixed_answer_is_not_turned_into_a_hole(self): + original = "theorem t : IsGLB S answer(2) := by\n sorry" + unchanged, holes = hoist_answers(original, "t", ["ENNReal"]) + self.assertEqual(unchanged, original) + self.assertEqual(holes, []) + + def test_nested_answer_term_is_one_balanced_slot(self): + calls = answer_spans("theorem t : f answer((fun x => x) (g 2)) := by\n sorry") + self.assertEqual(len(calls), 1) + self.assertEqual(calls[0][2], "(fun x => x) (g 2)") + + def test_answer_text_in_comments_and_strings_is_ignored(self): + calls = answer_spans( + '-- answer(1)\ntheorem t : p "answer(2)" answer(3) := by sorry' + ) + self.assertEqual(len(calls), 1) + self.assertEqual(calls[0][2], "3") + + +class PreambleTest(unittest.TestCase): + """Only directives in force at the statement are carried.""" + + def test_variable_in_a_closed_section_is_dropped(self): + lines = [ + "section S", + "variable {n : Nat}", + "end S", + "", + "open Nat", + "", + "theorem t : True := trivial", + ] + pre, ns = file_scoped_preamble(lines, 7) + self.assertEqual(pre, ["open Nat"]) + self.assertEqual(ns, []) + + def test_namespace_stack_is_reported(self): + lines = ["namespace A", "open Nat", "theorem t : True := trivial"] + pre, ns = file_scoped_preamble(lines, 3) + self.assertEqual(pre, ["open Nat"]) + self.assertEqual(ns, ["A"]) + + def test_directive_inside_a_comment_is_not_a_directive(self): + lines = ["/--", "open the door", "-/", "theorem t : True := trivial"] + pre, _ = file_scoped_preamble(lines, 4) + self.assertEqual(pre, []) + + +class StatementTest(unittest.TestCase): + def test_proof_is_replaced_but_statement_kept(self): + out = replace_proof_with_sorry( + "theorem t : True := by\n have h := trivial\n exact h" + ) + self.assertIn("theorem t : True", out) + self.assertNotIn("have h", out) + self.assertTrue(out.rstrip().endswith("sorry")) + + def test_term_mode_proof_is_replaced_too(self): + out = replace_proof_with_sorry("theorem t : True := trivial") + self.assertNotIn("trivial", out) + self.assertTrue(out.rstrip().endswith("sorry")) + + def test_structure_literal_assign_is_statement_text(self): + # `{ a := 1 }` lives inside brackets; only the top-level `:=` starts + # the proof, so the statement survives intact. + out = replace_proof_with_sorry("theorem t : F { a := 1 } := ⟨rfl⟩") + self.assertIn("F { a := 1 }", out) + self.assertNotIn("⟨rfl⟩", out) + self.assertTrue(out.rstrip().endswith("sorry")) + + def test_autoparam_default_is_statement_text(self): + # An autoParam binder carries `:= by` inside its parentheses; the + # proof is the top-level one. + out = replace_proof_with_sorry( + "theorem t (h : Fact (1 < 2) := by norm_num) : True := by trivial" + ) + self.assertIn(":= by norm_num", out) + self.assertNotIn("trivial", out) + + def test_two_top_level_assigns_are_refused(self): + with self.assertRaises(SystemExit): + replace_proof_with_sorry("def t : Nat := f := g") + + def test_a_line_comment_between_docstring_and_attribute_is_stripped(self): + # Erdos 918 writes a `--` formalisation note there. One anchored pass + # each left `@[category research open]` on the statement, and Lean + # parsed as far as the `open` inside it. + out = strip_decorations( + "/-- doc -/\n-- note\n@[category research open, AMS 5]\n" + "theorem t : True := by\n sorry" + ) + self.assertTrue(out.startswith("theorem")) + + def test_open_in_survives_stripping(self): + # It binds to the declaration, and it sits above the docstring. + out = strip_decorations( + "open scoped Classical in\n/-- doc -/\n@[category research open]\n" + "theorem t : True := by\n sorry" + ) + self.assertTrue(out.startswith("open scoped Classical in\ntheorem")) + + def test_decorations_are_stripped_from_the_target(self): + out = strip_decorations( + "/-- doc -/\n@[category research open]\ntheorem t : True := by\n sorry" + ) + self.assertTrue(out.startswith("theorem")) + + +class DocstringReferenceTest(unittest.TestCase): + """The source citation is read from Formal Conjectures, not copied. + + A hand-kept copy drifts. The Margulis module's docstring pins + `arxiv/2504.17644v3`; the problem file that used to carry the same + citation had the unversioned URL, so the copy was already less exact + than the docstring it was copied from. + """ + + def test_the_first_reference_link_is_the_citation(self): + doc = ( + "/-!\n# Erdős Problem 1038\n\n*Reference:*\n" + " - [erdosproblems.com/1038](https://www.erdosproblems.com/1038)\n" + " - [Tao25] a blog post (https://example.com/other)\n-/" + ) + self.assertEqual( + fc_source.docstring_reference(doc), "https://www.erdosproblems.com/1038" + ) + + def test_an_arxiv_version_suffix_is_preserved(self): + doc = "/-!\n*Reference:* [arxiv/2504.17644v3](https://arxiv.org/abs/2504.17644v3)\n-/" + self.assertEqual( + fc_source.docstring_reference(doc), "https://arxiv.org/abs/2504.17644v3" + ) + + def test_links_above_the_reference_line_are_not_the_citation(self): + doc = "/-!\n# A problem\n\nSee [Mathlib](https://leanprover-community.github.io).\n-/" + self.assertEqual(fc_source.docstring_reference(doc), "") + + def test_a_module_without_a_docstring_has_no_citation(self): + self.assertEqual(fc_source.docstring_reference(""), "") + + +class ModuleNameCodecTest(unittest.TestCase): + """`module_name` and `module_source_path` are inverse on real modules.""" + + def test_a_guillemet_component_keeps_its_dots(self): + self.assertEqual( + fc_source.split_module( + "FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture" + ), + ["FormalConjectures", "Arxiv", "0912.2382", "CurlingNumberConjecture"], + ) + + def test_a_dotted_final_component_keeps_its_tail(self): + # `with_suffix` would have turned `«2501.03234»` into `«2501.lean`. + path = fc_source.module_source_path( + "FormalConjectures.Arxiv.«2501.03234».ArithmeticSumS" + ) + self.assertEqual(path.name, "ArithmeticSumS.lean") + self.assertEqual(path.parent.name, "2501.03234") + + def test_a_malformed_name_is_refused(self): + with self.assertRaises(SystemExit): + fc_source.split_module("FormalConjectures.«unterminated") + + def test_every_real_module_round_trips(self): + # The property that keeps the codec from drifting again: for every + # file the importer can name, decoding the name reaches the file. + for src in fc_source.source_dirs(fc_source.ROOT): + for path in src.rglob("*.lean"): + rel = path.relative_to(fc_source.ROOT) + with self.subTest(module=str(rel)): + self.assertEqual( + fc_source.module_source_path(fc_source.module_name(rel)), path + ) + + +class QualifiedResolutionTest(unittest.TestCase): + """Qualified requests resolve through the namespace stack.""" + + def test_the_bare_colliding_name_is_ambiguous(self): + with self.assertRaises(SystemExit) as ctx: + fc_source.find_declaration("conjecture") + self.assertIn("ambiguous", str(ctx.exception)) + + def test_each_qualified_name_reaches_its_own_file(self): + for qualified, filename in ( + ("OeisA303656.conjecture", "303656.lean"), + ("OeisA308734.conjecture", "308734.lean"), + ): + with self.subTest(qualified=qualified): + path, _, _, _ = fc_source.find_declaration(qualified) + self.assertEqual(path.name, filename) + + def test_a_declared_name_with_dots_still_resolves(self): + # The declared name itself contains dots; no namespace split applies. + path, _, _, _ = fc_source.find_declaration( + "erdos_125.variants.positive_unequal_density" + ) + self.assertEqual(path.name, "125.lean") + + def test_longest_declared_suffix_wins(self): + # `Erdos125.erdos_125.variants.positive_unequal_density`: the first + # component is the namespace, the rest is the declared name. + path, _, _, _ = fc_source.find_declaration( + "Erdos125.erdos_125.variants.positive_unequal_density" + ) + self.assertEqual(path.name, "125.lean") + + +class FlattenDeclaredNameTest(unittest.TestCase): + """Dotted declaration names are restated as slugs for the generator.""" + + def test_the_declaring_occurrence_is_renamed(self): + name, statement = fc_source.flatten_declared_name( + "erdos_100.variants.strong", + "theorem erdos_100.variants.strong : True := by\n sorry", + ) + self.assertEqual(name, "erdos_100_variants_strong") + self.assertEqual( + statement, "theorem erdos_100_variants_strong : True := by\n sorry" + ) + + def test_a_prefix_line_does_not_confuse_the_rename(self): + # `open X in` binds to the declaration below and travels with the + # slice; the declaring line is not the first line. + name, statement = fc_source.flatten_declared_name( + "a.b", "open Nat in\ntheorem a.b : True := by\n sorry" + ) + self.assertEqual(name, "a_b") + self.assertIn("theorem a_b :", statement) + + def test_an_absent_declaration_is_refused(self): + with self.assertRaises(SystemExit): + fc_source.flatten_declared_name("a.b", "theorem c.d : True := sorry") + + +class PreambleNotationTest(unittest.TestCase): + """File-scoped notation and macros travel with the preamble.""" + + def test_local_notation_is_kept(self): + # Irrational.lean: dropping `local notation "e" => exp 1` left `e` + # to auto-bind as an implicit at FC pins and fail at LeanEval's. + lines = ['local notation "e" => exp 1', "theorem t : True := trivial"] + pre, _ = file_scoped_preamble(lines, 2) + self.assertEqual(pre, ['local notation "e" => exp 1']) + + def test_a_macro_keeps_its_indented_body(self): + # Poincare.lean: the 𝕊ⁿ macro's body is on the next line; one kept + # line would be broken syntax. + lines = [ + 'local macro:max "𝕊" noWs n:superscript(term) : term =>', + " `(Metric.sphere 0 1)", + "theorem t : True := trivial", + ] + pre, _ = file_scoped_preamble(lines, 3) + self.assertEqual(len(pre), 1) + self.assertIn("`(Metric.sphere 0 1)", pre[0]) + + def test_noncomputable_section_is_restated(self): + # OpenQuantumProblems/23: a copied def that was total inside + # `noncomputable section` fails to compile outside it. + lines = ["noncomputable section", "theorem t : True := trivial"] + pre, _ = file_scoped_preamble(lines, 2) + self.assertIn("noncomputable section", pre) + + def test_a_closed_noncomputable_section_is_not_restated(self): + lines = ["noncomputable section", "end", "theorem t : True := trivial"] + pre, _ = file_scoped_preamble(lines, 3) + self.assertNotIn("noncomputable section", pre) + + +class AscribedSlotTest(unittest.TestCase): + """`(answer(sorry) : T)` states its own type at its own position.""" + + def test_the_ascription_wins_over_the_erasure_rule(self): + # Erdos332: the annotation for an ascribed-and-applied slot does not + # survive elaboration, so the environment reports nothing and the + # erasure rule would call it Prop. + statement = ( + "theorem erdos_332 (A : Set ℕ) : " + "(answer(sorry) : Set ℕ → Prop) A → True := by\n sorry" + ) + _, holes = hoist_answers(statement, "erdos_332", []) + self.assertEqual(holes[0].type, "Set ℕ → Prop") + + def test_a_nested_paren_type_stays_whole(self): + statement = "theorem t : (answer(sorry) : (ℕ → ℕ) → Prop) f := by\n sorry" + _, holes = hoist_answers(statement, "t", []) + self.assertEqual(holes[0].type, "(ℕ → ℕ) → Prop") + + def test_an_unascribed_slot_still_follows_the_erasure_rule(self): + statement = "theorem t : answer(sorry) ↔ True := by\n sorry" + _, holes = hoist_answers(statement, "t", []) + self.assertEqual(holes[0].type, "Prop") + + +class NotationBlocksTest(unittest.TestCase): + """FC-defined notation is copied only where it was in force.""" + + def _with_commands(self, commands): + return mock.patch.object( + fc_source, "fc_notation_commands", return_value=commands + ) + + def test_a_scoped_notation_needs_its_namespace_opened(self): + commands = [ + (["ℝ²"], 'scoped[EuclideanGeometry] notation "ℝ²" => E', "EuclideanGeometry", True, pathlib.Path("FormalConjecturesForMathlib/Geometry.lean")), + ] + with self._with_commands(commands): + self.assertEqual( + fc_source.notation_blocks(["def f : ℝ² := sorry"], {"EuclideanGeometry"}), + [('scoped[EuclideanGeometry] notation "ℝ²" => E', + pathlib.Path("FormalConjecturesForMathlib/Geometry.lean"))], + ) + # Green9's `⊆` false positive: same token, namespace never opened. + self.assertEqual( + fc_source.notation_blocks(["def f : ℝ² := sorry"], set()), [] + ) + + def test_a_shared_global_notation_is_copied_as_local(self): + # Global would be declared in ChallengeDeps and re-extracted into + # the importing file too; `local` keeps each copy to its own file. + commands = [(["≪"], 'notation g " ≪ " f => IsBigO g f', None, True, + pathlib.Path("FormalConjecturesForMathlib/Order.lean"))] + with self._with_commands(commands): + self.assertEqual( + fc_source.notation_blocks(["theorem t : a ≪ b := sorry"], set()), + [('local notation g " ≪ " f => IsBigO g f', + pathlib.Path("FormalConjecturesForMathlib/Order.lean"))], + ) + + def test_a_problem_module_global_notation_is_never_copied(self): + commands = [(["≪"], 'notation g " ≪ " f => X g f', None, False, + pathlib.Path("FormalConjectures/Wikipedia/X.lean"))] + with self._with_commands(commands): + self.assertEqual( + fc_source.notation_blocks(["theorem t : a ≪ b := sorry"], set()), [] + ) + + def test_an_unused_token_is_not_copied(self): + commands = [(["ℝ²"], 'notation "ℝ²" => E', None, True, + pathlib.Path("FormalConjecturesForMathlib/Geometry.lean"))] + with self._with_commands(commands): + self.assertEqual(fc_source.notation_blocks(["theorem t : True"], set()), []) + + +class LocaliseNotationTest(unittest.TestCase): + def test_a_global_notation_becomes_local(self): + self.assertEqual( + fc_source.localise_notation(['notation "R(" k ")" => f k']), + ['local notation "R(" k ")" => f k'], + ) + + def test_quot_precheck_travels_with_the_notation(self): + out = fc_source.localise_notation( + ["set_option quotPrecheck false", 'local notation "A" => s'] + ) + self.assertEqual( + out[1], + 'set_option quotPrecheck false in\nlocal notation "A" => s', + ) + + def test_other_preamble_lines_pass_through(self): + self.assertEqual( + fc_source.localise_notation(["open Nat", "variable (n : Nat)"]), + ["open Nat", "variable (n : Nat)"], + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/comparator/adapter/test_leaneval_interface.py b/comparator/adapter/test_leaneval_interface.py new file mode 100644 index 0000000000..bf880b7377 --- /dev/null +++ b/comparator/adapter/test_leaneval_interface.py @@ -0,0 +1,523 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""Tests for the importer-to-generator interface. + +The two values here are the whole contract between the half of this work +Formal Conjectures owns and the half `leanprover/lean-eval-generator` will +own. A value that does not survive being written out and read back is not a +contract, and a manifest that has lost the source commit cannot be regenerated +when Formal Conjectures corrects the statement upstream. +""" + +import unittest +from unittest import mock + +from leaneval_interface import ( + DefinitionHole, + ImportPolicy, + MarkedUpModule, + ProblemManifest, + ProducerRecord, + SourceRecord, + TargetRecord, + _utf16_column, + build_problem, + build_request, + declaration_spans, + module_declarations, + parse_response, + problem_group, + slug, +) + + +def a_source(**overrides): + fields = { + "repository": "https://github.com/google-deepmind/formal-conjectures", + "commit": "a" * 40, + "path": "FormalConjectures/Example.lean", + "blob_sha": "b" * 40, + "module": "FormalConjectures.Example", + "declaration": "erdos_940", + "copied_dependencies": ( + { + "declaration": "Foo.bar", + "module": "FormalConjectures.Example", + "path": "FormalConjectures/Example.lean", + "range": {"startLine": 3, "startColumn": 0, "endLine": 4, "endColumn": 11}, + "content_sha256": "d" * 64, + }, + ), + "original_range": {"startLine": 20, "startColumn": 0, "endLine": 22, "endColumn": 7}, + "original_sha256": "e" * 64, + "lean_toolchain": "leanprover/lean4:v4.33.1", + "mathlib_revision": "c" * 40, + } + fields.update(overrides) + return SourceRecord(**fields) + + +def a_target(**overrides): + fields = { + "lean_toolchain": "leanprover/lean4:v4.33.0", + "mathlib_revision": "f" * 40, + } + fields.update(overrides) + return TargetRecord(**fields) + + +def a_policy(**overrides): + fields = { + "group": "", + "status": "draft", + "visible": True, + "statement_revision": 1, + "submitter": "formal-conjectures-importer", + "tags": ("formal-conjectures",), + } + fields.update(overrides) + return ImportPolicy(**fields) + + +def a_manifest(**overrides): + fields = { + "id": "erdos_940", + "theorem": "erdos_940", + "qualified_theorem": "Erdos.erdos_940", + "apply_arguments": (), + "holes": (DefinitionHole(name="erdos_940_answer", type="ENNReal"),), + "permitted_axioms": ("propext", "Quot.sound", "Classical.choice"), + "source": a_source(), + "source_url": "https://www.erdosproblems.com/940", + "category": "research open", + } + fields.update(overrides) + return ProblemManifest(**fields) + + +A_MODULE = MarkedUpModule( + dependencies="def Foo.bar := 1", + scope="open Erdos", + holes="noncomputable def erdos_940_answer : ENNReal := sorry", + statement="theorem erdos_940 : erdos_940_answer = 0 := by\n sorry", + dependency_declarations=(("Foo.bar", "def Foo.bar := 1"),), +) + + +class ManifestTest(unittest.TestCase): + def test_source_commit_and_declaration_are_required(self): + # lean-eval#536 names both, and neither is something the generator can + # supply: it sees a Lean module, not a repository. + with self.assertRaisesRegex(SystemExit, "no FC source commit"): + a_manifest(source=a_source(commit="")) + with self.assertRaisesRegex(SystemExit, "no FC declaration id"): + a_manifest(source=a_source(declaration="")) + + def test_the_manifest_does_not_carry_the_consumers_pins(self): + # lean-eval#536 gives LeanEval the pin regime. A manifest asserting it + # would go stale when LeanEval bumped, with nothing here to notice. + self.assertNotIn("target", a_manifest().to_json_object()) + + def test_the_pins_the_hole_types_were_read_at_are_recorded(self): + # The consumer supplies its own pins, but it cannot know where these + # hole types were read unless the manifest says so. + payload = a_manifest().to_json_object() + self.assertEqual(payload["source"]["lean_toolchain"], "leanprover/lean4:v4.33.1") + + def test_the_manifest_survives_a_round_trip(self): + manifest = a_manifest() + self.assertEqual(ProblemManifest.from_json(manifest.to_json()), manifest) + + def test_the_serialised_manifest_carries_the_commit_and_declaration(self): + # A reviewer of a generated workspace reads this file, so the two + # fields have to be in it under their own names. + payload = a_manifest().to_json_object() + self.assertEqual(payload["source"]["commit"], "a" * 40) + self.assertEqual(payload["source"]["declaration"], "erdos_940") + + def test_a_manifest_from_another_schema_version_is_refused(self): + payload = a_manifest().to_json_object() + payload["schema_version"] = 99 + with self.assertRaises(SystemExit): + ProblemManifest.from_json_object(payload) + + def test_hole_declaration_is_the_text_the_module_carries(self): + hole = DefinitionHole(name="t_answer", type="Prop") + self.assertEqual( + hole.declaration(), "noncomputable def t_answer : Prop := sorry" + ) + + +class MarkedUpModuleTest(unittest.TestCase): + def test_the_module_stands_on_mathlib_alone(self): + self.assertTrue(A_MODULE.render().startswith("import Mathlib\n")) + + def test_the_module_carries_no_markers(self): + # The handed-over module is plain Lean: `@[eval_problem]` does not + # exist outside lean-eval, and the request's resolved holes already + # say where the declarations are. + rendered = A_MODULE.render() + self.assertNotIn("@[eval_problem]", rendered) + self.assertNotIn("-- @region", rendered) + + def test_regions_render_in_declaration_order(self): + # A hole is used by the statement below it, and both need the scope + # above them. + rendered = A_MODULE.render() + positions = [ + rendered.index(getattr(A_MODULE, region)) + for region in ("dependencies", "scope", "holes", "statement") + ] + self.assertEqual(positions, sorted(positions)) + + def test_an_empty_region_leaves_no_blank_gap(self): + module = MarkedUpModule( + dependencies="def f := 1", scope="", holes="", statement="theorem t : True" + ) + self.assertEqual( + module.render(), + "import Mathlib\n\ndef f := 1\n\ntheorem t : True\n", + ) + + +class SlugTest(unittest.TestCase): + def test_a_qualified_declaration_becomes_an_identifier(self): + # A Lake package name is an identifier, so the dots cannot survive. + self.assertEqual( + slug("erdos_940.variants.large_integers"), + "erdos_940_variants_large_integers", + ) + + + +class DeclarationSpanTest(unittest.TestCase): + """Spans are computed from the rendered text, exactly.""" + + def test_every_declaration_gets_the_span_of_its_own_text(self): + text = A_MODULE.render() + spans = declaration_spans(text, module_declarations(A_MODULE, a_manifest())) + lines = text.split("\n") + for span in spans: + with self.subTest(name=span["name"]): + sliced = "\n".join( + lines[span["startLine"] - 1 : span["endLine"]] + )[span["startColumn"] :] + self.assertTrue(sliced.startswith(("def", "noncomputable", "theorem"))) + + def test_a_body_appearing_twice_is_refused(self): + with self.assertRaisesRegex(SystemExit, "more than once"): + declaration_spans( + "def f := 1\ndef f := 1\n", [("f", "def f := 1", "def", None)] + ) + + def test_a_missing_body_is_refused(self): + with self.assertRaisesRegex(SystemExit, "not found"): + declaration_spans("def g := 1\n", [("f", "def f := 1", "def", None)]) + + def test_utf16_columns_count_supplementary_plane_pairs(self): + # 𝕜 is beyond the BMP: one codepoint, two UTF-16 units. An `.ilean` + # column after it disagrees with the codepoint column by one. + text = "def 𝕜x := 1\ntheorem t : True := trivial\n" + (span,) = declaration_spans( + text, [("t", "theorem t : True := trivial", "theorem", None)] + ) + self.assertEqual(span["startColumn"], span["utf16StartColumn"]) + line = "abc𝕜 def f := 1" + self.assertEqual(_utf16_column(line, 5), 6) + + +class BuildProblemTest(unittest.TestCase): + def test_the_problem_satisfies_the_contract_shape(self): + problem, ilean = build_problem(A_MODULE, a_manifest(), a_policy()) + self.assertEqual(problem["id"], "erdos_940") + self.assertEqual(problem["group"], "open-conjectures") + self.assertEqual(problem["moduleName"], "erdos_940") + self.assertEqual( + problem["holes"], ["erdos_940_answer", "erdos_940"] + ) + self.assertEqual(problem["moduleContent"], A_MODULE.render()) + kinds = [hole["kind"] for hole in problem["resolvedHoles"]] + self.assertEqual(kinds, ["def", "theorem"]) + # Helpers are `.ilean` material, not holes. + self.assertIn("Foo.bar", ilean) + self.assertNotIn( + "Foo.bar", [hole["declarationName"] for hole in problem["resolvedHoles"]] + ) + + def test_the_theorem_hole_carries_the_copied_dependencies(self): + problem, _ = build_problem(A_MODULE, a_manifest(), a_policy()) + theorem = problem["resolvedHoles"][-1] + self.assertEqual(theorem["sameModuleDependencies"], ["Foo.bar"]) + self.assertEqual(problem["resolvedHoles"][0]["sameModuleDependencies"], []) + + def test_a_non_problem_category_is_refused(self): + with self.assertRaises(SystemExit): + build_problem(A_MODULE, a_manifest(category="API"), a_policy()) + + def test_the_category_rides_along_as_a_tag(self): + problem, _ = build_problem(A_MODULE, a_manifest(category="research solved"), a_policy()) + self.assertIn("research-solved", problem["tags"]) + + def test_a_set_override_keeps_a_solved_member_in_its_set(self): + # The frozen list is immutable while its members keep getting + # solved, so the set decides the tab and the tag says which are + # solved (formal-conjectures#5075). + problem, _ = build_problem( + A_MODULE, + a_manifest(category="research solved"), + a_policy(group="open-conjectures"), + ) + self.assertEqual(problem["group"], "open-conjectures") + + def test_a_set_override_does_not_admit_a_non_problem(self): + with self.assertRaises(SystemExit): + build_problem( + A_MODULE, a_manifest(category="API"), a_policy(group="open-conjectures") + ) + + +class BuildRequestTest(unittest.TestCase): + def test_the_request_carries_the_targets_pins(self): + problem, _ = build_problem(A_MODULE, a_manifest(), a_policy()) + request = build_request([problem], a_target(), "-- test", "context") + self.assertEqual(request["schemaVersion"], 1) + self.assertEqual(request["leanToolchain"], "leanprover/lean4:v4.33.0") + self.assertEqual(request["mathlib"]["rev"], "f" * 40) + self.assertEqual(request["templates"]["workspaceTest"], "-- test") + + def test_duplicate_ids_are_refused(self): + problem, _ = build_problem(A_MODULE, a_manifest(), a_policy()) + with self.assertRaisesRegex(SystemExit, "duplicate workspace id"): + build_request([problem, problem], a_target(), "", "context") + + +class ParseResponseTest(unittest.TestCase): + def _response(self, content="hello", **entry_overrides): + import hashlib + import json + + entry = { + "problemId": "p", + "path": "a.txt", + "sha256": hashlib.sha256(content.encode()).hexdigest(), + "content": "hello", + } + entry.update(entry_overrides) + return json.dumps({"schemaVersion": 1, "files": [entry]}) + + def test_a_traversal_path_is_refused(self): + for path in ("../outside.txt", "a/../../b.txt", "/etc/x", "a//b.txt", + "./a.txt", "a\\b.txt", "C:whatever"): + with self.subTest(path=path): + with self.assertRaisesRegex(SystemExit, "response path"): + parse_response(self._response(path=path)) + + def test_the_sidecar_name_is_refused(self): + # A response naming fc-provenance.json would silently lose to the + # sidecar written after it — and its recorded digest would then + # describe bytes no longer on disk. + with self.assertRaisesRegex(SystemExit, "provenance sidecar"): + parse_response(self._response(path="fc-provenance.json")) + + def test_unknown_response_keys_are_refused(self): + import json + + payload = json.loads(self._response()) + payload["extra"] = True + with self.assertRaisesRegex(SystemExit, "unknown keys"): + parse_response(json.dumps(payload)) + + def test_unknown_entry_keys_are_refused(self): + with self.assertRaisesRegex(SystemExit, "unknown keys"): + parse_response(self._response(mode="0755")) + + def test_a_missing_entry_field_is_a_refusal_not_a_crash(self): + import json + + payload = json.loads(self._response()) + del payload["files"][0]["sha256"] + with self.assertRaisesRegex(SystemExit, "has no sha256"): + parse_response(json.dumps(payload)) + + def test_non_json_is_a_refusal_not_a_crash(self): + with self.assertRaisesRegex(SystemExit, "not JSON"): + parse_response("lake build output\n{") + + def test_the_returned_workspaces_must_be_the_requested_ones(self): + with self.assertRaisesRegex(SystemExit, "returned no files for q"): + parse_response(self._response(), expected_ids=["p", "q"]) + with self.assertRaisesRegex(SystemExit, "nothing requested"): + parse_response(self._response(), expected_ids=[]) + + def test_a_good_response_yields_the_file_map(self): + self.assertEqual(parse_response(self._response()), {"p": {"a.txt": "hello"}}) + + def test_a_damaged_digest_is_refused(self): + with self.assertRaisesRegex(SystemExit, "does not match"): + parse_response(self._response(content="tampered")) + + def test_an_unknown_schema_version_is_refused(self): + with self.assertRaisesRegex(SystemExit, "schema version"): + parse_response('{"schemaVersion": 2, "files": []}') + + +class ProvenanceSidecarTest(unittest.TestCase): + """The sidecar is the schema-version-1 provenance boundary: strict, deterministic, digested.""" + + def test_digests_round_trip(self): + bound = a_manifest().with_digests("a" * 64, {"Challenge.lean": "b" * 64, "A.lean": "c" * 64}) + again = ProblemManifest.from_json(bound.to_json()) + self.assertEqual(again.module_sha256, "a" * 64) + self.assertEqual(dict(again.file_sha256), {"A.lean": "c" * 64, "Challenge.lean": "b" * 64}) + + def test_serialisation_is_key_sorted(self): + text = a_manifest().with_digests("a" * 64, {"b": "1" * 64, "a": "2" * 64}).to_json() + keys = [line.split('"')[1] for line in text.splitlines() if line.startswith(' "')] + self.assertEqual(keys, sorted(keys)) + + def test_unknown_keys_are_refused(self): + payload = a_manifest().to_json_object() + payload["notes"] = "anything" + with self.assertRaises(SystemExit): + ProblemManifest.from_json_object(payload) + + def test_unknown_digest_keys_are_refused(self): + payload = a_manifest().with_digests("a" * 64, {}).to_json_object() + payload["digests"]["blake3"] = "d" * 64 + with self.assertRaises(SystemExit): + ProblemManifest.from_json_object(payload) + + def test_the_request_digest_survives_a_round_trip(self): + bound = a_manifest().with_digests("a" * 64, {}, request_sha256="d" * 64) + loaded = ProblemManifest.from_json(bound.to_json()) + self.assertEqual(loaded.request_sha256, "d" * 64) + + +class ProblemGroupTest(unittest.TestCase): + """Categories map to lean-eval groups; non-problems are refused.""" + + def _manifest(self, category): + manifest = mock.Mock() + manifest.category = category + manifest.id = "some_problem" + return manifest + + def test_open_research_is_an_open_conjecture(self): + self.assertEqual( + problem_group(self._manifest("research open")), + "open-conjectures", + ) + + def test_settled_statements_are_evaluation_material(self): + for category in ("research solved", "textbook", "test"): + with self.subTest(category=category): + self.assertEqual( + problem_group(self._manifest(category)), + "formalization-evaluation", + ) + + def test_api_and_untagged_declarations_are_refused(self): + for category in ("API", ""): + with self.subTest(category=category): + with self.assertRaises(SystemExit): + problem_group(self._manifest(category)) + + +class StatementPrefixSpanTest(unittest.TestCase): + def test_the_span_starts_at_the_declaration_keyword(self): + from leaneval_interface import module_declarations + + module = MarkedUpModule( + dependencies="def Foo.bar := 1", + scope="", + holes="", + statement="open scoped Classical in\ntheorem t : True := by\n sorry", + dependency_declarations=(("Foo.bar", "def Foo.bar := 1"),), + ) + manifest = a_manifest( + theorem="t", qualified_theorem="t", holes=(), apply_arguments=() + ) + *_, statement_entry = module_declarations(module, manifest) + self.assertTrue(statement_entry[1].startswith("theorem t")) + self.assertNotIn("Classical in", statement_entry[1]) + +def a_producer(**overrides): + fields = { + "importer_commit": "9" * 40, + "importer_dirty": False, + "generator_repository": "https://github.com/leanprover/lean-eval-generator", + "generator_rev": "7" * 40, + "contract_version": 1, + "target_lean_toolchain": "leanprover/lean4:v4.33.0", + "target_mathlib_revision": "6" * 40, + "target_comparator": "c" * 40, + "target_lean4export": "1" * 40, + } + fields.update(overrides) + return ProducerRecord(**fields) + + +class ProducerRecordTest(unittest.TestCase): + """The sidecar names what produced the artifact, and only that.""" + + def test_the_producer_survives_a_round_trip(self): + bound = a_manifest().with_producer(a_producer(importer_dirty=True)) + loaded = ProblemManifest.from_json(bound.to_json()) + self.assertEqual(loaded.producer, bound.producer) + self.assertTrue(loaded.producer.importer_dirty) + + def test_a_manifest_without_a_producer_stays_without_one(self): + loaded = ProblemManifest.from_json(a_manifest().to_json()) + self.assertIsNone(loaded.producer) + + def test_unknown_producer_keys_are_refused(self): + payload = a_manifest().with_producer(a_producer()).to_json_object() + payload["producer"]["generator"]["binary_path"] = "/tmp/gen" + with self.assertRaisesRegex(SystemExit, "unknown keys"): + ProblemManifest.from_json_object(payload) + + def test_unknown_copied_dependency_keys_are_refused(self): + payload = a_manifest().to_json_object() + payload["source"]["copied_dependencies"][0]["blob"] = "f" * 40 + with self.assertRaisesRegex(SystemExit, "unknown keys"): + ProblemManifest.from_json_object(payload) + + +class SeamDirectionTest(unittest.TestCase): + """The arrow points one way, and this is the assertion OWNERSHIP.md cites.""" + + def test_the_cli_plumbing_does_not_import_the_importer(self): + # `leaneval_generator_cli` runs the pinned binary and nothing else. If + # it grew an importer import, the seam would still work and the + # ownership split would quietly stop being true. + import ast + import pathlib + + source = ( + pathlib.Path(__file__).with_name("leaneval_generator_cli.py") + ).read_text(encoding="utf-8") + imported = set() + for node in ast.walk(ast.parse(source)): + if isinstance(node, ast.Import): + imported.update(alias.name for alias in node.names) + elif isinstance(node, ast.ImportFrom) and node.module: + imported.add(node.module) + self.assertNotIn("fc_leaneval_importer", imported) + self.assertNotIn("fc_source", imported) + self.assertIn("leaneval_interface", imported) + + +if __name__ == "__main__": + unittest.main() diff --git a/comparator/adapter/test_make_comparator_workspace.py b/comparator/adapter/test_make_comparator_workspace.py new file mode 100644 index 0000000000..d32a4eff4b --- /dev/null +++ b/comparator/adapter/test_make_comparator_workspace.py @@ -0,0 +1,243 @@ +# Copyright 2026 The Formal Conjectures Authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""Tests for the command that runs the importer and then the generator. + +The case that matters here is the seam itself: what this repository hands over +has to be enough. If a workspace cannot be generated from the emitted request +and context directory alone, then some of the interface is still travelling +inside the process, and the pinned `lean-eval-generator` binary could not +reproduce this command's output. +""" + +import json +import os +import pathlib +import shutil +import tempfile +import unittest + +import leaneval_generator_cli as generator_cli +from make_comparator_workspace import ( + CONTEXT_DIR, + generate_workspaces, + seam_files, + write_tree, +) +from leaneval_interface import dump_json +from test_leaneval_interface import A_MODULE, a_manifest + + +class SeamFilesTest(unittest.TestCase): + def test_the_emitted_files_are_the_request_its_context_and_provenance(self): + _, files = seam_files([(A_MODULE, a_manifest())]) + self.assertEqual( + sorted(files), + [ + f"{CONTEXT_DIR}/.lake/build/lib/lean/erdos_940.ilean", + f"{CONTEXT_DIR}/erdos_940.lean", + "fc-provenance-erdos_940.json", + "request.json", + ], + ) + + def test_the_request_names_a_relative_context_root(self): + # The emitted artifact must be reproducible from any path, so the + # request cannot bake in where this machine staged it. + request, _ = seam_files([(A_MODULE, a_manifest())]) + self.assertEqual(request["contextRoot"], CONTEXT_DIR) + + def test_the_context_module_is_the_request_module_byte_for_byte(self): + # The generator refuses a request whose `moduleContent` differs from + # the file at the context root; emitting both from one value is what + # makes that check pass by construction. + request, files = seam_files([(A_MODULE, a_manifest())]) + self.assertEqual( + files[f"{CONTEXT_DIR}/erdos_940.lean"], + request["problems"][0]["moduleContent"], + ) + + def test_the_ilean_carries_every_declaration(self): + _, files = seam_files([(A_MODULE, a_manifest())]) + decls = json.loads( + files[f"{CONTEXT_DIR}/.lake/build/lib/lean/erdos_940.ilean"] + )["decls"] + self.assertEqual( + sorted(decls), + ["Foo.bar", "erdos_940", "erdos_940_answer"], + ) + + def test_the_provenance_sidecar_is_the_manifest(self): + # The schema-version-1 wire format has no provenance fields, so the FC source + # commit and declaration id §10 requires travel beside the request. + _, files = seam_files([(A_MODULE, a_manifest())]) + payload = json.loads(files["fc-provenance-erdos_940.json"]) + self.assertEqual(payload["source"]["commit"], "a" * 40) + self.assertEqual(payload["source"]["declaration"], "erdos_940") + + def test_two_problems_with_one_id_are_refused(self): + with self.assertRaisesRegex(SystemExit, "duplicate workspace id"): + seam_files([(A_MODULE, a_manifest()), (A_MODULE, a_manifest())]) + + +class WriteTreeTest(unittest.TestCase): + def test_existing_directory_is_not_overwritten(self): + with tempfile.TemporaryDirectory() as tmp: + target = pathlib.Path(tmp) / "ws" + target.mkdir() + with self.assertRaisesRegex(SystemExit, "refusing to overwrite"): + write_tree(target, {"a.txt": "a"}) + + def test_failed_write_leaves_no_partial_directory(self): + with tempfile.TemporaryDirectory() as tmp: + target = pathlib.Path(tmp) / "ws" + files = {"a.txt": "a", "b.txt": None} # None: write_text raises + with self.assertRaises(Exception): + write_tree(target, files) + self.assertFalse(target.exists()) + self.assertEqual(list(pathlib.Path(tmp).iterdir()), []) + + +@unittest.skipUnless( + os.environ.get(generator_cli.BINARY_ENV) or shutil.which(generator_cli.BINARY_NAME), + "pinned lean-eval-generator binary not available", +) +class PinnedGeneratorTest(unittest.TestCase): + """End to end against the real pinned binary, when one is built. + + CI builds the revision `comparator/tools.toml` pins and exports + `LEAN_EVAL_GENERATOR_BIN`; locally the test is skipped unless you have + done the same. + """ + + EXPECTED_FILES = [ + "Challenge.lean", + "ChallengeDeps.lean", + "README.md", + "Solution.lean", + "Submission.lean", + "Submission/Helpers.lean", + "WorkspaceTest.lean", + "config.json", + "fc-provenance.json", + "holes.json", + "lakefile.toml", + "lean-toolchain", + ] + + def test_a_workspace_generates_and_the_seam_reproduces_it(self): + with tempfile.TemporaryDirectory() as tmp: + out = pathlib.Path(tmp) / "out" + (workspace,) = generate_workspaces([(A_MODULE, a_manifest())], out) + written = sorted( + str(p.relative_to(workspace)) + for p in workspace.rglob("*") + if p.is_file() + ) + self.assertEqual(written, self.EXPECTED_FILES) + # The definition hole reaches the config, and the delegation is + # reducible in the Solution. + config = json.loads((workspace / "config.json").read_text()) + self.assertEqual(config["definition_names"], ["erdos_940_answer"]) + self.assertIn( + "@[reducible] noncomputable def erdos_940_answer", + (workspace / "Solution.lean").read_text(), + ) + + def test_the_emitted_request_yields_identical_digests(self): + # The seam is real only if the emitted bytes regenerate the same + # workspace: run the binary on the emitted request, from inside the + # emitted directory, and compare content digests per file. + request, files = seam_files([(A_MODULE, a_manifest())]) + with tempfile.TemporaryDirectory() as tmp: + root = pathlib.Path(tmp) + for relative, content in files.items(): + path = root / relative + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(content, encoding="utf-8") + # The emitted request IS what generation runs: the same bytes, + # resolved from inside the emitted directory. + request_text = (root / "request.json").read_text(encoding="utf-8") + self.assertEqual(request_text, dump_json(request)) + first = generator_cli.generate(request_text, cwd=root) + second = generator_cli.generate(request_text, cwd=root) + self.assertEqual(first, second) + self.assertEqual(sorted(first), ["erdos_940"]) + + + +class SubsetTest(unittest.TestCase): + def test_the_open_set_lists_one_hundred_declarations(self): + from make_comparator_workspace import subset_declarations + + names = subset_declarations("FC100OpenSet1") + self.assertEqual(len(names), 100) + self.assertIn("OeisA308734.conjecture", names) + self.assertIn("Erdos125.erdos_125.variants.positive_unequal_density", names) + + def test_a_missing_subset_is_refused(self): + from make_comparator_workspace import subset_declarations + + with self.assertRaises(SystemExit): + subset_declarations("NoSuchSet") + + +class KnownFailuresTest(unittest.TestCase): + def _load(self, text): + from known_failures import load_known_failures + + with tempfile.NamedTemporaryFile("w", suffix=".toml", delete=False) as f: + f.write(text) + name = f.name + try: + return load_known_failures(name) + finally: + os.unlink(name) + + def test_entries_are_keyed_by_declaration(self): + failures = self._load( + '[[failure]]\ndeclaration = "A.b"\nstage = "source"\nreason = "x"\n' + ) + self.assertEqual(failures["A.b"]["stage"], "source") + + def test_an_unknown_stage_is_refused(self): + with self.assertRaises(SystemExit): + self._load( + '[[failure]]\ndeclaration = "A.b"\nstage = "later"\nreason = "x"\n' + ) + + def test_a_missing_field_is_refused(self): + with self.assertRaises(SystemExit): + self._load('[[failure]]\ndeclaration = "A.b"\nstage = "source"\n') + + def test_an_unknown_key_is_refused(self): + # A typo'd key would otherwise ride along invisibly. + with self.assertRaisesRegex(SystemExit, "unknown keys: workspce"): + self._load( + '[[failure]]\ndeclaration = "A.b"\nstage = "source"\n' + 'reason = "x"\nworkspce = "A_b"\n' + ) + + def test_a_duplicate_declaration_is_refused(self): + # Last-one-wins would shadow an entry and quietly defeat the exact + # match the gates promise. + with self.assertRaisesRegex(SystemExit, "recorded twice"): + self._load( + '[[failure]]\ndeclaration = "A.b"\nstage = "source"\nreason = "x"\n' + '[[failure]]\ndeclaration = "A.b"\nstage = "source"\nreason = "y"\n' + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/comparator/known_failures.toml b/comparator/known_failures.toml new file mode 100644 index 0000000000..622a029ee8 --- /dev/null +++ b/comparator/known_failures.toml @@ -0,0 +1,10 @@ +# Declarations the whole-set audit is expected to fail on, each with the +# reason and the stage it fails at. `--known-failures` asserts this list +# exactly: an unexpected failure and a silently fixed one both fail the run, +# because a gate that only ever passes proves nothing. +# +# declaration the qualified FC declaration name +# workspace the workspace id, for the target-stage compile report +# stage "source" (import or --verify at FC pins) or +# "target" (compile at LeanEval pins) +# reason what fails and why it is not fixed here diff --git a/comparator/problems/Erdos340.erdos_340.variants.co_density_zero_sub.toml b/comparator/problems/Erdos340.erdos_340.variants.co_density_zero_sub.toml new file mode 100644 index 0000000000..ceecc4f228 --- /dev/null +++ b/comparator/problems/Erdos340.erdos_340.variants.co_density_zero_sub.toml @@ -0,0 +1,18 @@ +# Lean erases the value of the opaque theorem used inside +# `Finset.greedySidon.go`'s generated proof constant. The compiled dependency +# graph therefore cannot recover this source-only reference, but the copied +# definition body still names it and needs its statement to elaborate. +id = "Erdos340.erdos_340.variants.co_density_zero_sub" +declaration = "Erdos340.erdos_340.variants.co_density_zero_sub" + +[[copy_dependencies]] +declaration = "IsSidon.insert" +module = "FormalConjecturesForMathlib/Combinatorics/Basic.lean" + +[[copy_dependencies]] +declaration = "Finset.IsSidon.insert_ge_max'" +module = "FormalConjecturesForMathlib/Combinatorics/Basic.lean" + +[[copy_dependencies]] +declaration = "Finset.IsSidon.exists_insert_ge" +module = "FormalConjecturesForMathlib/Combinatorics/Basic.lean" diff --git a/comparator/problems/arithmetic_sum_s_conjecture_1_1.toml b/comparator/problems/arithmetic_sum_s_conjecture_1_1.toml new file mode 100644 index 0000000000..49dcb6ff29 --- /dev/null +++ b/comparator/problems/arithmetic_sum_s_conjecture_1_1.toml @@ -0,0 +1,3 @@ +id = "arithmetic_sum_s_conjecture_1_1" +declaration = "conjecture_1_1" +module = "FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean" diff --git a/comparator/problems/margulis_conjecture_1_1.toml b/comparator/problems/margulis_conjecture_1_1.toml new file mode 100644 index 0000000000..49e821b185 --- /dev/null +++ b/comparator/problems/margulis_conjecture_1_1.toml @@ -0,0 +1,6 @@ +# `conjecture_1_1` is declared by two files. Without `module` the generator +# refuses rather than picking one, so each needs its own manifest and its own +# `id`; the id is what names the workspace directory. +id = "margulis_conjecture_1_1" +declaration = "conjecture_1_1" +module = "FormalConjectures/Arxiv/2504.17644/Margulis.lean" diff --git a/comparator/templates/WorkspaceTest.lean b/comparator/templates/WorkspaceTest.lean new file mode 100644 index 0000000000..a231373e04 --- /dev/null +++ b/comparator/templates/WorkspaceTest.lean @@ -0,0 +1,37 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Lean + +open Lean + +/-- Run comparator on this workspace's `config.json`, so that `lake test` +is the check. Adapted from `leanprover/lean-eval`'s workspace test template. +The binary comes from `PATH`, or from `COMPARATOR_BIN`. -/ +def main : IO UInt32 := do + let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator" + try + let child ← IO.Process.spawn { + cmd := "lake" + args := #["env", comparatorBin, "config.json"] + } + child.wait + catch err => + IO.eprintln s!"Failed to run comparator via `{comparatorBin}`." + IO.eprintln "Install comparator, with landrun and lean4export, and put it \ +on PATH, or set COMPARATOR_BIN. See leanprover/comparator's README." + IO.eprintln s!"Original error: {err}" + pure 1 diff --git a/comparator/tools.toml b/comparator/tools.toml new file mode 100644 index 0000000000..8e6ff7e6b3 --- /dev/null +++ b/comparator/tools.toml @@ -0,0 +1,25 @@ +# The pinned external tools, one machine-readable source of truth. "At or +# after" prose is not a lock — and neither is a key nothing reads: every key +# in this file has a consumer in the adapter or in CI, and a key that loses +# its last consumer is deleted rather than kept for confidence. + +# Where a generated workspace is built and checked. These are LeanEval's pins, +# not this repository's: a workspace is vendored into lean-eval and built +# there, so it has to be buildable where it is going. The resolved component +# pins below are authoritative; there is deliberately no lean-eval commit +# here, because nothing could check the two statements against each other. +[target] +comparator_repository = "https://github.com/leanprover/comparator" +lean_toolchain = "leanprover/lean4:v4.33.0" +mathlib_revision = "6f1ef4e5dd604a435bddba4747b13970cd65d2a1" +mathlib_git = "https://github.com/leanprover-community/mathlib4.git" +comparator = "c0c5a52d2aff92b457c3e5ed4a68c1ebc5795809" +lean4export = "15f6055e299ad5b89345e533cc2192f4cc00f659" + +# The extracted generator this repository's requests are written against. +# `schemas/request-v1.schema.json` and `response-v1.schema.json` at this +# revision are the normative wire format; a bump here is a contract change +# and has to survive the seam round-trip test. +[generator] +repository = "https://github.com/leanprover/lean-eval-generator" +rev = "77373a539b31f8f304c852f288d7d8469cceebff" diff --git a/lakefile.toml b/lakefile.toml index 8cc37c76ba..2710a1a13b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -77,6 +77,17 @@ weak.linter.style.imports = true weak.google.answer = "postpone" +[[lean_lib]] +name = "ComparatorFacts" +srcDir = "comparator/adapter" + +[[lean_exe]] +name = "comparator_facts" +srcDir = "comparator/adapter" +root = "comparator_facts" +exeName = "comparator_facts" +supportInterpreter = true + [[lean_exe]] name = "extract_names" srcDir = "scripts"