Query Lean goals, diagnostics and other information.
Use this when an agent needs goal state, term goals, or diagnostics from a Lean file at a specific cursor position.
scripts/lean-lsp start --root .scripts/lean-lsp checkscripts/lean-lsp stopscripts/lean-lsp plain-goal <file> <line> <col>scripts/lean-lsp plain-term-goal <file> <line> <col>scripts/lean-lsp hover <file> <line> <col>scripts/lean-lsp diagnostics <file> <line> <col>scripts/lean-lsp all <file> <line> <col>scripts/lean-lsp request --method <method> --params <json>scripts/lean-lsp notify --method <method> --params <json>scripts/lean-lsp batch --ops @ops.json--jsonscripts/lean-lsp start first.LEAN_LSP_SOCKET or ./lean-lsp.sock.lean-lsp script next to SKILL.md.scripts/lean-lsp is a wrapper that calls the bundled script.