Getting Started

Learn how to set up and start using Astrolabe for your Lean 4 projects.

This guide walks you through installing Astrolabe and visualizing your first Lean 4 project.

Prerequisites

Before you begin, ensure you have:

• Node.js 18+ for the frontend
• Python 3.10+ for the backend
• Lean 4 installed (Installation Guide)
• A Lean 4 project with .ilean files (run lake build first)

Installation

Clone the Repository

git clone https://github.com/Xinze-Li-Bryan/Astrolabe.git
cd Astrolabe

Install Frontend Dependencies

npm install

Install Backend Dependencies

cd backend
pip install -e ".[dev]"
cd ..

Running Astrolabe

Development Mode

The simplest way to start both frontend and backend:

npm run dev:all

This runs:

• Frontend on http://localhost:3456
• Backend on http://localhost:8765

Manual Startup

If you prefer to start services separately:

# Terminal 1: Start backend
cd backend
python -m uvicorn astrolabe.server:app --host 127.0.0.1 --port 8765

# Terminal 2: Start frontend
npm run dev -- -p 3456

# Terminal 3 (optional): Start Tauri desktop app
TAURI_DEV_URL="http://localhost:3456" npm run tauri dev

Loading Your Project

1. Open Astrolabe in your browser at http://localhost:3456
2. Click Load Project and select your Lean 4 project directory
3. Astrolabe will parse .ilean files and build the dependency graph

Make sure you've run lake build in your Lean project first to generate the .ilean files.

Quick Navigation

Once your project loads:

• Press Cmd+K (Mac) or Ctrl+K (Windows/Linux) to open the Lens Picker
• Use the search bar to find specific theorems or definitions
• Click nodes to focus and explore dependencies

Available Scripts

Next Steps

• Learn about Navigation Controls
• Explore Visualization Modes
• Configure Settings and Options