Awesome-omni-skill lean-lsp

Query Lean goals, diagnostics and other information.

install

source · Clone the upstream repo

git clone https://github.com/diegosouzapw/awesome-omni-skill

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/diegosouzapw/awesome-omni-skill "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/backend/lean-lsp" ~/.claude/skills/diegosouzapw-awesome-omni-skill-lean-lsp && rm -rf "$T"

manifest: skills/backend/lean-lsp/SKILL.md

source content

What I do

Query Lean goals and diagnostics at a 1-based line/column.
Use the daemon socket to fetch results quickly (auto-starting if needed).
Provide JSON output when needed for structured processing.

When to use me

Use this when an agent needs goal state, term goals, or diagnostics from a Lean file at a specific cursor position.

Commands

Start the daemon:
- ```
scripts/lean-lsp start --root .
```
Check daemon status:
- ```
scripts/lean-lsp check
```
Stop the daemon:
- ```
scripts/lean-lsp stop
```

Plain goal:

scripts/lean-lsp plain-goal <file> <line> <col>

Term goal:

scripts/lean-lsp plain-term-goal <file> <line> <col>

Hover info:

scripts/lean-lsp hover <file> <line> <col>

Diagnostics at a position:

scripts/lean-lsp diagnostics <file> <line> <col>

All of the above:

scripts/lean-lsp all <file> <line> <col>

Raw LSP request:

scripts/lean-lsp request --method <method> --params <json>

Notification:

scripts/lean-lsp notify --method <method> --params <json>

Batch ops:
- ```
scripts/lean-lsp batch --ops @ops.json
```
JSON output (structured):
- add
```
--json
```

Notes

The daemon auto-starts when you run queries, or you can start it manually.
Auto-start uses the current working directory and default server command.
For custom root or server cmd, run
```
scripts/lean-lsp start
```
first.
Socket path defaults to
```
LEAN_LSP_SOCKET
```
or
```
./lean-lsp.sock
```
.
This skill bundles the
```
lean-lsp
```
script next to
```
SKILL.md
```
.
```
scripts/lean-lsp
```
is a wrapper that calls the bundled script.