Skip to content

Projects

Module: lean_interact.project

This module provides classes for managing Lean projects, including local directories and git repositories. It supports automatic building and dependency management using lake, and can be used to create temporary projects with specific configurations. It is useful for setting up Lean environments for development, testing, or running benchmarks without manual setup.

LocalProject dataclass 

LocalProject(
    *,
    directory: str | PathLike,
    lake_path: str | PathLike = "lake",
    auto_build: bool = True,
)

Bases: BaseProject

Configuration for using an existing local Lean project directory.

Examples:

# Use an existing local project
project = LocalProject(
    directory="/path/to/my/lean/project",
    auto_build=True  # Build the project automatically
)

config = LeanREPLConfig(project=project)

directory instance-attribute 

directory: str | PathLike

Path to the local Lean project directory.

lake_path class-attribute instance-attribute 

lake_path: str | PathLike = 'lake'

The path to the lake executable. Default is "lake", which assumes it is in the system PATH.

auto_build class-attribute instance-attribute 

auto_build: bool = True

Whether to automatically build the project after instantiation.

get_directory 

get_directory() -> str

Get the directory of the Lean project.

Source code in src/lean_interact/project.py 
45
46
47
48
49
def get_directory(self) -> str:
    """Get the directory of the Lean project."""
    if self.directory is None:
        raise ValueError("`directory` must be set")
    return str(Path(self.directory).resolve())

get_lean_version 

get_lean_version() -> str

The Lean version used by this project.

Source code in src/lean_interact/project.py 
51
52
53
54
55
56
def get_lean_version(self) -> str:
    """The Lean version used by this project."""
    version = get_project_lean_version(Path(self.get_directory()))
    if version is None:
        raise ValueError("Unable to determine Lean version")
    return version

build 

build(
    verbose: bool = True,
    update: bool = False,
    _lock: bool = True,
) -> None

Build the Lean project using lake. Args: verbose: Whether to print building information to the console. update: Whether to run lake update before building. _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).

Source code in src/lean_interact/project.py 
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
def build(self, verbose: bool = True, update: bool = False, _lock: bool = True) -> None:
    """Build the Lean project using lake.
    Args:
        verbose: Whether to print building information to the console.
        update: Whether to run `lake update` before building.
        _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).
    """
    directory = Path(self.get_directory())
    check_lake(self.lake_path)

    def _do_build():
        stdout = None if verbose else subprocess.DEVNULL
        stderr = None if verbose else subprocess.DEVNULL
        try:
            # Run lake update if requested
            if update:
                subprocess.run(
                    [str(self.lake_path), "update"], cwd=directory, check=True, stdout=stdout, stderr=stderr
                )

            # Try to get cache first (non-fatal if it fails)
            cache_result = subprocess.run(
                [str(self.lake_path), "exe", "cache", "get"],
                cwd=directory,
                check=False,
                stdout=stdout,
                stderr=stderr,
            )
            if cache_result.returncode != 0 and verbose:
                logger.info(
                    "Getting 'error: unknown executable cache' is expected if the project doesn't depend on Mathlib"
                )

            # Build the project (this must succeed)
            subprocess.run([str(self.lake_path), "build"], cwd=directory, check=True, stdout=stdout, stderr=stderr)
            logger.debug("Successfully built project at %s", directory)

        except subprocess.CalledProcessError as e:
            logger.error("Failed to build the project: %s", e)
            raise

    if _lock:
        with FileLock(f"{directory}.lock"):
            _do_build()
    else:
        _do_build()

GitProject dataclass 

GitProject(
    *,
    directory: str | PathLike | None = None,
    lake_path: str | PathLike = "lake",
    auto_build: bool = True,
    url: str,
    rev: str | None = None,
    force_pull: bool = False,
)

Bases: BaseProject

Configuration for using an online git repository containing a Lean project.

Examples:

# Clone and use a Git repository
project = GitProject(
    url="https://github.com/user/lean-project",
    rev="main",  # Optional: specific branch/tag/commit
    directory="/custom/cache/dir",  # Optional: custom directory
    force_pull=False  # Optional: force update on each use
)

config = LeanREPLConfig(project=project)

url instance-attribute 

url: str

The git URL of the repository to clone.

directory class-attribute instance-attribute 

directory: str | PathLike | None = field(default=None)

The directory where the git project will be cloned. If None, a unique path inside the default LeanInteract cache directory will be used.

rev class-attribute instance-attribute 

rev: str | None = None

The specific git revision (tag, branch, or commit hash) to checkout. If None, uses the default branch.

force_pull class-attribute instance-attribute 

force_pull: bool = False

Whether to force pull the latest changes from the remote repository, overwriting local changes.

lake_path class-attribute instance-attribute 

lake_path: str | PathLike = 'lake'

The path to the lake executable. Default is "lake", which assumes it is in the system PATH.

auto_build class-attribute instance-attribute 

auto_build: bool = True

Whether to automatically build the project after instantiation.

get_directory 

get_directory() -> str

Get the directory of the Lean project.

Source code in src/lean_interact/project.py 
45
46
47
48
49
def get_directory(self) -> str:
    """Get the directory of the Lean project."""
    if self.directory is None:
        raise ValueError("`directory` must be set")
    return str(Path(self.directory).resolve())

get_lean_version 

get_lean_version() -> str

The Lean version used by this project.

Source code in src/lean_interact/project.py 
51
52
53
54
55
56
def get_lean_version(self) -> str:
    """The Lean version used by this project."""
    version = get_project_lean_version(Path(self.get_directory()))
    if version is None:
        raise ValueError("Unable to determine Lean version")
    return version

build 

build(
    verbose: bool = True,
    update: bool = False,
    _lock: bool = True,
) -> None

Build the Lean project using lake. Args: verbose: Whether to print building information to the console. update: Whether to run lake update before building. _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).

Source code in src/lean_interact/project.py 
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
def build(self, verbose: bool = True, update: bool = False, _lock: bool = True) -> None:
    """Build the Lean project using lake.
    Args:
        verbose: Whether to print building information to the console.
        update: Whether to run `lake update` before building.
        _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).
    """
    directory = Path(self.get_directory())
    check_lake(self.lake_path)

    def _do_build():
        stdout = None if verbose else subprocess.DEVNULL
        stderr = None if verbose else subprocess.DEVNULL
        try:
            # Run lake update if requested
            if update:
                subprocess.run(
                    [str(self.lake_path), "update"], cwd=directory, check=True, stdout=stdout, stderr=stderr
                )

            # Try to get cache first (non-fatal if it fails)
            cache_result = subprocess.run(
                [str(self.lake_path), "exe", "cache", "get"],
                cwd=directory,
                check=False,
                stdout=stdout,
                stderr=stderr,
            )
            if cache_result.returncode != 0 and verbose:
                logger.info(
                    "Getting 'error: unknown executable cache' is expected if the project doesn't depend on Mathlib"
                )

            # Build the project (this must succeed)
            subprocess.run([str(self.lake_path), "build"], cwd=directory, check=True, stdout=stdout, stderr=stderr)
            logger.debug("Successfully built project at %s", directory)

        except subprocess.CalledProcessError as e:
            logger.error("Failed to build the project: %s", e)
            raise

    if _lock:
        with FileLock(f"{directory}.lock"):
            _do_build()
    else:
        _do_build()

TemporaryProject dataclass 

TemporaryProject(
    *,
    directory: str | PathLike | None = None,
    lake_path: str | PathLike = "lake",
    auto_build: bool = True,
    lean_version: str,
    verbose: bool = True,
    content: str,
    lakefile_type: Literal["lean", "toml"] = "lean",
)

Bases: BaseTempProject

Configuration for creating a temporary Lean project with custom lakefile content.

Examples:

# Create a temporary project with custom lakefile
project = TemporaryProject(
    lean_version="v4.19.0",
    content="""
import Lake
open Lake DSL

package "my_temp_project" where
version := v!"0.1.0"

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "v4.19.0"
""",
    lakefile_type="lean"  # or "toml"
)

config = LeanREPLConfig(project=project)

content instance-attribute 

content: str

The content to write to the lakefile (either lakefile.lean or lakefile.toml format).

lakefile_type class-attribute instance-attribute 

lakefile_type: Literal['lean', 'toml'] = 'lean'

The type of lakefile to create. Either 'lean' for lakefile.lean or 'toml' for lakefile.toml.

directory class-attribute instance-attribute 

directory: str | PathLike | None = field(default=None)

The directory where temporary Lean projects will be cached. If None, a unique path inside the default LeanInteract cache directory will be used.

lake_path class-attribute instance-attribute 

lake_path: str | PathLike = 'lake'

The path to the lake executable. Default is "lake", which assumes it is in the system PATH.

auto_build class-attribute instance-attribute 

auto_build: bool = True

Whether to automatically build the project after instantiation.

lean_version instance-attribute 

lean_version: str

The Lean version to use for this project.

verbose class-attribute instance-attribute 

verbose: bool = True

Whether to print additional information during the setup process.

get_directory 

get_directory() -> str

Get the directory of the Lean project.

Source code in src/lean_interact/project.py 
45
46
47
48
49
def get_directory(self) -> str:
    """Get the directory of the Lean project."""
    if self.directory is None:
        raise ValueError("`directory` must be set")
    return str(Path(self.directory).resolve())

get_lean_version 

get_lean_version() -> str

The Lean version used by this project.

Source code in src/lean_interact/project.py 
51
52
53
54
55
56
def get_lean_version(self) -> str:
    """The Lean version used by this project."""
    version = get_project_lean_version(Path(self.get_directory()))
    if version is None:
        raise ValueError("Unable to determine Lean version")
    return version

build 

build(
    verbose: bool = True,
    update: bool = False,
    _lock: bool = True,
) -> None

Build the Lean project using lake. Args: verbose: Whether to print building information to the console. update: Whether to run lake update before building. _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).

Source code in src/lean_interact/project.py 
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
def build(self, verbose: bool = True, update: bool = False, _lock: bool = True) -> None:
    """Build the Lean project using lake.
    Args:
        verbose: Whether to print building information to the console.
        update: Whether to run `lake update` before building.
        _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).
    """
    directory = Path(self.get_directory())
    check_lake(self.lake_path)

    def _do_build():
        stdout = None if verbose else subprocess.DEVNULL
        stderr = None if verbose else subprocess.DEVNULL
        try:
            # Run lake update if requested
            if update:
                subprocess.run(
                    [str(self.lake_path), "update"], cwd=directory, check=True, stdout=stdout, stderr=stderr
                )

            # Try to get cache first (non-fatal if it fails)
            cache_result = subprocess.run(
                [str(self.lake_path), "exe", "cache", "get"],
                cwd=directory,
                check=False,
                stdout=stdout,
                stderr=stderr,
            )
            if cache_result.returncode != 0 and verbose:
                logger.info(
                    "Getting 'error: unknown executable cache' is expected if the project doesn't depend on Mathlib"
                )

            # Build the project (this must succeed)
            subprocess.run([str(self.lake_path), "build"], cwd=directory, check=True, stdout=stdout, stderr=stderr)
            logger.debug("Successfully built project at %s", directory)

        except subprocess.CalledProcessError as e:
            logger.error("Failed to build the project: %s", e)
            raise

    if _lock:
        with FileLock(f"{directory}.lock"):
            _do_build()
    else:
        _do_build()

TempRequireProject dataclass 

TempRequireProject(
    *,
    directory: str | PathLike | None = None,
    lake_path: str | PathLike = "lake",
    auto_build: bool = True,
    lean_version: str,
    verbose: bool = True,
    require: Literal["mathlib"]
    | LeanRequire
    | list[LeanRequire | Literal["mathlib"]],
)

Bases: BaseTempProject

Configuration for setting up a temporary project with specific dependencies.

As Mathlib is a common dependency, you can just set require="mathlib" and a compatible version of mathlib will be used. This feature has been developed mostly to be able to run benchmarks using Mathlib as a dependency (such as ProofNet# or MiniF2F) without having to manually set up a Lean project.

Examples:

# Create a temporary project with Mathlib
project = TempRequireProject(
    lean_version="v4.19.0",
    require="mathlib"  # Shortcut for Mathlib
)

# Or with custom dependencies
project = TempRequireProject(
    lean_version="v4.19.0",
    require=[
        LeanRequire("mathlib", "https://github.com/leanprover-community/mathlib4.git", "v4.19.0"),
        LeanRequire("my_lib", "https://github.com/user/my-lib.git", "v1.0.0")
    ]
)

config = LeanREPLConfig(project=project)

require instance-attribute 

require: (
    Literal["mathlib"]
    | LeanRequire
    | list[LeanRequire | Literal["mathlib"]]
)

The dependencies to include in the project. Can be:

  • "mathlib" for automatic Mathlib dependency matching the Lean version
  • A single LeanRequire object for a custom dependency
  • A list of dependencies (mix of "mathlib" and LeanRequire objects)

directory class-attribute instance-attribute 

directory: str | PathLike | None = field(default=None)

The directory where temporary Lean projects will be cached. If None, a unique path inside the default LeanInteract cache directory will be used.

lake_path class-attribute instance-attribute 

lake_path: str | PathLike = 'lake'

The path to the lake executable. Default is "lake", which assumes it is in the system PATH.

auto_build class-attribute instance-attribute 

auto_build: bool = True

Whether to automatically build the project after instantiation.

lean_version instance-attribute 

lean_version: str

The Lean version to use for this project.

verbose class-attribute instance-attribute 

verbose: bool = True

Whether to print additional information during the setup process.

get_directory 

get_directory() -> str

Get the directory of the Lean project.

Source code in src/lean_interact/project.py 
45
46
47
48
49
def get_directory(self) -> str:
    """Get the directory of the Lean project."""
    if self.directory is None:
        raise ValueError("`directory` must be set")
    return str(Path(self.directory).resolve())

get_lean_version 

get_lean_version() -> str

The Lean version used by this project.

Source code in src/lean_interact/project.py 
51
52
53
54
55
56
def get_lean_version(self) -> str:
    """The Lean version used by this project."""
    version = get_project_lean_version(Path(self.get_directory()))
    if version is None:
        raise ValueError("Unable to determine Lean version")
    return version

build 

build(
    verbose: bool = True,
    update: bool = False,
    _lock: bool = True,
) -> None

Build the Lean project using lake. Args: verbose: Whether to print building information to the console. update: Whether to run lake update before building. _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).

Source code in src/lean_interact/project.py 
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
def build(self, verbose: bool = True, update: bool = False, _lock: bool = True) -> None:
    """Build the Lean project using lake.
    Args:
        verbose: Whether to print building information to the console.
        update: Whether to run `lake update` before building.
        _lock: (internal parameter) Whether to acquire a file lock (should be False if already locked by caller).
    """
    directory = Path(self.get_directory())
    check_lake(self.lake_path)

    def _do_build():
        stdout = None if verbose else subprocess.DEVNULL
        stderr = None if verbose else subprocess.DEVNULL
        try:
            # Run lake update if requested
            if update:
                subprocess.run(
                    [str(self.lake_path), "update"], cwd=directory, check=True, stdout=stdout, stderr=stderr
                )

            # Try to get cache first (non-fatal if it fails)
            cache_result = subprocess.run(
                [str(self.lake_path), "exe", "cache", "get"],
                cwd=directory,
                check=False,
                stdout=stdout,
                stderr=stderr,
            )
            if cache_result.returncode != 0 and verbose:
                logger.info(
                    "Getting 'error: unknown executable cache' is expected if the project doesn't depend on Mathlib"
                )

            # Build the project (this must succeed)
            subprocess.run([str(self.lake_path), "build"], cwd=directory, check=True, stdout=stdout, stderr=stderr)
            logger.debug("Successfully built project at %s", directory)

        except subprocess.CalledProcessError as e:
            logger.error("Failed to build the project: %s", e)
            raise

    if _lock:
        with FileLock(f"{directory}.lock"):
            _do_build()
    else:
        _do_build()

LeanRequire dataclass 

LeanRequire(name: str, git: str, rev: str | None = None)

Lean project dependency specification for lakefile.lean files.

name instance-attribute 

name: str

The name of the dependency package.

git instance-attribute 

git: str

The git URL of the dependency repository.

rev class-attribute instance-attribute 

rev: str | None = None

The specific git revision (tag, branch, or commit hash) to use. If None, uses the default branch.