Skip to content

Allows more granular config for an existing installation of Lake/Lean/REPL #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
vadimkantorov wants to merge 4 commits into from
Closed

Allows more granular config for an existing installation of Lake/Lean/REPL #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9ae2cc2
Make gitpython less required
vadimkantorov Apr 30, 2025
d1a8fbc
Syntax fixes
vadimkantorov Apr 30, 2025
1214125
Newline fix
vadimkantorov Apr 30, 2025
c6c03d0
Delete stray print
vadimkantorov Apr 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 18 additions & 5 deletions src/lean_interact/config.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@
from typing import Literal

from filelock import FileLock
from git import GitCommandError, Repo

from lean_interact.utils import (
DEFAULT_CACHE_DIR,
Expand Down Expand Up @@ -235,8 +234,7 @@ def _modify_lakefile(self, project_dir: str, lean_version: str) -> None:
with open(os.path.join(project_dir, "lakefile.lean"), "a", encoding="utf-8") as f:
for req in require:
f.write(f'\n\nrequire {req.name} from git\n "{req.git}"' + (f' @ "{req.rev}"' if req.rev else ""))



class LeanREPLConfig:
def __init__(
self,
Expand All @@ -247,6 +245,11 @@ def __init__(
cache_dir: str = DEFAULT_CACHE_DIR,
memory_hard_limit_mb: int | None = None,
verbose: bool = False,
setup: bool = True,
lake_env_repl_path : str | None = None,
working_dir : str | None = None,
lake_path : str = "lake",
lake_command : str = "env",
):
"""
Initialize the Lean REPL configuration.
Expand Down Expand Up @@ -303,11 +306,14 @@ def __init__(
"Lean 4 build system (`lake`) is not installed. You can try to run `install-lean` or find installation instructions here: https://leanprover-community.github.io/get_started.html"
)

self._setup_repl()
if setup:
self._setup_repl()

assert isinstance(self.lean_version, str)

if self.project is None:
if working_dir:
self._working_dir = working_dir
elif self.project is None:
self._working_dir = self._cache_repl_dir
else:
self.project._instantiate(
Expand All @@ -316,8 +322,14 @@ def __init__(
verbose=self.verbose,
)
self._working_dir = self.project._get_directory(cache_dir=self.cache_dir, lean_version=self.lean_version)

self.lake_env_repl_path = lake_env_repl_path or os.path.join(self._cache_repl_dir, ".lake", "build", "bin", "repl")
self.lake_path = lake_path
self.lake_command = lake_command

def _setup_repl(self) -> None:
from git import GitCommandError, Repo

assert isinstance(self.repl_rev, str)

# Lock the clean REPL directory during setup to prevent race conditions
Expand Down Expand Up @@ -385,6 +397,7 @@ def _get_available_lean_versions_sha(self) -> list[tuple[str, str]]:
"""
Get the available Lean versions for the selected REPL.
"""
from git import Repo
repo = Repo(self.cache_clean_repl_dir)
return [
(str(commit.message.strip()), commit.hexsha)
Expand Down
4 changes: 2 additions & 2 deletions src/lean_interact/server.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ def lean_version(self) -> str | None:

def start(self) -> None:
self._proc = subprocess.Popen(
["lake", "env", os.path.join(self.config._cache_repl_dir, ".lake", "build", "bin", "repl")],
[self.config.lake_path, self.config.lake_command, self.config.lake_env_repl_path],
cwd=self.config.working_dir,
stdin=subprocess.PIPE,
stdout=subprocess.PIPE,
Expand Down Expand Up @@ -121,7 +121,7 @@ def _execute_cmd_in_repl(self, json_query: str, verbose: bool, timeout: float |
with self._lock:
if verbose:
logger.info("Sending query: %s", json_query)
self._proc.stdin.write(json_query + "\n\n")
self._proc.stdin.write(json_query + "\n\n\n\n")
Copy link
Copy Markdown
Author

@vadimkantorov vadimkantorov May 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

without "\n\n\n\n" I was getting hangs with my existing installation of REPL

or maybe it's because "\r\n\r\n" is needed in input as well, as was discussed in leanprover-community/repl#5 (comment) ?

leanprover-community/repl#5 (comment) suggests that "\r\n" is part of JSON-RPC standard

@augustepoiroux I also noticed that you are using universal_newlines=True which seems the deprecated version of text=True, according to https://docs.python.org/3/library/subprocess.html

Copy link
Copy Markdown
Owner

@augustepoiroux augustepoiroux May 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the PR. I am on vacation now and won't have time to have a proper look into this before a week.

It seems that the REPL has changed since the PR you mention and the version you are using, hence "\n\n" is now enough. It is possible that "\n\n\n\n" or "\r\n\r\n" will not work with current REPL versions.

@augustepoiroux I also noticed that you are using universal_newlines=True which seems the deprecated version of text=True, according to https://docs.python.org/3/library/subprocess.html

If I am not mistaken, we are using text=True in Leaninteract and not universal_newlines=True.

Copy link
Copy Markdown
Author

@vadimkantorov vadimkantorov May 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(You are right, sorry about universal_newlines - I confused it with something else)

self._proc.stdin.flush()

output: str = ""
Expand Down