Skip to main content
Pre-release

This release is a pre-release and may not be stable for production use.

Lean Server Package

This package contains the core lean-server application, a FastAPI-based server that provides a REST API for interacting with the Lean prover.

📖 Overview

The server is designed to be run inside the Docker environment provided at the root of this monorepo. It exposes endpoints to perform proof checking and other Lean-related tasks.

The main API endpoint is:

  • POST /prove/check: Accepts a proof and an optional config to run a proof.

⚙️ Configuration

The server's behavior can be configured via config.yaml. Key settings include:

  • Server host and port.
  • Lean process configuration.
  • Proof checking timeouts.

🚀 Running the Server

This package is intended to be run within the development container.

  1. Navigate to the Dev Container: Follow the instructions in the root README to set up the development environment.

  2. Install Dependencies: In the container's terminal, install the package in editable mode:

    uv pip install -e .
    

    (Note: The root setup installs this automatically).

  3. Start the Server: The pyproject.toml file defines a script entry point. You can start the server with the following command:

    lean-server
    

    By default, it should be available at http://localhost:8000.

Metadata

Release files for lmms-lean-server 0.0.1.dev4

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for lmms-lean-server 0.0.1.dev4
File Size Uploaded Provenance
lmms_lean_server-0.0.1.dev4.tar.gz 8.5 kB Without provenance Details

Built distribution (wheel)

Table of built distributions (wheels) for lmms-lean-server 0.0.1.dev4
File Interpreter ABI Platform
lmms_lean_server-0.0.1.dev4-py3-none-any.whl Python 3 none any Details

Total release size: 19.1 kB

Release files / lmms_lean_server-0.0.1.dev4.tar.gz

Download URL lmms_lean_server-0.0.1.dev4.tar.gz
Size 8.5 kB
Tags Source
SHA-256 checksum
How to use checksums
c6fbf1ee7828d1aefd6cc288ebec60f4b79718aee2e68f5ec582519b17268753
BLAKE2b-256 checksum
How to use checksums
4ff2ae63dd6d39c4f891d669beed57d30cdf0691787f68764eafb71fd2da7aef
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via uv/0.7.13

Release files / lmms_lean_server-0.0.1.dev4-py3-none-any.whl

Download URL lmms_lean_server-0.0.1.dev4-py3-none-any.whl
Size 10.6 kB
Tags Python 3
SHA-256 checksum
How to use checksums
c825cc2f5a537e5e670d2e8992190eece249e50e81ca9a44464f19ae2723ddec
BLAKE2b-256 checksum
How to use checksums
53faead69cc4b1f3198eebcade2325bbe5c7ee6839196df6ac1fcb58cfd65238
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via uv/0.7.13

Security for lmms-lean-server 0.0.1.dev4

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.

To learn more about protecting yourself from malicious actors, visit our package security documentation.

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page