Lean 4 Build & Debug

Build the ComputationalPaths Lean 4 project using Lake.

Essential Commands

# Build entire project
lake build

# Build specific module
lake build ComputationalPaths.Path.CompPath.CircleCompPath

# Clean and rebuild
lake clean && lake build

# Run executable
lake exe computational_paths

Common Build Errors

Debugging

#check myTerm             -- show type
#print axioms myTheorem   -- show axioms used
#reduce myTerm            -- fully normalize

Toolchain

• Current: leanprover/lean4:v4.24.0 (see lean-toolchain)
• Update: edit lean-toolchain, then lake clean && lake build