name: new-project description: Scaffold a new Lean 4 project in the workspace. Use when creating a new project, library, or application.
New Project Scaffolding
Create a new Lean 4 project with the correct structure for this workspace.
Quick Start
- Determine project category and name
- Create directory structure
- Generate lakefile.lean with GitHub-style dependencies
- Create README.md and CLAUDE.md
- Set up test structure with Crucible
Project Categories
| Category | Purpose | Directory |
|---|---|---|
| graphics | TUI, GPU, widgets, rendering | graphics/ |
| web | HTTP, HTML, templates | web/ |
| network | HTTP client, protocols | network/ |
| data | Databases, data structures | data/ |
| apps | Applications | apps/ |
| util | Utilities, tools | util/ |
| math | Linear algebra, units | math/ |
| audio | Sound synthesis | audio/ |
| testing | Test frameworks | testing/ |
Directory Structure
<category>/<project>/
├── lakefile.lean
├── README.md
├── CLAUDE.md
├── <Project>/
│ └── Basic.lean
├── <Project>.lean
└── Tests/
└── Main.lean
Template: lakefile.lean
import Lake
open Lake DSL
package «projectName» where
leanOptions := #[
⟨`autoImplicit, false⟩
]
@[default_target]
lean_lib «ProjectName» where
roots := #[`ProjectName]
require crucible from git "https://github.com/nathanial/crucible" @ "v0.0.1"
lean_exe tests where
root := `Tests.Main
@[test_driver]
script test do
let result ← IO.Process.run {
cmd := ".lake/build/bin/tests"
args := #[]
}
IO.println result
return 0
Template: Main Library (<Project>.lean)
import ProjectName.Basic
Template: Basic.lean
namespace ProjectName
-- Your code here
end ProjectName
Template: Tests/Main.lean
import Crucible
import ProjectName
open Crucible
def main : IO Unit := Crucible.runTests "ProjectName" do
describe "Basic" do
it "works" do
assert true
Template: CLAUDE.md
# <Project Name>
Brief description.
## Build
\`\`\`bash
lake build && lake test
\`\`\`
## Usage
\`\`\`lean
import ProjectName
\`\`\`
Naming Conventions
- Directory: lowercase with hyphens (e.g.,
my-project) - Package: lowercase with hyphens in lakefile
- Library/namespace: PascalCase (e.g.,
MyProject) - GitHub repo: matches directory name (except
chronos→chronos-lean)
After Creation
-
lake buildto verify structure -
lake testto run initial tests -
git init && git add -A && git commit -m "Initial commit" - Create GitHub repo and push
- Add to workspace CLAUDE.md project list
chat Comments (0)
Sign in to join the discussion and leave a comment.
Skill Details
GitHub Stars
0
GitHub Forks
0
Created
Jan 2026
Last Updated
5个月前
tools
tools automation tools
Related Skills
Build your own?
Join 12,000+ developers contributing to the Claude ecosystem.
No comments yet. Be the first to share your thoughts!