agda_job_await
Collect the result of a pending Agda job by waiting up to waitMs; if it is still running, returns pending so you can check again.
Instructions
Collect the result of a pending Agda job, waiting up to waitMs; returns pending again if still running
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| job | Yes | Job id returned by a pending tool result | |
| waitMs | No | Milliseconds to wait for completion before returning pending again |