Configuration

Module: lean_interact.config

This module provides the LeanREPLConfig class, which is used to configure the Lean REPL (Read-Eval-Print Loop) used by the Lean servers in lean_interact.server.

LeanREPLConfig

LeanREPLConfig(
    lean_version: str | None = None,
    project: BaseProject | None = None,
    repl_rev: str = DEFAULT_REPL_VERSION,
    repl_git: str = DEFAULT_REPL_GIT_URL,
    force_pull_repl: bool = False,
    cache_dir: str | PathLike = DEFAULT_CACHE_DIR,
    local_repl_path: str | PathLike | None = None,
    build_repl: bool = True,
    lake_path: str | PathLike = "lake",
    memory_hard_limit_mb: int | None = None,
    verbose: bool = False,
)

Initialize the Lean REPL configuration.

Parameters:

Name	Type	Description	Default
lean_version	str | None	The Lean version you want to use. Should only be set when project is None. When project is provided, the Lean version will be inferred from the project. Default is None, which means the latest available version will be selected if project is None.	None
project	BaseProject | None	The project you want to use. Options: - None: The REPL sessions will only depend on Lean and its standard library. - LocalProject: An existing local Lean project. - GitProject: A git repository with a Lean project that will be cloned. - TemporaryProject: A temporary Lean project with a custom lakefile that will be created. - TempRequireProject: A temporary Lean project with dependencies that will be created.	None
repl_rev	str	The REPL version / git revision you want to use. It is not recommended to change this value unless you know what you are doing. It will first attempt to checkout {repl_rev}_lean-toolchain-{lean_version}, and fallback to {repl_rev} if it fails. Note: Ignored when local_repl_path is provided.	DEFAULT_REPL_VERSION
repl_git	str	The git repository of the Lean REPL. It is not recommended to change this value unless you know what you are doing. Note: Ignored when local_repl_path is provided.	DEFAULT_REPL_GIT_URL
force_pull_repl	bool	If True, always pull the latest changes from the REPL git repository before checking out the revision. By default, it is False to limit hitting GitHub API rate limits.	False
cache_dir	str | PathLike	The directory where the Lean REPL will be cached. Default is inside the package directory.	DEFAULT_CACHE_DIR
local_repl_path	str | PathLike | None	A local path to the Lean REPL. This is useful if you want to use a local copy of the REPL. When provided, the REPL will not be downloaded from the git repository. This is particularly useful during REPL development.	None
build_repl	bool	Whether to build the local REPL before running it. This option is ignored when local_repl_path is not provided.	True
lake_path	str | PathLike	The path to the lake executable. Default is "lake", which assumes it is in the system PATH.	'lake'
memory_hard_limit_mb	int | None	The maximum memory usage in MB for the Lean server. Setting this value too low may lead to more command processing failures. Only available on Linux platforms. Default is None, which means no limit.	None
verbose	bool	Whether to print additional information during the setup process.	False

Examples:

# Basic configuration with default settings
config = LeanREPLConfig(verbose=True)

# Configuration with specific Lean version
config = LeanREPLConfig(lean_version="v4.19.0", verbose=True)

# Configuration with memory limits
config = LeanREPLConfig(memory_hard_limit_mb=2000)

# Configuration with custom REPL version and repository
config = LeanREPLConfig(
    repl_rev="v4.21.0-rc3",
    repl_git="https://github.com/leanprover-community/repl"
)

# Working with projects
config = LeanREPLConfig(
    project=LocalProject(directory="/path/to/project"),
    verbose=True
)

Source code in src/lean_interact/config.py

def __init__(
    self,
    lean_version: str | None = None,
    project: BaseProject | None = None,
    repl_rev: str = DEFAULT_REPL_VERSION,
    repl_git: str = DEFAULT_REPL_GIT_URL,
    force_pull_repl: bool = False,
    cache_dir: str | PathLike = DEFAULT_CACHE_DIR,
    local_repl_path: str | PathLike | None = None,
    build_repl: bool = True,
    lake_path: str | PathLike = "lake",
    memory_hard_limit_mb: int | None = None,
    verbose: bool = False,
):
    """
    Initialize the Lean REPL configuration.

    Args:
        lean_version:
            The Lean version you want to use. Should only be set when `project` is `None`.
            When `project` is provided, the Lean version will be inferred from the project.
            Default is `None`, which means the latest available version will be selected if `project` is `None`.
        project:
            The project you want to use. Options:
            - `None`: The REPL sessions will only depend on Lean and its standard library.
            - `LocalProject`: An existing local Lean project.
            - `GitProject`: A git repository with a Lean project that will be cloned.
            - `TemporaryProject`: A temporary Lean project with a custom lakefile that will be created.
            - `TempRequireProject`: A temporary Lean project with dependencies that will be created.
        repl_rev:
            The REPL version / git revision you want to use. It is not recommended to change this value unless you know what you are doing.
            It will first attempt to checkout `{repl_rev}_lean-toolchain-{lean_version}`, and fallback to `{repl_rev}` if it fails.
            Note: Ignored when `local_repl_path` is provided.
        repl_git:
            The git repository of the Lean REPL. It is not recommended to change this value unless you know what you are doing.
            Note: Ignored when `local_repl_path` is provided.
        force_pull_repl:
            If True, always pull the latest changes from the REPL git repository before checking out the revision.
            By default, it is `False` to limit hitting GitHub API rate limits.
        cache_dir:
            The directory where the Lean REPL will be cached.
            Default is inside the package directory.
        local_repl_path:
            A local path to the Lean REPL. This is useful if you want to use a local copy of the REPL.
            When provided, the REPL will not be downloaded from the git repository.
            This is particularly useful during REPL development.
        build_repl:
            Whether to build the local REPL before running it. This option is ignored when `local_repl_path` is not provided.
        lake_path:
            The path to the lake executable. Default is "lake", which assumes it is in the system PATH.
        memory_hard_limit_mb:
            The maximum memory usage in MB for the Lean server. Setting this value too low may lead to more command processing failures.
            Only available on Linux platforms.
            Default is `None`, which means no limit.
        verbose:
            Whether to print additional information during the setup process.

    Examples:
        ```python
        # Basic configuration with default settings
        config = LeanREPLConfig(verbose=True)

        # Configuration with specific Lean version
        config = LeanREPLConfig(lean_version="v4.19.0", verbose=True)

        # Configuration with memory limits
        config = LeanREPLConfig(memory_hard_limit_mb=2000)

        # Configuration with custom REPL version and repository
        config = LeanREPLConfig(
            repl_rev="v4.21.0-rc3",
            repl_git="https://github.com/leanprover-community/repl"
        )

        # Working with projects
        config = LeanREPLConfig(
            project=LocalProject(directory="/path/to/project"),
            verbose=True
        )
        ```
    """
    if project is not None and lean_version is not None:
        raise ValueError(
            "lean_version should only be set when project is None. When a project is provided, the Lean version is inferred from the project."
        )

    # Initialize basic configuration
    if lean_version:
        lean_version = parse_lean_version(lean_version)
        if lean_version is None:
            raise ValueError(f"Unable to parse Lean version format: `{lean_version}`")
    self.lean_version = lean_version
    self.project = project
    self.repl_git = repl_git
    self.repl_rev = repl_rev
    self.force_pull_repl = force_pull_repl
    self.cache_dir = Path(cache_dir)
    self.local_repl_path = Path(local_repl_path) if local_repl_path else None
    self.build_repl = build_repl
    self.memory_hard_limit_mb = memory_hard_limit_mb
    self.lake_path = Path(lake_path)
    self.verbose = verbose
    self._timeout_lock = 300

    if self.project is not None:
        self.lean_version = self.project.get_lean_version()
        if self.project.directory is None:
            raise ValueError("Project directory cannot be None")

    self._setup_repl()

lean_version instance-attribute

lean_version = lean_version

project instance-attribute

project = project

repl_git instance-attribute

repl_git = repl_git

repl_rev instance-attribute

repl_rev = repl_rev

force_pull_repl instance-attribute

force_pull_repl = force_pull_repl

cache_dir instance-attribute

cache_dir = Path(cache_dir)

local_repl_path instance-attribute

local_repl_path = (
    Path(local_repl_path) if local_repl_path else None
)

build_repl instance-attribute

build_repl = build_repl

memory_hard_limit_mb instance-attribute

memory_hard_limit_mb = memory_hard_limit_mb

lake_path instance-attribute

lake_path = Path(lake_path)

verbose instance-attribute

verbose = verbose

cache_repl_dir property

cache_repl_dir: str

Get the cache directory for the Lean REPL.

working_dir property

working_dir: str

Get the working directory, where the commands are executed.

get_available_lean_versions

get_available_lean_versions() -> list[str]

Get the available Lean versions for the selected REPL.

Source code in src/lean_interact/config.py

def get_available_lean_versions(self) -> list[str]:
    """
    Get the available Lean versions for the selected REPL.
    """
    return [commit[0] for commit in self._get_available_lean_versions()]

is_setup

is_setup() -> bool

Check if the Lean environment has been set up.

Source code in src/lean_interact/config.py

def is_setup(self) -> bool:
    """Check if the Lean environment has been set up."""
    return hasattr(self, "_cache_repl_dir") and self._cache_repl_dir is not None