# Init Merlean

> Set up the MerLEAN system in this repo (replaces the old src/deploy.sh) — build the shared Python .venv from src/requirements.txt, write the root .mcp.json for the lean-lsp MCP server, ensure an OpenAI key in .env, and prepare the root Lean + Mathlib workspace (lake update / cache get / build). Use when asked to install, set up, initialize, or (re)deploy MerLEAN, or when a fresh clone needs its r…

- **Type:** Skill
- **Install:** `agentstack add skill-merleanprover-merlean-init-merlean`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [MerLeanProver](https://agentstack.voostack.com/s/merleanprover)
- **Installs:** 0
- **Category:** [AI & ML](https://agentstack.voostack.com/c/ai-and-ml)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [MerLeanProver](https://github.com/MerLeanProver)
- **Source:** https://github.com/MerLeanProver/MerLean/tree/master/.claude/skills/init_merlean

## Install

```sh
agentstack add skill-merleanprover-merlean-init-merlean
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# init_merlean — one-command MerLEAN setup

`.claude/` (skills + agents + settings) is tracked in git, so there is nothing to "deploy":
this skill prepares the **runtime** only. Everything is done by one idempotent, non-interactive
script:

```
bash .claude/skills/init_merlean/setup.sh [--openai-key sk-...] [--skip-venv] [--skip-mathlib]
```

## Procedure

1. **Key first.** Check whether an OpenAI key is already reachable: `.env` at the repo root
   contains `OPENAI_API_KEY=sk-...`, or `OPENAI_API_KEY` is set in the environment. If neither,
   ask the user for their key (it is required by the Mem0-g plan graph for embeddings/rerank);
   they may also skip and fill `.env` in later.
2. **Run the script** (from the repo root):
   - key in hand → `bash .claude/skills/init_merlean/setup.sh --openai-key `
   - key already reachable, or user skipped → `bash .claude/skills/init_merlean/setup.sh`
   - The Mathlib step (`lake update` + `lake exe cache get` + `lake build`) can take many
     minutes on first run — run it with a generous timeout or in the background. Pass
     `--skip-mathlib` only if the user asks for a quick/venv-only setup.
3. **Read the check block** the script prints at the end. All three must be `[ok]`:
   `lean-lsp-mcp` importable from the venv, `lake` on PATH, `plan_store` importable.
   - `lake not found` → tell the user to install Lean via `elan`
     (https://leanprover-community.github.io/get_started.html), then re-run this skill.
   - venv failures → the script already tried `ensurepip`/`get-pip` and a `uv` fallback;
     report the pip error to the user.
4. **Restart note.** If `.mcp.json` was just (re)generated, tell the user the `lean-lsp` MCP
   server loads on the next Claude Code session start.

## What the script does (all idempotent)
| step | action |
|---|---|
| venv | build `.venv/` from `src/requirements.txt` (host python ≥ 3.9, else `uv` fallback) |
| .env | write from `--openai-key`, else preserve an existing key, else leave the template |
| .mcp.json | generated from `templates/mcp.json` — registers the `lean-lsp` MCP server, run from the venv python |
| Lean workspace | copy `lean-toolchain` / `lakefile.toml` / `MerLeanExperiment.lean` to the root if missing, then `lake update` + `lake exe cache get` + `lake build` (toolchain auto-synced to Mathlib's) |
| checks | `lean-lsp-mcp` import, `lake` on PATH, `plan_store` import |

Existing root files (`.env`, `lean-toolchain`, `lakefile.toml`, `MerLeanExperiment.lean`) are
**never overwritten** (only `.mcp.json` is regenerated). Re-running after a failed step is safe.

After setup, the plan-graph CLI is invoked as
`.venv/bin/python src/cli.py --data  `
(Windows/Git Bash: `.venv/Scripts/python.exe`) — see the `plan-graph` skill.

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [MerLeanProver](https://github.com/MerLeanProver)
- **Source:** [MerLeanProver/MerLean](https://github.com/MerLeanProver/MerLean)
- **License:** Apache-2.0

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** yes
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-merleanprover-merlean-init-merlean
- Seller: https://agentstack.voostack.com/s/merleanprover
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.