utensil.tngl.sh
A Lean 4 Jupyter kernel via repl
Add section usage for clarity
author
utensil
date
(Nov 19, 2024, 5:22 PM +0800)
commit
7d94cb6a
7d94cb6a2ba64798ea10444205d2ff8a9d1fdf82
parent
1cf24c1c
1cf24c1c6cd9f9ad56c6114ae117091bda310b21
+3
-5
+3
-5
README.md
+3
-5
README.md
···
60
60
61
61
### Prerequisites
62
62
63
-
1. A working Lean 4 installation. You can install it via [elan](https://github.com/leanprover/elan), e.g. on Linux-like systems:
64
-
65
-
```bash
66
-
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y --default-toolchain none
67
-
```
63
+
1. A working Lean 4 installation. You can install it via [elan](https://github.com/leanprover/elan).
68
64
69
65
2. A working Python installation (e.g. 3.11). If using a virtual environment, activate it before installing the kernel.
70
66
···
79
75
Note: the script could remove an existing `repl`, and it assumes `/usr/local/bin` is in your `PATH`, it will also set the default Lean 4 toolchain to the same as the one used by the `repl` to ensure `repl` works outside projects. For installing the extension to highlight Lean 4 syntax in JupyterLab, it will also use nvm to install Node.js if it's not installed.
80
76
81
77
If you prefer manual installation, please read __Manual installation__ below.
78
+
79
+
### Usage
82
80
83
81
To use it, run one of:
84
82