How to use the REPL from within python?

Stream: Machine Learning for Theorem Proving

[Niels Voss]

What ways are there to call the lean REPL from within python? I initially thought that sending commands and receiving output from the REPL with subprocess would be a simple task, but after spending several hours unsuccessfully debugging issues related to flushing, buffering, and pipes, I realized it wasn't as simple as I hoped. I'm curious if there are any packages that either make managing external processes easier, or directly wrap the Lean REPL.

I am on Lean 4.7.0 (which isn't ideal), but answers that work for newer versions of Lean would be helpful to me as well.

[Auguste Poiroux]

It is indeed not very straightforward. I have a working implementation using threading to send requests and get the output here. And you can find the initialization of the subprocess here.

[Niels Voss]

Ah, thanks, I'll try that code out. Although, based on the description of Lean Interact, maybe at this point it just makes more sense for me to use Lean Interact itself instead of trying to fiddle with subprocess. I'm getting a No module named 'resource' error when running import lean_interact on Windows though.

[Auguste Poiroux]

Yes indeed, I am currently trying to make LeanInteract cross-platform with this pull-request. The resource error should be resolved on Windows now, but I still have issues regarding access to the lake command.

[Niels Voss]

It's funny, I was having issues installing the REPL on windows as well, but somehow I managed to fix it? I can't remember what the issue was (I think maybe I was using lowercase require repl from git ... instead of require REPL from git ..., which actually worked)

[Niels Voss]

I just git clone'd the LeanInteract repository on Windows, did git checkout cross_platform and then uninstalled the version of lean interact on PyPI and then ran pip install . from within the LeanInteract directory. Now, everything seems to work fine for me, and Lean Interact seems to be capable of running on windows. So at the very least, your changes work for me on windows.

What issues with windows support did you still have?

[Auguste Poiroux]

Amazing! Indeed, it seems that it works for recent Lean versions, but there are issues with building the REPL with Lean v4.7.0. I am trying to fix that.

[Auguste Poiroux]

Thanks for testing it on Windows :) If you find bugs, please tell me

[Niels Voss]

This was on 4.7.0. I think maybe I did something earlier that fixed it (maybe adding the REPL to the lakefile.lean and building it beforehand)? It's super late for me so I need to get to sleep but I can help you debug at some point in the future.

[Auguste Poiroux]

Oh thanks, that would be amazing!
It seems that the issue I am facing (ld.lld: error: too many exported symbols (got 65611, max 65535)) was fixed with Lean v4.8.0-rc1: github issue, thread1, thread2, thread3.
I might drop support for Lean v4.7.0 on Windows platform then. Looking forward to see your fix @Niels Voss

[Auguste Poiroux]

Another issue with Windows: file paths are limited to 260 characters by default. Paths used for LeanInteract cache are sometimes longer than that. Here is the Microsoft doc about this and the command to fix it:

 New-ItemProperty -Path "HKLM:\SYSTEM\CurrentControlSet\Control\FileSystem" -Name LongPathsEnabled -Value 1 -PropertyType DWord -Force
 git config --system core.longpaths true

[Amitayush Thakur]

Please checkout:
https://github.com/trishullab/itp-interface
It does what you are trying to do and can run a scale across multiple ray cluster nodes (and on multiple Lean versions). One can also perform scalable proof search using our other framework:
https://github.com/trishullab/proof-wala

[Amitayush Thakur]

The whole interaction you want to build with REPL JRPC has been already baked in itp-interface . You just need to pip install the package

[Amitayush Thakur]

Just three steps:

pip install itp-interface
export LEAN_VERSION=4.7.0
install-lean-repl
install-itp-interface

^just these steps and you are ready to use the package. No need to explicitly install Lean or anything.

[Niels Voss]

Oh thanks, that would be amazing!
It seems that the issue I am facing (ld.lld: error: too many exported symbols (got 65611, max 65535)) was fixed with Lean v4.8.0-rc1: github issue, thread1, thread2, thread3.
I might drop support for Lean v4.7.0 on Windows platform then. Looking forward to see your fix Niels Voss

Oh, I think maybe I wasn't using 4.7.0 after all. I think I just assumed that if I ran LeanInteract in my project directory, it would use that project, but it didn't and it used 4.19.0. I think it's still broken on 4.7.0 :/

[Niels Voss]

Since I've already gotten repl installed successfully as an executable in my lean 4.7.0 project (in the sense that lake exe repl runs properly), is there a way for me to make Lean Interact or something just use the existing repl instead of trying to manage its own version of the repl?

[Niels Voss]

Amitayush Thakur said:

Please checkout:
https://github.com/trishullab/itp-interface
It does what you are trying to do and can run a scale across multiple ray cluster nodes (and on multiple Lean versions). One can also perform scalable proof search using our other framework:
https://github.com/trishullab/proof-wala

Does itp-interface work on windows? I'm getting a "No module named 'termios'" error when trying to run it, and I think termios is not available on windows.

[Auguste Poiroux]

Niels Voss said:

Since I've already gotten repl installed successfully as an executable in my lean 4.7.0 project (in the sense that lake exe repl runs properly), is there a way for me to make Lean Interact or something just use the existing repl instead of trying to manage its own version of the repl?

If you have a working project, then you can try to do the following with LeanInteract:

from lean_interact import LocalProject, LeanREPLConfig, LeanServer
config = LeanREPLConfig(project=LocalProject("path/to/your/project"), verbose=True)
server = LeanServer(config)

The issue I have with v4.7.0 on Windows happens when I try to create a temporary project with Mathlib as dependency.

[Niels Voss]

I get the following error:

Header

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> python
Python 3.13.2 (tags/v3.13.2:4f8bb39, Feb  4 2025, 15:23:48) [MSC v.1942 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from lean_interact import LocalProject, LeanREPLConfig, LeanServer
>>> config = LeanREPLConfig(project=LocalProject("."), verbose=True)
[20/20] Linking repl.exe
error: > c:\Users\niels\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe -o .\.lake\build\bin\repl.exe .\.lake\build\ir\REPL\Main.c.o .\.lake\build\ir\REPL\JSON.c.o .\.lake\build\ir\REPL\Frontend.c.o .\.lake\build\ir\REPL\Util\Path.c.o .\.lake\build\ir\REPL\Lean\ContextInfo.c.o .\.lake\build\ir\REPL\Util\Pickle.c.o .\.lake\build\ir\REPL\Lean\Environment.c.o .\.lake\build\ir\REPL\Lean\InfoTree.c.o .\.lake\build\ir\REPL\Lean\InfoTree\ToJson.c.o .\.lake\build\ir\REPL\Snapshots.c.o
error: stderr:
ld.lld: error: too many exported symbols (got 65611, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\niels\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe` exited with code 1
[14:33:22] ERROR    Failed to build the REPL: Command '['lake', 'build']' returned non-zero exit status 1.                                     config.py:374
Traceback (most recent call last):
  File "<python-input-1>", line 1, in <module>
    config = LeanREPLConfig(project=LocalProject("."), verbose=True)
  File "C:\Users\niels\AppData\Local\Programs\Python\Python313\Lib\site-packages\lean_interact\config.py", line 299, in __init__
    self._setup_repl()
    ~~~~~~~~~~~~~~~~^^
  File "C:\Users\niels\AppData\Local\Programs\Python\Python313\Lib\site-packages\lean_interact\config.py", line 370, in _setup_repl
    subprocess.run(
    ~~~~~~~~~~~~~~^
        ["lake", "build"], cwd=self._cache_repl_dir, check=True, stdout=self._stdout, stderr=self._stderr
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    )
    ^
  File "C:\Users\niels\AppData\Local\Programs\Python\Python313\Lib\subprocess.py", line 579, in run
    raise CalledProcessError(retcode, process.args,
                             output=stdout, stderr=stderr)
subprocess.CalledProcessError: Command '['lake', 'build']' returned non-zero exit status 1.
>>>

[Niels Voss]

This is strange because lake build, lake exe repl, and .\.lake\packages\REPL\.lake\build\bin\repl.exe all run correctly from my current directory

[Auguste Poiroux]

Interesting, so here the REPL fetched by LeanInteract fails to build. It is not the same REPL as the one you execute with lake exe repl. The REPL used by LeanInteract is slightly different from the one tagged by v4.7.0 in the official REPL repo. In fact, it is coming from https://github.com/augustepoiroux/repl/tree/v1.0.6, which backports the new features to previous Lean versions. So the issue is probably that the backport for v4.7.0 does not compile on Windows (the CI only tests for Ubuntu on this repo) ^^'

[Niels Voss]

Yeah, now I'm getting the same error as you. After modifying my lakefile.lean with the following change:

-require REPL from git "https://github.com/leanprover-community/repl.git" @ leanVersion
+require REPL from git "https://github.com/augustepoiroux/repl.git" @ "v1.0.6"

I tried to build it and got the following:

Lake

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> lake update REPL
REPL: cloning https://github.com/augustepoiroux/repl.git to '.\.lake\packages\REPL'
warning: Qq: ignoring missing dependency manifest '.\.lake\packages\Qq\lake-manifest.json'
warning: Cli: ignoring missing dependency manifest '.\.lake\packages\Cli\lake-manifest.json'
mathlib: running post-update hooks
No files to download
Decompressing 4359 file(s)
unpacked in 639 ms
PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> lake build
PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> lake exe repl
info: [0/20] Building REPL.Util.Path
info: [0/20] Building REPL.Frontend
info: [0/20] Building REPL.Lean.InfoTree
info: [0/20] Building REPL.Util.Pickle
info: [0/20] Building REPL.Lean.ContextInfo
info: [0/20] Building REPL.JSON
info: [5/20] Compiling REPL.Lean.ContextInfo
info: [5/20] Building REPL.Lean.Environment
info: [5/20] Building REPL.Snapshots
info: [5/20] Compiling REPL.Util.Path
info: [5/20] Compiling REPL.Util.Pickle
info: [5/20] Compiling REPL.Frontend
info: [5/20] Compiling REPL.JSON
info: [6/20] Building REPL.Lean.InfoTree.ToJson
info: [6/20] Compiling REPL.Lean.InfoTree
info: [12/20] Compiling REPL.Lean.Environment
info: [14/20] Compiling REPL.Snapshots
info: [16/20] Building REPL.Main
info: [16/20] Compiling REPL.Lean.InfoTree.ToJson
info: [19/20] Compiling REPL.Main
info: [20/20] Linking repl.exe
error: > c:\Users\niels\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe -o .\.lake/packages\REPL\.lake\build\bin\repl.exe .\.lake/packages\REPL\.lake\build\ir\REPL\Main.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\JSON.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Frontend.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Util\Path.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Lean\ContextInfo.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Util\Pickle.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Lean\Environment.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Lean\InfoTree.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Lean\InfoTree\ToJson.c.o .\.lake/packages\REPL\.lake\build\ir\REPL\Snapshots.c.o
error: stderr:
ld.lld: error: too many exported symbols (got 65611, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\niels\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe` exited with code 1

[Niels Voss]

Actually, looking at the number of exported symbols, it says that we have 65611 symbols which exceeds the max of 65535. Could it maybe be that by backporting the new features, you added just enough code to push the symbol limit over the top?

[Auguste Poiroux]

It looks very plausible. I am not sure how to contain that though as new features get added to the REPL.

Niels Voss said:

Since I've already gotten repl installed successfully as an executable in my lean 4.7.0 project (in the sense that lake exe repl runs properly), is there a way for me to make Lean Interact or something just use the existing repl instead of trying to manage its own version of the repl?

Regarding using a custom REPL, there is no easy way yet to do so because of the automated management of Lean versions.
However, there is a hack: you can try to inherit from LeanREPLConfig and override the __init__ and _setup_repl methods (and don't use super().__init__ or super()._setup_repl as they do the versioning management). You might face bugs as the REPL interface has probably changed in the meantime, which might not be completely compatible with what LeanInteract expects.

[Niels Voss]

I'll give this a shot, although I'm starting to suspect that maybe updating to Lean v4.8.0 or later on windows is the path of least resistance. If the old repl is indeed just short of the 65535 symbol limit, continuing to use that repl and hoping that we don't go over the top with symbols is a fragile solution at best.

[Auguste Poiroux]

Sounds like a good idea. Hopefully, it will work with Lean v4.8.0 :pray:

[Niels Voss]

Earlier I copied parts of LeanInteract to write this:

Python

import os
import subprocess
import shutil
from pathlib import Path
from typing import NewType
import time
import platform
import threading
import logging
logger = logging.getLogger(__name__)

# If I understand correctly, this code does not work on windows because resource is not available.
# So, code should check to make sure it isn't running on Windows before calling this.
# https://github.com/augustepoiroux/LeanInteract/blob/7b0ed74c2e29fa0ae6bc9d437dc77ab9aa9a4421/src/lean_interact/utils.py#L39
def _limit_memory(max_mb: int | None):
    """Limit the memory usage of the current process."""
    if max_mb is None:
        return
    try:
        import resource

        resource.setrlimit(resource.RLIMIT_AS, (max_mb * 1024 * 1024, max_mb * 1024 * 1024))
        # logger.info("Memory usage limited to %d MB", max_mb)
    except ValueError:
        # logger.warning("Failed to set memory limit to %d MB.", max_mb)
        pass
    except ImportError:
        # logger.warning("Memory limits not supported on this platform.")
        pass
    except Exception as e:
        # logger.warning("Error while setting memory limit: %s", e)
        pass

# Currently unused
LeanEnvironmentId = NewType("LeanEnvironmentId", int)
"""
When the Lean REPL finishes executing a command, it stores the resulting environment and returns
its index.
Then, when you run another command with the REPL, you can provide that index and reuse the same
environment.
"""

class LeanREPL:
    def __init__(self, project_directory: Path):
        """
        Opens a repl in project at the current directory. This runs `lake exe repl`, so it requires
        REPL to be installed as a lake dependency for that project.
        """

        '''
        path_to_lake: str = shutil.which("lake")
        print(f"Using lake at {path_to_lake}")
        print(f"Opening REPL at {project_directory}")
        self.repl_subprocess: subprocess.Popen[str] = \
            subprocess.Popen([path_to_lake, "exe", "repl"], cwd=project_directory, text=True,
                            stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE,
                            bufsize=1)
        self.repl_subprocess.stdin.write('{ "cmd": "def f := 2" }\n\n')
        self.repl_subprocess.stdin.flush()
        '''

        self._lock = threading.Lock()

        # https://github.com/augustepoiroux/LeanInteract/blob/7b0ed74c2e29fa0ae6bc9d437dc77ab9aa9a4421/src/lean_interact/server.py#L64-L77
        self._proc = subprocess.Popen(
            #["lake", "env", os.path.join(self.config._cache_repl_dir, ".lake", "build", "bin", "repl")],
            ["lake", "exe", "repl"],
            cwd=project_directory,
            stdin=subprocess.PIPE,
            stdout=subprocess.PIPE,
            stderr=subprocess.PIPE,
            encoding="utf-8",
            text=True,
            bufsize=1,
            preexec_fn=None
            if platform.system() == "Windows"
            else lambda: _limit_memory(self.config.memory_hard_limit_mb), # TOOD: Config
        )

    # https://github.com/augustepoiroux/LeanInteract/blob/7b0ed74c2e29fa0ae6bc9d437dc77ab9aa9a4421/src/lean_interact/server.py#L108-L139
    def _execute_cmd_in_repl(self, json_query: str, verbose: bool, timeout: float | None) -> str:
        """Send JSON queries to the Lean REPL and wait for the standard delimiter."""
        assert self._proc is not None and self._proc.stdin is not None and self._proc.stdout is not None
        with self._lock:
            if verbose:
                logger.info("Sending query: %s", json_query)
            self._proc.stdin.write(json_query + "\n\n")
            self._proc.stdin.flush()

            output: str = ""

            def reader():
                # Read until delimiter "\n\n" or timeout
                nonlocal output
                assert self._proc is not None and self._proc.stdout is not None
                while True:
                    line = self._proc.stdout.readline()
                    if not line:
                        break  # EOF
                    output += line
                    if output.endswith("\n\n"):
                        break

            t = threading.Thread(target=reader)
            t.start()
            t.join(timeout)
            if t.is_alive():
                self.kill()
                raise TimeoutError(f"The Lean server did not respond in time ({timeout=}) and is now killed.")
            if output:
                return output
            raise BrokenPipeError("The Lean server returned no output.")

and it hung forever when running _execute_cmd_in_repl. This was the same issue I was getting at the top of this thread when running subprocess. It could be that the Lean REPL was just broken in v4.7.0 and I need to use your modified version to get it to work

[Auguste Poiroux]

There is this commit adding flushing to the repl after the v4.7.0 tag, so maybe.

[Niels Voss]

At first glance, v4.8.0 seems to be working. I haven't tested it on a project yet, but here's a quick interaction with python:

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> python
Python 3.13.2 (tags/v3.13.2:4f8bb39, Feb  4 2025, 15:23:48) [MSC v.1942 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> import lean_interact
>>> from lean_interact import LocalProject, LeanREPLConfig, LeanServer
>>> config = LeanREPLConfig(lean_version="v4.8.0", verbose=True)
info: Version 4.0.1 of elan is available! Use `elan self update` to update.
info: downloading component 'lean'
180.8 MiB / 180.8 MiB (100 %)  20.0 MiB/s ETA:   0 s
info: installing component 'lean'
Build completed successfully.
>>> server = LeanServer(config)
>>> from lean_interact import Command
>>> server.run(Command(cmd="def f := 2"))
CommandResponse(env=0)
>>> server.run(Command(cmd="def f := 2"))
CommandResponse(env=1)
>>>

[Auguste Poiroux]

Nice, let's see how it goes. I am also thinking that using WSL (Windows Subsystem for Linux) might be an option as well if you need v4.7.0

[Niels Voss]

Hopefully Lean 4.7.0 is not strictly necessary, but I can check out WSL if it is. The main reason we're on such an outdated version of Lean is because we were doing stuff with proofs from the Natural Number Game, which is still on v4.7.0, and my team doesn't want to update unless strictly necessary because they're worried it might break stuff. But it seems it is strictly necessary to update, so that'll probably be what we try next.

[Kevin Buzzard]

I should think that bumping NNG would be easy unless it also needs a bump of Lean4game in which case I have no idea how easy it will be

[Niels Voss]

I can maybe give that a shot tomorrow. Lean4Game is still on 4.7.0, so it looks like it might not be that easy to port. We only need the proofs from NNG4, not the actual game server, so updating is probably not that big of a deal. (Although in the long run, updating NNG4 is probably the right thing to do)

[Amitayush Thakur]

Niels Voss said:

Amitayush Thakur said:

Please checkout:
https://github.com/trishullab/itp-interface
It does what you are trying to do and can run a scale across multiple ray cluster nodes (and on multiple Lean versions). One can also perform scalable proof search using our other framework:
https://github.com/trishullab/proof-wala

Does itp-interface work on windows? I'm getting a "No module named 'termios'" error when trying to run it, and I think termios is not available on windows.

Right now it doesn't work on Windows natively, but you can always use WSL.

[Niels Voss]

Thank you, that's helpful to know. I think right now I'm going to try to get Lean Interact working because it's closer to a one-to-one correspondence with the REPL, which is what I need, but I'll probably check out itp-interface in the future.

[Niels Voss]

So far, after updating the project to Lean 4.8.0, Lean Interact seems to work:

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> python
Python 3.13.2 (tags/v3.13.2:4f8bb39, Feb  4 2025, 15:23:48) [MSC v.1942 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from lean_interact import LocalProject, LeanREPLConfig, LeanServer, Command
>>> config = LeanREPLConfig(project=LocalProject("."), verbose=True)
Build completed successfully.
Build completed successfully.
>>> server = LeanServer(config)
>>> server.run(Command(cmd="def f := 2"))
CommandResponse(env=0)
>>> server.run(Command(cmd="import Game"))
CommandResponse(env=1)
>>> server.run(Command(cmd="import Game"))
CommandResponse(env=2)
>>>

I think the Lean 4.7.0 -> 4.8.0 transition was not too bad, with the only major change being that Std (which was a separate repository at the time, and is unrelated to the current Std) was renamed to Batteries. But just changing a few imports fixes this.

[Niels Voss]

@Auguste Poiroux Thank you for all the help, and I really appreciate the time you spent writing Lean Interact!

[Auguste Poiroux]

Thank you! I hope your project goes well from here :) Looking forward to reading your work using NNG

[Auguste Poiroux]

Niels Voss said:

So far, after updating the project to Lean 4.8.0, Lean Interact seems to work:

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> python
Python 3.13.2 (tags/v3.13.2:4f8bb39, Feb  4 2025, 15:23:48) [MSC v.1942 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from lean_interact import LocalProject, LeanREPLConfig, LeanServer, Command
>>> config = LeanREPLConfig(project=LocalProject("."), verbose=True)
Build completed successfully.
Build completed successfully.
>>> server = LeanServer(config)
>>> server.run(Command(cmd="def f := 2"))
CommandResponse(env=0)
>>> server.run(Command(cmd="import Game"))
CommandResponse(env=1)
>>> server.run(Command(cmd="import Game"))
CommandResponse(env=2)
>>>

I think the Lean 4.7.0 -> 4.8.0 transition was not too bad, with the only major change being that Std (which was a separate repository at the time, and is unrelated to the current Std) was renamed to Batteries. But just changing a few imports fixes this.

Oh one last thing (hopefully): imports in commands never crash (see this PR), so your test doesn't really check if it's working yet...

[Niels Voss]

I ran #check on a symbol that was imported so hopefully this is a sign that it works fine.

PS C:\Users\niels\Documents\Projects\LeanTutor\NNG4> python
Python 3.13.2 (tags/v3.13.2:4f8bb39, Feb  4 2025, 15:23:48) [MSC v.1942 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> from lean_interact import LocalProject, LeanREPLConfig, LeanServer, Command
>>> config = LeanREPLConfig(project=LocalProject("."), verbose=True)
Build completed successfully.
Build completed successfully.
>>> server = LeanServer(config)
>>> server.run(Command(cmd="import Game"))
CommandResponse(env=0)
>>> server.run(Command(cmd="#check MyNat",env=0))
CommandResponse(env=1, messages=[Message(data='MyNat : Type', severity='info', start_pos=Pos(line=1, column=0), end_pos=Pos(line=1, column=6))])
>>> server.run(Command(cmd="#check MyNat")) # no env, so this should hopefully fail
CommandResponse(env=2, messages=[Message(data="unknown identifier 'MyNat'", severity='error', start_pos=Pos(line=1, column=7), end_pos=Pos(line=1, column=12))])
>>>

[Niels Voss]

Oh yeah, since I just remembered that I'm using the unreleased version of LeanInteract, and not the version on PyPI, do you know when the PR you opened yesterday might be merged? (No worries if it's not anytime soon, I'm perfectly fine using a version not on PyPI)

[Auguste Poiroux]

Hopefully this will be merged during the week. I am trying to have a working CI for windows to avoid regressions :+1:

[Simon Sorg]

Another use-case that might be interesting is library building (i.e. LegoProver).
Use tactic mode to find proofs, and them manifest these proofs in the environment somehow.
The only way I know of to accomplish this is to manually track tactic strings and indent them correctly before sending a command to the REPL containing the theorem with proof.

For large-scale projects, it would also be nice to have a way to share environments with various REPL instances. Pickling works, but shares the whole environment. If one had two REPL instances that already have the same environment, it would be nice to only share the delta. For now, one simply needs to manifest the same theorem in each REPL instance.

[Auguste Poiroux]

@Niels Voss v0.5.0 of LeanInteract with Windows compatibility is released on PyPI ;)

[Niels Voss]

Thank you so much! You're the best