GitLocker: The Coding Marketplace

Description:

lean4jupyter 0.0.1

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)