REPL for Lean 4

Stream: Machine Learning for Theorem Proving

[Scott Morrison]

There is a primitive REPL for Lean 4 available at https://github.com/leanprover-community/repl.

From the README:

A read-eval-print-loop for Lean 4

Run using ./run.
Communicates via JSON on stdin and stdout.
Commands should be separated by blank lines.
Commands may be of the form

{ "cmd" : "import Mathlib.Data.List.Basic\ndef f := 2" }

or

{ "cmd" : "example : f = 2 := rfl", "env" : 3 }

The env field, if present,
must contain a number received in the env field of a previous response,
and causes the command to be run in the existing environment.

If there is no env field, a new environment is created.

You can only use import commands when you do not specify the env field.

You can backtrack simply by using earlier values for env.

The results are of the form

{"sorries":
 [{"pos": {"line": 1, "column": 18},
   "endPos": {"line": 1, "column": 23},
   "goal": "⊢ Nat"}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 23},
   "endPos": {"line": 1, "column": 26},
   "data":
   "type mismatch\n  rfl\nhas type\n  f = f : Prop\nbut is expected to have type\n  f = 2 : Prop"}],
 "env": 6}

showing any messages generated, or sorries with their goal states.

Information is generated for tactic mode sorries,
but currently not for term mode sorries.

[Scott Morrison]

PRs (e.g. detecting term mode sorries as well, python bindings, etc) very welcome.

[Zhangir Azerbayev]

I created a PR that allows you to interface with the repl via a python package PR #5

[Fabian Glöckle]

Hi @Scott Morrison and @Zhangir Azerbayev, thanks for making this available!

Could you help me get the mathlib4 dependency running? I got a core dump with the following:

$ git clone git@github.com:leanprover-community/repl.git
Cloning into 'repl'...
remote: Enumerating objects: 42, done.
remote: Counting objects: 100% (42/42), done.
remote: Compressing objects: 100% (25/25), done.
remote: Total 42 (delta 16), reused 38 (delta 12), pack-reused 0
Receiving objects: 100% (42/42), 8.82 KiB | 902.00 KiB/s, done.
Resolving deltas: 100% (16/16), done.
$ cd repl/
$ emacs lakefile.lean
$ cat lakefile.lean
import Lake
open Lake DSL

package REPL {
  -- add package configuration options here
}

lean_lib REPL {
  -- add library configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

-- Unfortunately the compiled version doesn't work: `unknown package 'Init'`
@[default_target]
lean_exe repl where
  root := `REPL.Main
$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
cloning https://github.com/leanprover/std4 to ./lake-packages/std
$ lake exe cache get
info: Building Cache.IO
info: Building Cache.Hashing
info: Compiling Cache.IO
info: Building Cache.Requests
info: Compiling Cache.Hashing
info: Compiling Cache.Requests
info: Building Cache.Main
info: Compiling Cache.Main
info: Linking cache
No files to download
Decompressing 2289 file(s)
$ lake build
Building REPL.Frontend
Building REPL.InfoTree
Building REPL.JSON
Compiling REPL.Frontend
Compiling REPL.JSON
Building REPL.Main
Compiling REPL.InfoTree
Compiling REPL.Main
Linking repl
$ ./run
{ "cmd" : "import Mathlib.Data.List.Basic\ndef f := 2" }

$ du -h core
621M    core
$ elan show | tail -n 6
active toolchain
----------------

leanprover/lean4:nightly-2023-03-17 (overridden by '/private/home/fgloeckle/sandbox/repl/lean-toolchain')
Lean (version 4.0.0-nightly-2023-03-17, commit 8650804b025c, Release)

Thanks in advance!!

(I am not really familiar with the Lean4/Lake build system if the problems stems from that..)

[Kyle Miller]

@Fabian Glöckle Make sure you're using the same Lean toolchain as mathlib4. To do this, you can copy what's in mathlib4/lean-toolchain into your local lean-toolchain file at the root of your project. You're using 2023-03-17, but the newest mathlib is using 2023-04-20.

[Fabian Glöckle]

oh great thank you @Kyle Miller, problem solved!