Lean-TUI

Standalone interactive view for detailed visualization of programs and proofs that are written in Lean.

Watch a demo of some of the features: https://youtu.be/whekHs2P1Ew. See the bottom of this page for a usage guide.

• Lean-TUI
  • Installation
    • 1. Install lean-tui from Crates.io
    • 2. Add LeanPrism Dependency
  • Configuration
    • Helix (recommended)
    • Neovim
    • VS Code
    • Zed
  • Quickstart
    • 1. Split Your Terminal
    • 2. Open your editor
    • 3. Add Back-end Import
    • 4. Open lean-tui
    • 5. Start Writing Lean
  • User Guide
    • Keyboard
    • Node State Colors
    • Label Colors
    • Diff Colors for Types
  • Display Styles
    • Compact View
    • Semantic Tableau View
    • Compact Tree View
    • Data Flow
    • Effect Flow
  • Development

Installation

For those that just want to get started quickly

1. Install lean-tui from Crates.io

Install Rust (through rustup) if you haven't compiled Rust programs before. Then install this crate as a binary in your user with:

cargo install lean-tui

Or if you want the latest unstable version,

cargo install https://codeberg.org/wvhulle/lean-tui

Now, make sure that ~/.cargo/bin is in your path to be able to run lean-tui (without the ~/.cargo/bin/lean-tui prefix).

2. Add LeanPrism Dependency

Add LeanPrism as a Lake dependency.

In your lakefile.toml:

[[require]]
name = "LeanPrism"
git = "https://codeberg.org/wvhulle/lean-prism.git"
rev = "main"

Alternatively, in lakefile.lean:

require LeanPrism from "https://codeberg.org/wvhulle/lean-prism.git" @ "main"

Optionally, pre-fetch the source of this library and build it:

lake update LeanPrism
lake build LeanPrism

Configuration

You need a working code editor with an LSP client.

Helix

This is the recommended editor and used by the author. You should not need to do any setup since Helix already has Lean configured out of the box.

If you are using an older version, configure Helix to use lake serve as the Lean LSP server like this

# .helix/languages.toml
[language-server.lean]
command = "lake"
args = ["serve"]

[[language]]
language-servers = ["lean"]
name = "lean"

Neovim

Configure the command lake serve as a language server for .lean files. See official Neovim LSP docs.

VS Code

Install the Lean extension from VS Code Marketplace.

Zed

You can choose:

• Configure lake serve as LSP server, see official docs (recommended)
• Install the Lean extension

Quickstart

1. Split Your Terminal

You can choose between:

• Using multiple terminals (emulator windows) side-by-side (a terminal app is typically provided on Windows/Linux/Mac)
• Using a single terminal window with a terminal multiplexer (you'll need to install zellij or tmux with your system package manager)

2. Open Your Editor

Open your Lean file in your favorite (modal) editor that has a built-in LSP client (I recommend Helix, but Neovim, Zed, Kate also seem to have one). Lean will start up an LSP client hooked up to the default Lean LSP server, which might take awhile. Normally, any diagnostics should appear in your editor as the LSP client finishes start up.

If you encounter problems, it is usually because of stale build artifacts or incorrect lakefile.toml.

3. Add Back-End Import

Add this to the top of your Lean file (or build target):

import LeanPrism

The Lake LSP server now needs to be restarted. You can do this as follows:

• VS Code: Click on the \forall symbol at the corner and select "restart server"
• Helix: type command :lsp-restart
• Neovim / others: restart your LSP client using your editor's command

You should now see a diagnostic saying that Lake is building your dependencies (including LeanPrism), which can take awhile at the beginning.

4. Open lean-tui

Make sure you have followed the installation steps and added ~/.cargo/bin to your path. Focus the other terminal (in any directory) and run this TUI (stands for terminal user interface):

lean-tui

This will launch the TUI in the second terminal, listening on a TCP port.

5. Start Writing Lean

Now you can switch back to your editor. Move your cursor somewhere in a proof or function using keyboard or mouse.

Depending on your editor, the Lean-TUI view will update after specific events:

• Helix, one of the following:
  • Open the completion menu in insert mode: ctrl+x
  • Open documentation popup in normal mode: space,k
• VS Code: any cursor movement or change should update the TUI
• Neovim: same as Helix, but you may configure more frequent updates using Lua

The first rendering of a proof or function in a new project might be a bit slow, since the initialization happens lazily. Subsequent updates should be much faster.

User Guide

Keyboard

Normally, the view should follow your changes in the editor. Otherwise, you can also navigate with single-letter keyboard shortcuts:

The TUI follows your cursor in the editor automatically (called "follow mode") and will automatically open the view with the right file and display style.

You can disable this behavior with F or you can manually select an open analyzed file with the file picker menu f. Errors are often too long and would not fit in a node alone, so you can click on an error in to expand it in a popup at the top of the screen. Press escape to close the popup or select another node.

All views have the following key bindings for common operations:

The input pane's content depends on your program's style. For functional programs, it contains function parameters. For proofs, it contains the hypotheses. The output pane is the expected type or the proposition to be proven.

Node State Colors

The most important are the colors of the borders of the nodes and panes:

• Assumptions, parameters, and theorem hypotheses are blue
• Theorem statements, goals, and output types have an orange border.

The border colors of the nodes also change dynamically:

• The border the node under cursor will be emphasized depending on your terminal's color scheme (brighter or lighter).
• Nodes with unsolved goals have a yellow border.
• Completed nodes and proof states with no remaining open goals are purple.

Furthermore:

• Inactive proof states are dimmed gray.
• Nodes containing an error are red.

Label Colors

For tactic based proofs:

In term-based proofs, the colors are analogous

Diff Colors for Types

Hypotheses types that are added are highlighted in green, removed ones in red. Goal types that will be closed in the next step are red.

(Thanks to the expressive metaprogramming facilities of Lean, it easy to diff metavariable type values across state boundaries)

Display Styles

Different types of Lean programs or proof may require different visualization types. The categories currently supported:

• Tactics graph
• Data flow graph
• Effect flow graph

Switching between them happens automatically when you change between different parts of your program. If the autodetection does not work properly, you can also use:

Compact View

Shows the proof as a list of hypotheses and goals. By default, displays the current state with the previous state (before the current tactic) side by side.

Below you can see (or go to Codeberg) a simple but incomplete Lean proof:

import LeanPrism -- important
import Mathlib.Data.Set.Basic

theorem commutativityOfIntersections
    (s t : Set Nat) : s ∩ t = t ∩ s := by
  ext x
  apply Iff.intro

  intro h1
  rw [Set.mem_inter_iff, and_comm] at h1

  exact h1
  intro h2
  -- Wrong
  rw [ and_comm] at h2
  -- Correct: rw [Set.mem_inter_iff, and_comm] at h2
  exact h2

Notice that there is a deliberate type error. See how the rewrite is not sufficient to solve the proof goal and fails. The deliberate error is there to show how errors are displayed by this program. As errors are an important part of proof development, they are attached to every display style.

Lean-TUI will visualize the proof as follows:

By default the previous state is shown as well. Things that didn't change will have the default color (white or black). Things added in the current state are green. Goals that will be closed or hypotheses removed are red.

Semantic Tableau View

Intuitively, your proof consists of steps and each step is a node in this tree diagram. The tree follows the cursor position in your editor.

You can click on the goals and hypotheses of each node. You can also jump between clickable items with your keyboard:

This view is similar to how computer scientists and logicians talk about type theories, see Natural Deduction. The implementation is based on **Paperproof.

Compact Tree View

This is a more compact version of the semantic tableau with the tree on its side on the left.

On the right, you can see active hypotheses and goals, but only the ones currently active.

Not all proofs are written using tactics. Lean has support for both tactic-based and term-based proofs. Tactic-based proofs work backwards. Term-based proofs work forwards and are almost indistinguishable from normal functional programs.

Data Flow

If you are not using monads, and a simple pure functional programming style, you use this. It does a decomposition of your program into different related sub-states. The decomposition is built using a combination of CST and AST traversal. Each node contains the expected type at the focused part of the program and all active variables.

The following screenshot is a visualization of the ./Samples/sorting.lean file:

def insert (x : Nat) : List Nat → List Nat
  | [] => [x]
  | y :: ys => if x ≤ y then x :: y :: ys else  y :: insert x ys

The decomposition is based on a few built-in rules. However, not all Lean control flow has an accompanying rule.

Effect Flow

When working doing programming in a monad, you are doing some kind of effectful computations. Every monadic assignment in Lean written as let <- COMPUTATION can be viewed as a combination of:

• Return value: What the computation returns (if any), shown with a forward arrow.
• Effect: How the call-site is affected, such as state changes, shown with an icon below the return value. Effects may be hidden in nested monadic calls, these are bubbled up and shown in a list.

As example, here is a visualization of

def counterSequence : StateM Counter Nat := do
  let v1 ← increment
  let v2 ← double
  let v3 ← increment
  pure (v1 + v2 + v3)

If you want to see the leaf nodes, use the key binding e (expand). By default, nested calls and function definitions are hidden.

Development

Let me know if you tried it out and encountered any issues! PRs are also welcome. For those, who don't know Rust (understandable), there is a large portion of Lean code in the backend that also needs to be worked on. Take a look there if you want to contribute as a Lean user.

See ./CONTRIBUTING.md for more.