Report the detected Agda installation, compatibility, and active workspaces

Load and typecheck one top-level Agda module from disk

Reload and typecheck the active module in a workspace

Retrieve the current visible goals and opaque handles

Retrieve the type and local context for an opaque goal handle

Retrieve types and local contexts for several goal handles in one round trip

Retrieve constraints for the active module in a workspace

Preview a case split, or atomically apply and typecheck it with apply:true

Preview a refinement, or atomically apply and typecheck it with apply:true

Preview Agda proof search, or atomically apply and typecheck it with apply:true

Normalize an expression in workspace or goal-local scope

Infer the type of an expression in workspace or goal-local scope

Query visible and interaction-backend invisible metavariables

Collect the result of a pending Agda job, waiting up to waitMs; returns pending again if still running

Wait for the FIRST of several pending jobs to finish; use after fanning work out across workspaces

Report the state of a pending Agda job without waiting for it

Abort a pending Agda job and release its Agda command slot

List Agda jobs that are still running or awaiting collection