Report computation
report_computationSay how a computation an issue rests on stands — a GAP run, a batch of work units, a Lean build that ran somewhere else; the tracker runs nothing. Call it when the job is submitted, as it progresses and when it ends, with the same 'source' + 'externalId' every time: that is one job, updated, never a second. Send only what you know now — a field left out keeps what an earlier report said, so a progress report need not repeat the commit. 'state' is queued, running, done, failed, cancelled or lost (a job whose runner stopped answering); 'starting' reads as running. Report the commit it ran at and the repository's web address: that is what makes a [computer] result checkable, and the answer's 'commitUrl' links it where the host is GitHub or GitLab. 'result' is what came of it, in a sentence — Markdown and $…$ formulas work. Answers with 'created' and 'stateBefore'. A name already reported on another issue is refused with that issue's key. Requires permission to edit the issue.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| key | Yes | The issue the computation answers, e.g. 'MATH-74'. | |
| url | No | The job's own page on its runner (http/https). | |
| state | No | queued, running, done, failed, cancelled or lost. | |
| title | No | What it computes, in words, e.g. 'rank 5, order 2^11, stage C'. | |
| commit | No | The commit it ran at. | |
| result | No | What came of it, a sentence or two. Markdown, $...$ formulas. | |
| source | Yes | Who runs it, e.g. 'tm' or 'boinc'. The job's name is unique within it. | |
| command | No | How it was run: the command line or the job's description. | |
| outputUrl | No | Where its output can be fetched (http/https). | |
| startedAt | No | When it started (ISO 8601). Left out, a move to running stamps now. | |
| externalId | Yes | The job's own name there, e.g. 'kimmy/gap/m74r5u'. The same name again updates the job. | |
| finishedAt | No | When it ended (ISO 8601). Left out, a move to a finished state stamps now. | |
| repository | No | The repository's web address, e.g. 'https://github.com/org/repo'. | |
| progressDone | No | How much is done, as the runner counts, e.g. 812. | |
| progressTotal | No | Out of how much, e.g. 1695. |