How to interface with Lean from another language?

Stream: lean4

[Mr Proof]

I want to create a GUI which can interface with Lean. Can you point me in the right direction for how to interface with lean? For example if I was making a GUI in C++ or python how would I call the Lean library and get results back? Alternatively is there a web API? Can I run Lean from the command line?

Thanks.

[Mr Proof]

I see I can call it from the command line with:
lean --stdin
And then press control+Z to run it. Is there a more interactive way to use it?

[Chris Bailey]

When you say "interface with Lean", do you mean interface with a program written in lean, or with lean itself? For the latter, is there a reason you can't just invoke it with a shell?

[Ted Hwa]

how would I call the Lean library and get results back

I'm not sure what you mean by this, but it sounds like maybe there is a misunderstanding of what Lean does.

If you are writing (or reading) proofs in Lean, the standard, interactive way to use Lean is through an IDE which allows you to step through a proof and see the goal state at each step. I recommend starting with one of the tutorials at https://leanprover-community.github.io/learn.html

[Mr Proof]

For example if I make a Windows Form in C++ with buttons, and text boxes, I want to call the lean program by sending it commands and receive the results such as current goals etc.
I couldn't really see any C++ API or such like to call Lean for example as you would do with a C++ DLL.
Also, I couldn't find the documentation for interacting with Lean via the command line

[Mr Proof]

Yes, basically I want to make my own IDE. Which will have menus and graphical interface and typsetting. Preferably running Lean as a server which I can send code to and get back results.

[Ira Fesefeldt]

Lean implements the Language Server Protocol, which afaik also the vs code plugin uses to interface with lean.

[Mr Proof]

Thanks. That seems to be what I'm looking for. If anyone has any examples of using the LSP that would be very useful.

[Chris Bailey]

I would look at the lean vscode exension: https://github.com/leanprover/vscode-lean4/tree/master

Some of the machinery for working nicely with LSP is built in, I believe it's in the docs under Lean/Server or some stuff that has the LSP namespace: https://leanprover-community.github.io/mathlib4_docs/

[Chris Bailey]

Also the nvim extension: https://github.com/Julian/lean.nvim

[Chris Bailey]

The nvim one might actually be more useful than the vscode extension to get you off the ground. I suspect vscode itself might be a more noisy middleman in the conversation between the Lean server and the client.

[Ira Fesefeldt]

I think neovim also implements its own lsp client and its plugins "only" do the details.

[Neil Ramsamooj]

I managed to access Lean from python via its repl

Some code for a function call:

function code

import json
import subprocess
import tempfile
import os

def run_lean(command):
    # Create a temporary Lean file with the desired content
    with tempfile.NamedTemporaryFile(delete=False, suffix=".lean") as temp_file:
        temp_file.write(command.encode())
        temp_file_path = temp_file.name

    # Prepare the JSON command to be passed to the Lean REPL
    json_command = json.dumps({"path": temp_file_path, "allTactics": True})

    # Run the command using subprocess
    result = subprocess.run(
        f'echo \'{json_command}\' | lake exe repl',
        shell=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,  # Capture stderr but do not print
        text=True,
        timeout=30
    )

    # Capture the response and clean up the temporary file
    response = result.stdout.strip()
    os.remove(temp_file_path)

    return response

sample function call

# Example usage
lean_command = """
import Mathlib
example {x y : Real} (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := by
intro h1
have h2 : x = y := le_antisymm h.1 h1
exact h.2 h2
"""
response = run_lean(lean_command)
print(f"Response: {response}")

response from the repl

Response: {"tactics":
[{"tactic": "intro h1",
"proofState": 0,
"pos": {"line": 4, "column": 0},
"goals": "x y : ℝ h : x ≤ y ∧ x ≠ y ⊢ ¬y ≤ x",
"endPos": {"line": 4, "column": 8}},
{"tactic": "have h2 : x = y := le_antisymm h.1 h1",
"proofState": 1,
"pos": {"line": 5, "column": 0},
"goals": "x y : ℝ h : x ≤ y ∧ x ≠ y h1 : y ≤ x ⊢ False",
"endPos": {"line": 5, "column": 37}},
{"tactic": "exact h.2 h2",
"proofState": 2,
"pos": {"line": 6, "column": 0},
"goals": "x y : ℝ h : x ≤ y ∧ x ≠ y h1 : y ≤ x h2 : x = y ⊢ False",
"endPos": {"line": 6, "column": 12}}],
"env": 0}

[Marc Huisinga]

Unless you really want to implement a text editor for Lean, using the REPL or implementing your own frontend on top of the language processing architecture is the way to go. LSP is very specific to the interaction mode of text editors.

[Mr Proof]

@Marc Huisinga Yes, REPL might be better.
Ah I see it here. https://github.com/leanprover-community/repl I believe this is what is being used with the Lean-Jupyter experiment.

Yes that seems to be working. I need some help still understanding what all the different parts do such as "lake". According to the instructions I can make this work with the standard stdin and stdout.

Ideally I'd just like to send REPL commands to lean which is running as a server or client and then get back the replies. So the next step is to work out how to run lean as a client or server. Although I could probably get it working by reading and writing to the stdin/stdout from my program. @Neil Ramsamooj code thanks your code will be useful. Although it would be nice to be able to keep the state in a more interactive way.

I see OpenAI uses something similar: https://github.com/openai/lean-gym

BTW when I call "lean --run repl" it give me "REPL is unknown package" because repl.lean has imports like REPL.JSON . I can see those files in the REPL folder. So not sure why it's not seeing them. my commandline is on the folder with repl.lean in it:

repl.lean:1:0: error: unknown package 'REPL'
You might need to open 'C:\Users\me\Documents\REPL\repl-master' as a workspace in your editor

Update
I've got it working from C#. Starting a process calling "cmd" with arguments:

p.StartInfo.Arguments ="echo #eval 2+3| lean --stdin"

from the folder with repl.lean in it. It's progress but this only will call one command at a time. And I'm trying to have it be interactive. So it's still not quite right yet. But perhaps this is the best I can do for now.

Update 2
I got it working with the

p.StartInfo.Arguments ="echo {"cmd":"#eval 2+3"} | lake exe repl."

So progress..

Now when I send commands to the stdin, if I put two \n\n at the end then it exits out. But if I only put one \n then it doesn't send me a message. So I'm still working out how to get it working interactively.

I must be missing something because I am not getting the replies until it quits out or an error occurs. I think REPL is not flushing it's buffer or something.

[Max Nowak 🐉]

Note that the LSP is not a lean thing, it’s a standard protocol (developed by Microsoft) that’s commonly used in vscode, and now other IDEs. Lean merely implements it. But iirc lean also goes beyond it, with the infoview which isn’t part of the LSP spec officially?

The infoview can display arbitrary react components, and it can even be interactive with buttons. Maybe you could write your app in there. Look at Lean ProofWidgets for examples.

But either way, I wish you luck if you do decide to go the c++ way. Can learn a lot about LSP etc that way :)

[Mr Proof]

Yes, LSP looks good but it's probably too powerful for my needs. The repl seems about right if I can get it working. I'll try both. I might need LSP if I need it to have a searchable set of tactics.
I prefer to make it in a separate program so I can use custom graphics and latex and such like. I have already been able to get it to interface with maxima. The idea is to kind of hide some of the type theory behind the scenes and make the theorem proving a bit more intuitive. Whether that's achievable I don't know.