Skip to content

Asynchronous Submission and Retrieval

This guide covers the process of submitting a proof for verification without waiting for the result, and then retrieving the result later. This is useful for long-running proofs or for integrating into job queue systems.

Synchronous Client

The synchronous client allows you to submit a proof and then poll for the result at a later time.

API Reference: submit and get_result

First, client.submit() sends a proof to the server and returns a Proof object, which acts as a handle for the verification job. Then, client.get_result() uses this handle to fetch the result.

Function Signatures

def submit(
    self,
    proof: str | Path | os.PathLike,
    config: ProofConfig | None = None
) -> Proof:

def get_result(self, proof: Proof) -> ProofResult:

Parameters

  • submit.proof (str | Path | os.PathLike): The proof content to be verified (string, pathlib.Path, or path string).
  • submit.config (ProofConfig | None, optional): Configuration for the verification. See Proof Configuration for details.
  • get_result.proof (Proof): The Proof object returned by the submit method.

Returns

  • submit: Returns a Proof object containing metadata about the submitted job, including its unique ID.
  • get_result: Returns a ProofResult object with the full verification result.

Example

Submitting a proof and getting the result

The following example shows how to submit a proof and then retrieve its result. Note that in a real-world application, you might add a delay or a retry mechanism between submission and result retrieval.

import time
from lean_runner import LeanClient

with LeanClient("http://localhost:8000") as client:
    proof_content = (
        "import Mathlib.Tactic.NormNum\n"
        "theorem test : 2 + 2 = 4 := by norm_num"
    )

    # Submit the proof
    submitted_proof = client.submit(proof_content)
    print(f"Proof submitted with ID: {submitted_proof.id}")

    # Retrieve the result later
    # In a real scenario, you might wait here
    result = client.get_result(submitted_proof)
    print(result.model_dump_json(indent=4))

    time.sleep(1)

    result = client.get_result(submitted_proof)
    print(result.model_dump_json(indent=4))

Proof submitted with ID: 019894b0-554f-76e0-93db-0df8e92271ab
{
    "success": null,
    "status": "pending",
    "result": null,
    "error_message": null
}
{
    "success": null,
    "status": "running",
    "result": null,
    "error_message": null
}
{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}

Asynchronous Client

The asynchronous client provides non-blocking methods to submit a proof and fetch its result, making it ideal for highly concurrent applications.

API Reference: submit and get_result

The client.submit() coroutine sends the proof, and client.get_result() fetches the outcome.

Function Signatures

async def submit(
    self,
    proof: str | Path | os.PathLike | AnyioPath,
    config: ProofConfig | None = None,
) -> Proof:

async def get_result(self, proof: Proof) -> ProofResult:

Parameters

  • submit.proof (str | Path | os.PathLike | AnyioPath): The proof content (string, pathlib.Path, anyio.Path, or path string).
  • submit.config (ProofConfig | None, optional): Verification configuration. See Proof Configuration.
  • get_result.proof (Proof): The Proof object returned by submit.

Returns

  • submit: A Proof object.
  • get_result: A ProofResult object.

Example

Asynchronous submit and retrieve

This example demonstrates the async workflow.

import asyncio
from lean_runner import AsyncLeanClient

async def main():
    async with AsyncLeanClient("http://localhost:8000") as client:
        proof_content = (
            "import Mathlib.Tactic.NormNum\n"
            "theorem test : 2 + 2 = 4 := by norm_num"
        )

        # Submit the proof without blocking
        submitted_proof = await client.submit(proof_content)
        print(f"Proof submitted with ID: {submitted_proof.id}")

        result = await client.get_result(submitted_proof)
        print(result.model_dump_json(indent=4))

        # Wait and retrieve the result
        await asyncio.sleep(1) # Simulate waiting
        result = await client.get_result(submitted_proof)
        print(result.model_dump_json(indent=4))

        await asyncio.sleep(1)
        result = await client.get_result(submitted_proof)
        print(result.model_dump_json(indent=4))

if __name__ == "__main__":
    asyncio.run(main())

Proof submitted with ID: 019894b2-bf2b-77b1-9f82-774234ce1ea8
{
    "success": null,
    "status": "pending",
    "result": null,
    "error_message": null
}
{
    "success": null,
    "status": "running",
    "result": null,
    "error_message": null
}
{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}