using LeanHammer's premise selection server with REPL

Stream: lean4

[Dhyan Aranha]

I have a local repo in which I have added LeanHammer and Repl to the dependencies and when I run the following code, it works great and it prints a long list of premises for me.

import json
import subprocess
import os
import sys
from typing import List, Any

# Set the Lean project root directory
LEAN_PROJECT_ROOT = "~/SorryDBTest422"

# Change to the project directory
os.chdir(LEAN_PROJECT_ROOT)

process = subprocess.Popen(
    ["lake", "exe", "repl"],
    stdin=subprocess.PIPE,
    stdout=subprocess.PIPE,
    text=True,
    bufsize=1,
    env=os.environ,
    cwd=LEAN_PROJECT_ROOT  # Explicitly set working directory
)

def send_command(command):
    json_command = json.dumps(command, ensure_ascii=False) + "\n\n"
    process.stdin.write(json_command)
    process.stdin.flush()

    response_lines = []
    while True:
        stdout_line = process.stdout.readline()
        if stdout_line.strip() == "":
            break
        response_lines.append(stdout_line)

    return json.loads("".join(response_lines))


lol = send_command({ "cmd" : "import Mathlib \n import PremiseSelection \n example : (2:Nat) + 2 = 4 := by premises", "allTactics": True })
print(lol)
env_import = lol["env"]
print(env_import)

Now if I try to jazz things up and adapt this script (with lots of help from Claude) so that it also clones a repo and adds the required dependencies (REPL, LeanHammer) things stop working:

import json
import subprocess
import os
import sys
from typing import List, Any
import tempfile


GIT_REPO_URL = "https://github.com/dhyan-aranha/SorryDBTest422/"

def run_command(cmd, cwd=None):
    """Helper function to run shell commands"""
    result = subprocess.run(cmd, shell=True, cwd=cwd, capture_output=True, text=True)
    if result.returncode != 0:
        print(f"Error running command: {cmd}")
        print(f"Error output: {result.stderr}")
        raise Exception(f"Command failed: {cmd}")
    return result.stdout

# Create a temporary directory and clone the repository
print(f"Cloning repository...")
temp_dir = tempfile.mkdtemp(prefix="lean_project_")

# Clone the repository
run_command(f"git clone {GIT_REPO_URL}", cwd=temp_dir)

# Extract the repository name from the URL
repo_name = GIT_REPO_URL.rstrip('/').split('/')[-1].replace('.git', '')

# Set the Lean project root directory to the actual cloned repo location
LEAN_PROJECT_ROOT = os.path.join(temp_dir, repo_name)
print(f"Project cloned to: {LEAN_PROJECT_ROOT}")

# Change to the project directory
os.chdir(LEAN_PROJECT_ROOT)

# Read existing lakefile.toml
lakefile_path = os.path.join(LEAN_PROJECT_ROOT, "lakefile.toml")
with open(lakefile_path, 'r') as f:
    lakefile_content = f.read()

# Add required dependencies if not already present
repl_dependency = """
[[require]]
name = "REPL"
git = "https://github.com/leanprover-community/repl"
rev = "v4.22.0"
"""

hammer_dependency = """
[[require]]
name = "Hammer"
git = "https://github.com/JOSHCLUNE/LeanHammer"
rev = "v4.22.0"
"""

if "name = \"REPL\"" not in lakefile_content:
    lakefile_content += repl_dependency
    print("Added REPL dependency to lakefile.toml")

if "name = \"Hammer\"" not in lakefile_content:
    lakefile_content += hammer_dependency
    print("Added Hammer dependency to lakefile.toml")

# Write updated lakefile.toml
with open(lakefile_path, 'w') as f:
    f.write(lakefile_content)

print("Running lake update...")
run_command("lake update", cwd=LEAN_PROJECT_ROOT)

print("Running lake build...")
run_command("lake build", cwd=LEAN_PROJECT_ROOT)

print("Starting REPL process...")
# Start the REPL process
process = subprocess.Popen(
    ["lake", "exe", "repl"],
    stdin=subprocess.PIPE,
    stdout=subprocess.PIPE,
    text=True,
    bufsize=1,
    env=os.environ,
    cwd=LEAN_PROJECT_ROOT
)

def send_command(command):
    json_command = json.dumps(command, ensure_ascii=False) + "\n\n"
    process.stdin.write(json_command)
    process.stdin.flush()

    response_lines = []
    while True:
        stdout_line = process.stdout.readline()
        if stdout_line.strip() == "":
            break
        response_lines.append(stdout_line)

    return json.loads("".join(response_lines))

# Execute the REPL commands
lol = send_command({ "cmd" : "import Mathlib \n import PremiseSelection \n example : (2:Nat) + 2 = 4 := by premises", "allTactics": True })
print(lol)
env_import = lol["env"]
print(env_import)

the output is

{'messages': [{'severity': 'error', 'pos': {'line': 3, 'column': 18}, 'endPos': {'line': 3, 'column': 20}, 'data': "unexpected token '+'; expected ':=', 'where' or '|'"}], 'env': 0}
0

instead of a long list of premises like in the previous code. Any ideas about what is going on would be greatly appreciated!

[Dhyan Aranha]

Also, if I delete the hammer dependencies and REPL on my local test repo, then do a version of the script which imports them back into the local repo then does lake update and lake build, the REPL works with the premises tactic. So the issue is maybe related to how the cloned repo is being handled as a temp-file?

[Julian Berman]

I think removing the script from the equation is probably smart to start -- if I clone your repo and add the 2 dependencies to the lakefile.toml and then run the REPL the same way you did in the script I get the error you show.

[Julian Berman]

(Which seems to be a lie, if you replace example : (2:Nat) + 2 = 4 := by premises with #check 37 the error says something about "data": "unknown constant 'Unit'"so I'm not sure how much weight to put into the precise error message, it seems like something just isn't being parsed correctly)

[Julian Berman]

Something seems different between your local repository and the one I get from cloning I think, I can't get a working version quite yet with the one I got here. Does your local git repository show any other changes?

[Dhyan Aranha]

As far as I can tell they are basically the same.

[Dhyan Aranha]

ok there is a slight difference but I doubt it much of an issue. In testSorry.lean I have imported Hammer and in my local repo this commented out. (I know from tests that even locally that if I run the command with import hammer instead of import premise selection things break...but it shouldn't effect things if some file that's not being used imports it?)

[Aaron Liu]

Usually I see these kinds of errors when you haven't imported prelude

[Dhyan Aranha]

Aaron Liu said:

Usually I see these kinds of errors when you haven't imported prelude

im really inexperienced with all of this (sorry!), how would I import prelude?

[Aaron Liu]

no idea

[Anthony Wang]

Dhyan Aranha said:

{'messages': [{'severity': 'error', 'pos': {'line': 3, 'column': 18}, 'endPos': {'line': 3, 'column': 20}, 'data': "unexpected token '+'; expected ':=', 'where' or '|'"}], 'env': 0}
0

That error sounds a lot like #new members > Confusion about Lean REPL @ 💬 which might be related.

[Julian Berman]

Yeah I also assumed that somehow it was really the import failing here -- I thought (like Eric Wieser said in the linked thread) that the import statement might be to blame but the lean-repl README seems to imply it's perfectly supported -- you cannot provide env along with an import, but without one it seems to be supported. Let's try again...

[Julian Berman]

OK so I just got it to successfully show me premises at the REPL by doing... absolutely nothing different as far as I can guess. So some funny business is happening -- literally the only thing different that I can think of is that I first opened a real life Lean life in an editor and waited for the import to succeed, then quit and tried the REPL. So let's see if that's really the thing that affects whether it works or not, maybe REPL has some sort of timeout and is killing the process too quickly (in premises' case it needs to build the cache, so presumably the second import is faster).

[Julian Berman]

Yeah so that's definitely it here.

[Julian Berman]

If I clone the repo, add the 2 dependencies, run lake update, it clones all the dependencies, then lake build, lake exits immediately and does no work, then sending lake exe repl:

{"cmd": "import Mathlib \n import PremiseSelection \n example : (2:Nat) + 2 = 4 := by premises", "allTactics": true}

fails with that obscure syntax error.

If I open foo.lean, put that exact lean code in it, wait for the file to be processed, then clearly lake does do some work and starts building something. And then if I exit and go back to lake exe repl, the exact same line now works and gives me premises.

[Dhyan Aranha]

...so what does it all mean :P, do I need to make repl wait somehow? (Also, thanks a ton Julian for taking a deeper look into this)

Also, it seems in the documentation for the premise selection server:

The first call to premise selection (by hammer or by premises) may be much slower than subsequent calls, due to caching. One should expect the first call in any file session (especially in a downstream project of Mathlib, such as FLT) to be up to 10–20 seconds. Unrelatedly, the first call in a downstream project after a server restart may also be much slower (e.g. 2 minutes) due to the time it takes to fill the server-side cache, but subsequent calls in the downstream repository (by any user) will be much faster

[Julian Berman]

I'll try again when I get back to a computer to have a concrete recommendation -- it seems likely there's a bug somewhere and that you're not doing anything wrong yourself here but I'm not 100% where yet. I doubt purely sleeping is going to help, either there's a timeout parameter that needs tweaking or more likely lake build isn't doing the right thing and we need to figure out why.

[Mac Malone]

Julian Berman said:

If I clone the repo, add the 2 dependencies, run lake update, it clones all the dependencies, then lake build, lake exits immediately and does no work [..] If I open foo.lean, put that exact lean code in it, wait for the file to be processed, then clearly lake does do some work and starts building something. And then if I exit and go back to lake exe repl, the exact same line now works and gives me premises.

The problem here is likely that lake build on a new package does nothing (as no defaultTargets have been set), whereas opening foo.lean with that code builds its imports (i.e., Mathlib and PremiseSelection). The REPL needs those prebuilt and available in the Lean search path. You can do this without the test file with:

lake build Mathlib PremiseSelection

[Julian Berman]

There we go, an expert straightens us out :) thanks Mac.

[Ruben Van de Velde]

Don't use lake build Mathlib before using lake exe cache get though

[Mac Malone]

(fortunately, in Julian's example, cloning the Mathlib dependency also fetches the cache)

[Dhyan Aranha]

It works for me! Many thanks to everyone on the thread (esp. @Julian Berman and @Mac Malone ) :heart: