Lean Workspace Quickstart

Where you see this in the app

This guide applies when you choose the Lean + Lean-TUI Starter template for a post workspace.

The main surfaces are:

• the post Workspace tab
• the Terminal tool
• the Helix tool

Recommended startup sequence

For the smoothest first run, use this order:

1. Open Terminal
2. Run make build
3. Open ProofWorkspace.lean in Helix
4. Make a small edit or trigger Lean info once if needed
5. Return to Terminal and run make tui

This sequence ensures the Lean project dependencies are built first and the Lean editor state is active before Lean-TUI tries to follow it.

What each command does

You do not need a separate make setup step.

What to expect in Helix and Lean-TUI

Helix handles Lean editing and typechecking feedback.

Lean-TUI follows the active Lean editor state and shows proof or program state in the terminal. If it stays on Connecting to 127.0.0.1:9742..., go back to Helix, make an edit, and trigger Lean info once if needed.

Persistence between sessions

The workspace project stays mounted between sessions.

That means:

• your project files stay in the workspace
• the .lake dependency cache stays in the workspace
• later make tui runs should reuse the existing Lean dependencies instead of recloning them

When to use Reset workspace to template

Use Reset workspace to template only if you want to replace the current workspace project files with a fresh copy of the Lean starter.

Important details:

• it rewrites the workspace /project files
• it keeps runtime data in /data
• it does not automatically close other users' sessions

If you only want future fresh sessions to use the Lean template, use Browse templates instead of reset.

Related docs

• Workspace templates, pools, and reset behavior
• Workspace terminal, Helix, and Codex tool access
• Workspace defaults, env vars, and runtime commands