SKILL.md

name: lean-build description: 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.

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.HIT.Circle

# 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

Score

Total Score

60/100

Based on repository quality metrics

✓SKILL.md

SKILL.mdファイルが含まれている

+20

✓LICENSE

ライセンスが設定されている

+10

○説明文

100文字以上の説明がある

0/10

○人気

GitHub Stars 100以上

0/15

○最近の活動

3ヶ月以内に更新がある

0/10

○フォーク

10回以上フォークされている

0/5

✓Issue管理

オープンIssueが50未満

✓言語

プログラミング言語が設定されている

○タグ

1つ以上のタグが設定されている

0/5

lean-build