---

name: add-dependency description: Add a dependency to a Lean project's lakefile. Use when adding requires, dependencies, or imports to a project.

Add Dependency

Add dependencies to a Lean project with tier validation.

Quick Start

1. Identify the project and dependency
2. Check tier ordering (can't depend on higher tiers)
3. Find the dependency's current version tag
4. Update lakefile.lean with require statement
5. Run lake update and lake build

Dependency Tiers

Projects should only depend on projects in the same or lower tiers.

Require Statement Format

Copyrequire <name> from git "https://github.com/nathanial/<repo>" @ "v0.0.X"

Finding Current Version

Copycd <category>/<dependency>
git describe --tags --abbrev=0

Or check GitHub releases.

Common Dependencies

External Dependencies

Copy-- Mathlib (for collimator)
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.X.0"

-- Batteries (for ledger)
require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.X.0"

-- Plausible (for property testing)
require plausible from git "https://github.com/leanprover-community/plausible" @ "v4.X.0"

After Adding

Copylake update   # Fetch new dependency
lake build    # Verify it builds
lake test     # Ensure tests still pass

Tier Violation Warning

If adding a dependency from a higher tier, warn the user:

⚠️ Warning: Adding <dep> (Tier X) to <project> (Tier Y) violates tier ordering. This creates a circular dependency risk. Consider:

• Moving <project> to a higher tier
• Finding an alternative in a lower tier
• Extracting shared code to a new lower-tier project