Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lean 4’s infoview is not a static display. It is a React application that can render arbitrary user-defined components, call server-side Lean functions over an RPC channel, and display rich interactive data including goal states, diagnostics, and custom visualizations. This page explains how widgets are defined and registered, how the RPC protocol connects the client to the Lean server, and how the language server itself is structured.

​
User Widgets

​
What a widget is

A user widget is a JavaScript ES module that exports a React component. The infoview loads it and renders it whenever the text cursor is within the syntactic range of a widget invocation. Widgets can call back into the Lean server using the RPC protocol to fetch live data: current goal state, elaboration information, or the result of any function you mark with @[server_rpc_method].

​
Declaring a widget module

Define the JavaScript (or TypeScript compiled to JS) as a Lean String and wrap it in the Lean.Widget.Module structure, then tag the constant with @[widget_module]: 
import Lean.Widget.UserWidget

open Lean Widget

@[widget_module]
def myWidget : Module where
  javascript := "
    import * as React from 'react';
    export default function MyWidget({ pos }) {
      return React.createElement('p', null, `Cursor at line ${pos.line}`);
    }
  "
The Module structure (from Lean.Widget.Types) holds the JavaScript source and caches its hash: 
structure Module where
  javascript : String
  javascriptHash : { x : UInt64 // x = hash javascript } :=
    ⟨hash javascript, rfl⟩
The JavaScript environment inside the infoview provides @leanprover/infoview and react as importable modules. You access them via bare import specifiers rather than URLs.

​
Using include_str for external JS files

For larger widgets you typically maintain the JavaScript in a separate .js file and embed it with include_str: 
@[widget_module]
def myWidget : Module where
  javascript := include_str "widgets" / "my-widget.js"
include_str embeds the file at compile time but does not register a dependency with Lake. Your Lean module will not be automatically rebuilt when the .js file changes. Manually touch the .lean file or add an explicit input_file target in your lakefile.lean to force recompilation.

​
Attaching a widget to a position with savePanelWidgetInfo

To display a widget at a specific location in a file, call Widget.savePanelWidgetInfo from within a command elaborator or tactic. The function records a WidgetInstance in the InfoTree at the current syntax position: 
/-- Save the data of a panel widget which will be displayed
    whenever the text cursor is on `stx`. -/
def savePanelWidgetInfo
    (hash : UInt64)
    (props : StateM Server.RpcObjectStore Json)
    (stx : Syntax) : CoreM Unit
The hash must equal (ToModule.toModule c).javascriptHash for some @[widget_module]-tagged constant c. A typical elaborator pattern: 
open Lean Widget Server in
elab "#show_widget" : command => do
  let stx ← getRef
  savePanelWidgetInfo
    myWidget.javascriptHash
    (return Json.mkObj [("message", "hello")])
    stx

​
Persistent panel widgets with show_panel_widgets

The show_panel_widgets command registers a widget to appear globally (or in a scoped/local region) without any per-invocation elaboration: 
show_panel_widgets [myWidget]

-- With props
show_panel_widgets [myWidget with Json.mkObj [("color", "blue")]]

-- Local: display only in the current section, namespace, or file
show_panel_widgets [local myWidget]

-- Scoped: display only when the current namespace is open
show_panel_widgets [scoped myWidget]

-- Hidden in the current file only (does not affect downstream modules)
show_panel_widgets [-myWidget]

​
The deprecated UserWidgetDefinition

Older code used Widget.UserWidgetDefinition with @[widget]. This form is still supported for backward compatibility: 
@[widget]
def rubiks : UserWidgetDefinition where
  name := "Rubik's Cube"
  javascript := include_str "rubiks.js"
Prefer @[widget_module] with Module for new code.

​
The RPC Protocol

​
Architecture overview

The infoview communicates with the Lean server through the LSP $/lean/rpc/call request. The client maintains an RPC session per open file. Each call carries a method name (a Lean Name) and a JSON-encoded parameter object. The server dispatches the call to a registered RpcProcedure.

​
Registering a server-side RPC method

Annotate any function of type α → RequestM (RequestTask β) with @[server_rpc_method], where both α and β implement Server.RpcEncodable: 
import Lean.Server.Rpc.RequestHandling

open Lean Server in
structure MyParams where
  pos : Lsp.Position
  deriving Server.RpcEncodable

structure MyResponse where
  message : String
  deriving Server.RpcEncodable

@[server_rpc_method]
def myRpcHandler (p : MyParams) : RequestM (RequestTask MyResponse) :=
  RequestM.asTask do
    return { message := s!"Got position {p.pos.line}:{p.pos.character}" }
The @[server_rpc_method] attribute is defined in Lean.Server.Rpc.RequestHandling: 
Marks a function as a Lean server RPC method.
Shorthand for `registerRpcProcedure`.
The function must have type `α → RequestM (RequestTask β)` with
`[RpcEncodable α]` and `[RpcEncodable β]`.

​
RpcEncodable and WithRpcRef

Server.RpcEncodable is the typeclass for types that can be serialized over the RPC channel. It extends JSON encoding with support for WithRpcRef, which lets you pass server-side object references (closures, environment snapshots, etc.) to the client as opaque handles that the client returns on the next call. 
-- A goal is sent as an RpcEncodable structure
structure InteractiveGoal extends InteractiveGoalCore where
  userName?    : Option String
  goalPrefix   : String
  mvarId       : MVarId
  isInserted?  : Option Bool := none
  isRemoved?   : Option Bool := none
  deriving RpcEncodable

​
Key Widget Data Types

​
Lean.Widget.TaggedText

TaggedText is the core display type for pretty-printed terms and goals. It is a rose tree of text fragments where leaves carry semantic tags that the infoview uses to render interactive popups and hyperlinks. 
inductive TaggedText (α : Type u) where
  | text   : String → TaggedText α
  | append : Array (TaggedText α) → TaggedText α
  | tag    : α → TaggedText α → TaggedText α

​
Lean.Widget.InteractiveGoal

An InteractiveGoal wraps a tactic-mode goal for display in the infoview. It embeds CodeWithInfos (a TaggedText specialization) so every subterm is clickable: 
structure InteractiveGoalCore where
  hyps : Array InteractiveHypothesisBundle
  type : CodeWithInfos
  ctx  : WithRpcRef Elab.ContextInfo

structure InteractiveGoal extends InteractiveGoalCore where
  userName?  : Option String
  goalPrefix : String   -- usually "⊢ "
  mvarId     : MVarId
  isInserted? isRemoved? : Option Bool := none
  deriving RpcEncodable
The RPC method Lean.Widget.getInteractiveGoals returns the current goals at a given position, and the infoview calls it whenever the cursor moves.

​
Lean.Widget.InteractiveTermGoal

The term-mode counterpart embeds the range of the term as well as the TermInfo from elaboration: 
structure InteractiveTermGoal extends InteractiveGoalCore where
  range : Lsp.Range
  term  : WithRpcRef Elab.TermInfo
  deriving RpcEncodable

​
Lean.Widget.InteractiveCode (CodeWithInfos)

CodeWithInfos is TaggedText SubexprInfo, where SubexprInfo identifies a subexpression in the elaborated term. The infoview uses it to show hover popups and “go to definition” links directly in the goal display.

​
Language Server Architecture

​
The watchdog / file-worker split

The Lean language server (lean --server) is implemented in Lean.Server and follows a strict two-process architecture described in src/Lean/Server/README.md: 
Editor (VS Code)
    │  LSP JSON-RPC
    ▼
Watchdog process  (Lean.Server.Watchdog)
    │  spawns one per open file
    ▼
File worker process  (Lean.Server.FileWorker)
The watchdog has a minimal role: it manages the set of per-file worker processes, maintains the last-known file contents, and routes LSP notifications and requests between the editor and the correct worker. It does no elaboration. Each file worker does all the real work: it runs the Lean elaborator on the file, builds an InfoTree, answers hover/completion/go-to-definition requests, and generates diagnostics. If a worker crashes (e.g., due to a stack overflow in user metaprogram code), only that file is affected; the watchdog restarts it while all other open files continue operating.
When you rebuild lean after changing server code, use Restart Server in VS Code if you changed the watchdog, or Refresh File Dependencies if you only changed the worker.

​
Snapshots and incrementality

Workers use the snapshot system (Lean.Language.Snapshot) to make file processing incremental. A snapshot captures the elaboration state after each top-level command. When the user edits the file, the worker reuses any snapshot whose preceding commands have not changed, re-elaborating only from the first affected command onward. Request handlers locate the relevant snapshot using withWaitFindSnap, which asynchronously waits for elaboration to reach the cursor position before responding.

​
LSP capabilities implemented

The Lean server implements the following standard LSP features:
  • textDocument/didOpen, didChange, didClose, didSave
  • workspace/didChangeWatchedFiles (.lean and .ilean files)
  • $/lean/fileProgress — incremental elaboration progress notifications
  • textDocument/completion, completionItem/resolve
  • textDocument/hover
  • textDocument/signatureHelp
  • textDocument/codeAction, codeAction/resolve
  • textDocument/documentHighlight
  • textDocument/semanticTokens/full, textDocument/semanticTokens/range
  • textDocument/inlayHint
  • textDocument/foldingRange, textDocument/documentSymbol
  • Lean.Widget.getInteractiveDiagnostics
  • Lean.Widget.getInteractiveGoals
  • Lean.Widget.getInteractiveTermGoal
  • Lean.Widget.getWidgets
  • Lean.Widget.getWidgetSource
  • Lean.Widget.getGoToLocation
  • Lean.Widget.lazyTraceChildrenToInteractive
  • Lean.Widget.highlightMatches
  • Lean.Widget.InteractiveDiagnostics.infoToInteractive
  • Lean.Widget.InteractiveDiagnostics.msgToInteractive

​
Logging LSP traffic

To capture all LSP messages exchanged between the editor and the server, set the environment variable before launching: 
export LEAN_SERVER_LOG_DIR=/tmp/lean-lsp-logs
code .
This creates one file per I/O stream for the watchdog process and each worker process.

Build docs developers (and LLMs) love

Get started for freeTalk to us