lean4_jupyter

A Lean 4 Jupyter kernel via repl.

What's already working

🔥 See it in action: Tutorial notebook.

The kernel can:

• execute Lean 4 commands
• execute Lean 4 tatics with magic like % proof immediately after a sorryed theorem
• backtrack to earlier environment or proof states with magic like % env 1 or % prove 3
• support magics like %cd or %load (loading a file)
• support for importing modules from projects and their dependencies, e.g. Mathlib ( demo ).

Output:

• In jupyter notebook and alike: echos the input annotated in alectryon style, at the corresponding line (not columns yet), with messages, proof states
• In jupyter console and alike: echos the input annotated in codespan style, at the corresponding line:column, with messages, proof states

The kernel code is linted by flake8, and tested with nbval in CI.

What's next

• Fix repl#40 (PRed as repl#41)
• Improve the alectryon annotation to support annotations in the middle of a line
• Make magics like %cd and %load work more robustly
• Support show tactics after %load
• Add all repl test cases to the CI and set up coverage
• Improve UI in Jupyter Dark themes
• Support running lake commands via %lake, e.g. %lake build
• Better (streamed) feedback for long running commands such as import
• Support changing Lean toolchain and adding dependencies in an ad hoc manner
• Minor code refactor to smooth things out

Installation

First, you need a working Lean 4 installation. You can install it via elan.

Verify that lean and lake is in your PATH:

lean --version
lake --help|head -n 1

they should output Lean/Lake versions, respectively.

Then, you need to have a working repl in your PATH.

You can build it from source (please read and adjust them before executing):

# If you need to clean up before reinstalling
# rm -rf ~/.lean4_jupyter/repl
# rm /usr/local/bin/repl

# Prepare a directory for lean4_jupyter where we install repl to
mkdir -p ~/.lean4_jupyter

# Before repl#41 merge, you might need to use this branch instead
git clone -b fix-dup https://github.com/utensil/repl ~/.lean4_jupyter/repl
# git clone https://github.com/leanprover-community/repl ~/.lean4_jupyter/repl

# Build repl
(cd ~/.lean4_jupyter/repl && lake build)

# Install repl to a place in your PATH, so less hassle of fiddling with PATH
ln -s ~/.lean4_jupyter/repl/.lake/build/bin/repl /usr/local/bin/repl

Verify that repl is working:

echo '{"cmd": "#eval Lean.versionString"}'|repl

In case repl hangs, you could kill it with

ps aux|grep repl|grep -v grep|awk '{print $2}'|xargs kill -9

Then, ensure that you have python, pip, jupyter installed, and run:

pip install jupyterlab

Then, install the kernel:

pip install lean4_jupyter
# or in development mode, check out the repo then run
# pip install -e .
python -m lean4_jupyter.install

To use it, run one of:

# Web UI
jupyter notebook
jupyter lab

# Console UI
# hint: use Ctrl-D and confirm with y to exit
jupyter console --kernel lean4
# hint: you need to run `pip install PyQt5 qtconsole` to install it
jupyter qtconsole --kernel lean4

Inspired by

• Making simple Python wrapper kernels
• bash_kernel
• pySagredo (see also repl#5)
• LeanDojo
• alectryon
• codespan
• lean-lsp (My previous attempt to make a Lean 4 Jupyter kernel using Lean 4 LSP server)