opaque sageServerRef : IO.Ref (Option (IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }))

def getSageServer : IO (IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped })

Equations

• One or more equations did not get rendered due to their size.

def sendSageRequest (req : Lean.Json) : Lean.MetaM Lean.Json

Send a JSON request to the persistent Sage server and return the parsed response object. Handles the write/read/parse/status-check plumbing so callers only need to build the request and pull fields out of the result.

Throws on JSON parse errors and on responses with status ≠ "ok".

Equations

• One or more equations did not get rendered due to their size.