SkillsAdd

smithery/Arthur742Ramos

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.

Installation

$ npx skills add smithery/Arthur742Ramos --skill lean-build
View on skills.sh ↗ Website ↗

Similar popular skills

Related neighbors and high-traction skills in the same topics — useful to compare before installing.

agent-browser Shared topics
vercel-labs/agent-browser

Browser automation CLI for AI agents. Use when the user needs to interact with websites, includ…

810.4K installs
azure-diagnostics Shared topics
microsoft/azure-skills

Debug Azure production issues on Azure using AppLens, Azure Monitor, resource health, and safe …

568.9K installs
azure-validate Shared topics
microsoft/azure-skills

Pre-deployment validation for Azure readiness. Run deep checks on configuration, infrastructure…

567.7K installs
supabase-postgres-best-practices Shared topics
supabase/agent-skills

Postgres best practices maintained by Supabase, for Postgres running anywhere. Load this skill …

391.6K installs
mcp-builder Similar name
anthropics/skills

Guide for creating high-quality MCP (Model Context Protocol) servers that enable LLMs to intera…

112.3K installs
web-artifacts-builder Similar name
anthropics/skills

Suite of tools for creating elaborate, multi-component claude.ai HTML artifacts using modern fr…

98.9K installs

Also in this package

Other skills from smithery/Arthur742Ramos.

npx skills add smithery/Arthur742Ramos
path-tactics 0

Browse all from smithery/Arthur742Ramos

More details

Agent compatibility

Declared targets from SKILL.md / docs. Unmarked agents are not listed — the skill may still install via the CLI.

Claude Code Not declared
Cursor Not declared
Codex Not declared
GitHub Copilot Not declared
Windsurf Not declared
Gemini CLI Not declared
Cline Not declared
OpenCode Not declared

Package contents

Files included with this skill beyond the listing page.

  • skill md SKILL.md 1,227 B
  • docs SUMMARY.md 214 B

History

  1. First recorded snapshot · 0 installs

SKILL.md

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