Profile My skills Saved Collections Edit profile Submit a skill

Lean Build

Build, test, and debug Lean 4 projects using Lake. Use when building the ComputationalPaths project, checking for errors, running tests, cleaning artifacts, or debugging Lean 4 compilation issues. Use when this capability is needed.

tomevault-io e9e40b4 2 files · 2.1 KB Updated
Coding & Dev Tools

File contents

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

Error Solution
unknown identifier Check imports, use fully qualified name
type mismatch Add type annotations or use @ for explicit args
must be marked as 'noncomputable' Add noncomputable keyword
universe level mismatch Ensure consistent universe variables (typically Type u)

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

Converted and distributed by TomeVault — claim your Tome and manage your conversions.

tomevault-io/skills-registry/tree/main/arthur742ramos--computationalpathslean--lean-build commit e9e40b4a6d

Browse category

Frequently asked questions

npx skillmds@latest add tomevault-io/lean-build