Lean Lsp

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.