verify

The verification report and the shared verifier: compile a candidate project in a sandbox and judge whether it compiles, is sorry-free, and is axiom-clean. Every prover funnels its output through the Verifier.

Verifier

class open_atp.verify.Verifier(backend: ComputeBackend, *, timeout_s: int = 600)

Compiles projects in a ComputeBackend and reports their status.

Shared by every prover for the final compile/sorry/axiom check. Use docker_verifier() or modal_verifier() for the common cases.

Parameters:

backendComputeBackend

The sandbox the candidate project is compiled in. Its image carries the Lean toolchain + Mathlib pins every project is checked against.

timeout_sint, default 600

Wall-clock cap for the post-generation compile/axiom check, in seconds. Independent of a prover’s (larger) generation budget.

property image: Image

The image backend runs.

The compatibility contract every candidate project must match: the Lean toolchain and the locked Mathlib revision.

check_compatible(project: LeanProject) → None

Reject a project whose pins differ from the backend image’s.

Matches the project’s lean_toolchain against the image’s lean_toolchain, and its locked mathlib_rev (when the project records one) against the image’s mathlib_rev. Raises ToolchainMismatch or MathlibRevMismatch on the first mismatch.

Parameters:

projectLeanProject

The candidate project whose toolchain (and locked Mathlib revision, when recorded) must match the backend image’s pins.

Raises:

ToolchainMismatch

If the project’s toolchain differs from the image’s.

MathlibRevMismatch

If the project records a Mathlib revision that differs from the image’s.

Examples

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.images import Image
>>> from open_atp.lean import LeanProject
>>> from open_atp.verify import Verifier
>>> root = Path(tempfile.mkdtemp())
>>> _ = (root / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (root / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> project = LeanProject(root)

A matching pin passes silently:

>>> image = Image(lean_toolchain="leanprover/lean4:v4.31.0")
>>> ok = Verifier(DockerBackend(image=image))
>>> ok.check_compatible(project)

A differing pin is rejected up front:

>>> bad = Verifier(DockerBackend(image=Image()))
>>> bad.check_compatible(project)
Traceback (most recent call last):
    ...
open_atp.lean.ToolchainMismatch: Project pins ...

verify(project: LeanProject, *, session: ComputeSession | None = None) → VerificationReport | None

Compile project and return a VerificationReport.

With no session the compile spins up its own sandbox via backend.run. Passing a live session runs the compile in that already-hot sandbox instead, avoiding a second spin-up.

Parameters:

projectLeanProject

The candidate project to compile. Checked for compatibility first.

sessionComputeSession, optional

A live, already-hot sandbox to compile in. When None (the default), backend.run spins up a fresh sandbox for this compile.

Returns:

VerificationReport or None

The compile/sorry/axiom verdict or None if the compile exceeds the verifier’s wall-clock timeout. A project with no .lean files automatically passes.

Raises:

ToolchainMismatch

If the project’s pins differ from the backend image’s (via check_compatible()).

MathlibRevMismatch

If the project’s locked Mathlib revision differs from the image’s.

Examples

A project with no .lean files short-circuits to a trivial passing report without touching the sandbox:

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.images import Image
>>> from open_atp.lean import LeanProject
>>> from open_atp.verify import Verifier
>>> root = Path(tempfile.mkdtemp())
>>> _ = (root / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (root / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> image = Image(lean_toolchain="leanprover/lean4:v4.31.0")
>>> verifier = Verifier(DockerBackend(image=image))
>>> report = verifier.verify(LeanProject(root))
>>> report.verified
True

Report

class open_atp.verify.VerificationReport(compiles: bool, sorry_free: bool, axioms: tuple[str, ...] = (), compile_log: str = '', per_file: dict[str, bool] = <factory>)

Result of compiling a candidate project in a sandbox.

Produced by Verifier and shared by every prover, including Aristotle.

Parameters:

compilesbool

Whether the whole project built successfully.

sorry_freebool

Whether the build is free of sorry (no incomplete proofs remain).

axiomstuple[str, …], default ()

Every axiom the compiled project depends on, as reported by Lean.

compile_logstr, default “”

The full build log. Omitted from to_dict().

per_filedict[str, bool], optional

Per-file compile status, keyed by file path relative to the project root. Defaults to an empty mapping.

property non_standard_axioms: tuple[str, ...]

The depended-on axioms outside STANDARD_AXIOMS.

Notably sorryAx, whose presence means the proof is not actually complete.

property verified: bool

Whether the project compiles, has no sorry, and no foreign axioms.

True iff compiles and sorry_free both hold and the project depends on no axioms outside STANDARD_AXIOMS.

to_dict() → dict[str, object]

JSON-ready summary (the full compile_log is intentionally omitted).

Returns:

dict[str, object]

The verdict (verified/compiles/sorry_free), the axiom lists, and per_file; compile_log is excluded.

Standard Verifiers

open_atp.verify.docker_verifier(image: Image = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0')) → Verifier

A Verifier backed by a local Docker sandbox running image.

Parameters:

imageImage, default DEFAULT_IMAGE

The image whose Lean toolchain + Mathlib pins projects are checked against.

Returns:

Verifier

A verifier over a DockerBackend.

open_atp.verify.modal_verifier(image: Image = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0')) → Verifier

A Verifier backed by a Modal Sandbox running the published image.

Needs Modal credentials and the image published via open-atp build-modal-image. The image’s :tag is dropped for the Modal name lookup.

Parameters:

imageImage, default DEFAULT_IMAGE

The published image whose Lean toolchain + Mathlib pins projects are checked against.

Returns:

Verifier

A verifier over a ModalBackend.

Axioms

open_atp.verify.STANDARD_AXIOMS = frozenset({'Classical.choice', 'Quot.sound', 'propext'})

frozenset() -> empty frozenset object frozenset(iterable) -> frozenset object

Build an immutable unordered collection of unique elements.