lean4_jupyter

通过repl实现的Lean 4 Jupyter内核。

已实现的功能

🔥 查看操作： 教程笔记本。

内核可以

• 执行Lean 4命令
• 在定理“对不起”后立即使用如% proof这样的魔法执行Lean 4 tatics
• 使用如% env 1或% prove 3这样的魔法回溯到早期环境或证明状态
• 支持如%cd或%load（加载文件）这样的魔法
• 支持从项目和它们的依赖中导入模块，例如Mathlib（ 演示）。

输出

• 在jupyter notebook等中：以alectryon风格回显输入，在相应的行（目前还不是列），带有消息、证明状态
• 在jupyter console等中：以codespan风格回显输入，在相应的行:列，带有消息、证明状态

内核代码由flake8进行代码审查，并在CI中使用nbval进行测试。

下一步

• 修复repl#40（已作为repl#41提出）
• 改进alectryon注释以支持行中间的注释
• 使如%cd和%load这样的魔法更稳健地工作
• 支持在%load后显示tactics
• 将所有 repl 测试用例添加到持续集成并设置覆盖率
• 改进 Jupyter 暗色主题的 UI
• 支持通过 %lake 运行 lake 命令，例如 %lake build
• 对长时间运行的命令（如 import）提供更好的（流式）反馈
• 支持以临时方式更改 Lean 工具链和添加依赖项
• 进行小规模代码重构以平滑处理

安装

首先，您需要一个正常工作的 Lean 4 安装。您可以通过 elan 来安装它。

验证 lean 和 lake 是否已添加到您的 PATH

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

它们应分别输出 Lean/Lake 版本。

然后，您需要在 PATH 中有一个正常工作的 repl。

您可以从源代码构建它（请在执行之前阅读和调整它们）

# 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

验证 repl 是否正常工作

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

如果 repl 卡住，您可以将其终止

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

然后，确保您已安装 python、pip、jupyter，并运行

pip install jupyterlab

然后安装内核

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

要使用它，运行以下之一

# 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

灵感来源于

• 创建简单的 Python 包装器内核
• bash_kernel
• pySagredo（另请参阅 repl#5）
• LeanDojo
• alectryon
• codespan
• lean-lsp（我之前尝试使用 Lean 4 LSP 服务器制作 Lean 4 Jupyter 内核的尝试）