Project Files

Understanding the .astrolabe directory structure and JSON file formats.

When you open a Lean project in Astrolabe, a .astrolabe directory is created in the project root to store cached data and user customizations.

Directory Structure

your-lean-project/
├── .astrolabe/
│   ├── graph.json      # Dependency graph cache
│   ├── meta.json       # User metadata and canvas state
│   └── lsp.json        # LSP semantic information cache
├── .lake/
│   └── build/
│       └── *.ilean     # Lean compilation outputs (source for parsing)
└── *.lean              # Your Lean source files

graph.json

The main dependency graph cache. Generated by parsing .ilean files from Lean's build output.

Structure

{
  "version": "1.0",
  "generated_at": "2026-02-01T16:00:00Z",
  "ilean_hash": "a1b2c3d4e5f6...",
  "nodes": [...],
  "edges": [...]
}

Node Fields

Declaration Types (kind)

Edge Fields

Cache Validation

The cache is validated using an ilean_hash computed from:

• Filenames of all .ilean files
• Modification times
• File sizes

If the hash doesn't match, Astrolabe automatically reparses the project.

meta.json

Stores user customizations and canvas state. This file is created when you first modify any node/edge properties or save canvas positions.

Structure

{
  "nodes": {
    "Nat.add": {
      "label": "Custom Label",
      "size": 1.5,
      "pinned": true,
      "notes": "# My Notes\nWith **markdown** support"
    }
  },
  "edges": {
    "Nat.add->Nat.succ": {
      "style": "dashed",
      "notes": "Important dependency"
    }
  },
  "canvas": {
    "positions": {
      "Nat.add": {"x": 10.5, "y": 20.3, "z": 5.2}
    },
    "viewport": {
      "camera_position": [0, 0, 20],
      "camera_target": [0, 0, 0]
    },
    "visible_nodes": ["Nat.add", "Nat.succ"]
  }
}

Node Metadata Fields

Custom Nodes

You can create virtual nodes that don't exist in Lean:

{
  "nodes": {
    "custom-outline-1": {
      "name": "Proof Strategy",
      "kind": "custom",
      "references": ["Theorem.A", "Lemma.B"],
      "notes": "Conceptual grouping node"
    }
  }
}

Canvas State

The canvas object stores:

• positions: 3D coordinates for each node
• viewport: Camera position and target
• visible_nodes: Which nodes are currently displayed

Positions are automatically saved when you arrange nodes in the 3D view.

What's NOT Stored

Identity fields from Lean are read-only and not stored in meta.json:

• name, kind, file_path, line_number
• references, depends_on_count, used_by_count, depth

lsp.json

Caches semantic information from Lean's Language Server Protocol. See LSP Integration for details.

Structure

{
  "version": 3,
  "built_at": "2026-02-01T16:00:00Z",
  "files": {
    "/path/to/File.lean": {
      "symbols": [...],
      "diagnostics": [...],
      "node_statuses": {
        "Theorem.name": "proven"
      }
    }
  },
  "namespaces": {
    "MyNamespace": {
      "name": "MyNamespace",
      "file_path": "/path/to/File.lean",
      "line_number": 10
    }
  }
}

Node Status Values

File Watching

Astrolabe watches for changes to:

• .ilean files → Triggers graph reload
• meta.json → Triggers metadata reload

Changes are automatically detected and the visualization updates in real-time.

Best Practices

Version Control

Add to your .gitignore:

# Cache files (regenerated automatically)
.astrolabe/graph.json
.astrolabe/lsp.json

# Keep user customizations (optional)
# .astrolabe/meta.json

Whether to commit meta.json depends on your workflow:

• Commit: Share node positions and notes with team
• Ignore: Keep personal customizations local

Rebuilding Cache

If you encounter stale data:

1. Delete .astrolabe/graph.json
2. Run lake build to regenerate .ilean files
3. Reload the project in Astrolabe

Or use the API:

POST /api/project/refresh