REPL

Stream: lean4

[Petrica Chiriac]

Do we have a REPL (read–eval–print loop) for lean4? or is there a plan to exist?

[Kenny Lau]

The ability to use that would require typing a line of code perfectly without looking at the error message, which I believe only a handful in this community can do.

[Joe Hendrix]

There is not a REPL nor plans to write one afaik. I think it would have very limited utility.
I had thought I wanted a REPL when I first started using Lean, but once you have development environment integration working there isn't a need. If you want to interactively evaluate a term or print the type of an expression it is easier to quickly type commands like #eval or #check in your buffer then to switch to a terminal and use a REPL.

[Johan Commelin]

Also #eval foo updates automatically when you tweak foo. Continuous compilation is awesome.

[Arthur Paulino]

Just for the sake of clarification: is there any active Lean REPL project you're aware of?

[Arthur Paulino]

Ah, I guess the thread speaks by itself :D

[Arthur Paulino]

I'm trying to treat specific REPL commands here.
For instance, "!quit" and "!reset".

"!quit" is easy because I just need to break the loop. But "!reset" is supposed to start the loop again from a fresh environment. Is it possible to do so?

[Arthur Paulino]

I tried throwing an error from loop but I wasn't able to catch it in runCommandElabM

[Alexander Bentkamp]

For !reset, maybe you can do

      let env ← importModules [{ module := `Init }] {}
      modifyEnv (fun _ => env)
      loop

[Alexander Bentkamp]

For !quit, maybe simply do not call loop recursively?

[Sebastian Ullrich]

Environment is a persistent data structure, no need to recreate it. You can simply store the initial one in a variable.

[Arthur Paulino]

Thanks for both ideas!

[Arthur Paulino]

Alright, I was able to do this:
https://github.com/arthurpaulino/LeanREPL
Thanks for the help everyone!

I'd also like to know what you guys think about having something like this bundled in the Lean 4 binary so one could simply call:

$ lean --repl

I know it's not very useful for theorem proving, but it can allow people to build computational environments for Lean on top of it. For example, one possibility is making a Lean 4 kernel for Jupyter and having an extension that does the job of the Lean Infoview inside the Jupyter interface. Or if Jupyter is not plastic enough, another possibility is building an app dedicated for Lean 4.

Such environment would be suitable for applications that use libraries like Tomas' SciLean