verify

The output types 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.

class open_atp.verify.VerificationReport(compiles, sorry_free, axioms=(), compile_log='', per_file=<factory>)

Result of compiling a candidate project in a sandbox.

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

Attributes:

compilesbool

Whether the whole project built successfully.

sorry_freebool

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

axiomstuple[str, …]

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

compile_logstr

The full build log. Omitted from to_dict().

per_filedict[str, bool]

Per-file compile status, keyed by file path relative to the project root.

non_standard_axiomstuple[str, …]

The axioms outside STANDARD_AXIOMS – notably sorryAx, which means the proof is not actually complete.

verifiedbool

True iff the project compiles, has no sorry, and no foreign axioms.

to_dict()

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

class open_atp.verify.ProofResult(prover, verification, output_dir, completed_files=<factory>, cost_usd=None, duration_s=None, metadata=<factory>, error=None)

What a prover returns from prove().

The prover writes its artifacts into the caller-chosen output_dir, laid out as output_dir/{wd,logs}/: wd is the completed lake project (the proof output) and logs is the run record (the streamed agent stdout.txt, stderr.txt, result.json, and any harness-specific rich logs). This object just records where those live, plus the verification verdict and run metadata.

Attributes:

proverstr

Name of the prover that produced this result.

verificationVerificationReport or None

The shared verification of the completed project, or None when the run failed before a candidate could be verified (see error).

output_dirpathlib.Path

The run’s output directory. Holds the wd (proof project) and logs_dir (run record) subdirectories the prover populated.

completed_filesdict[str, str]

The completed .lean sources, keyed by file path relative to the project root.

cost_usdfloat, optional

Estimated USD cost of the run. None when the prover does not report cost.

duration_sfloat, optional

Wall-clock duration of the run, in seconds.

metadatadict[str, object]

Harness-specific run metadata (token counts, run summaries, …).

errorstr, optional

Set when the prover raised before producing a result (Docker down, API error, toolchain mismatch). verification is None and success is False.

wdpathlib.Path

The completed proof project (output_dir/wd).

logs_dirpathlib.Path

The run’s logs directory (output_dir/logs).

successbool

True iff verification exists and is verified.

to_dict()

JSON-ready view: inline files, verification, cost, and artifact paths.

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.

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

A Verifier backed by a local Docker sandbox running image.

class open_atp.verify.Verifier(backend)

Compiles projects in a ComputeBackend and reports their status.

check_compatible(project)

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.

Examples

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.backends.docker import DockerBackend, DockerConfig
>>> 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(DockerConfig(image=image)))
>>> ok.check_compatible(project)

A differing pin is rejected up front:

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

property image

The image the backend runs – the compatibility contract projects match.

verify(project, *, session=None)

Compile project and return a VerificationReport.

Standalone (session is None) the compile spins up its own sandbox via backend.run – the path Aristotle and the split-backend case take. When a caller passes a live session (the agent/verify backend-reuse path), the compile runs in that already-hot sandbox instead, avoiding a second spin-up.

Examples

A real project compiles in the backend; 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, DockerConfig
>>> 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(DockerConfig(image=image)))
>>> report = verifier.verify(LeanProject(root))
>>> report.verified
True