feat: lake: make job cancellation a first-class JobState flag

[dennj]

This PR makes job cancellation under --fail-fast a first-class notion: canceled jobs are reported as ⊘ Canceled rather than as successes, and a canceled dependency is no longer misreported as a bad import.

This is the follow-up anticipated in #14797's review, where cancellation is recognized by convention (a trace-level log entry with a marker string). Here it is recorded natively as JobState.canceled, a per-result flag alongside the existing wantsRebuild, which already has exactly this shape (a per-result Bool, merged with ||, read by the monitor). Precedence is therefore defined once, in JobState.merge, for every combinator: failure still dominates, because the monitor keeps computing failed from the log exactly as before and treats a job as canceled only when it did not itself fail. JobResult.isCanceled reads the flag; the marker string and its "for internal use only" constant are removed.

Unlike the first-class attempt in #13075, the error type is unchanged. Cancellation rides in state that already flows through every combinator, so Job.await, ensureJob, and job registration are untouched and no boundary has to translate a cancellation into something lossy, which is what caused the diagnostic-loss and fabricated-error bugs the earlier approach had. Exit codes, --wfail, and log replay are unaffected since failed is computed as before.

What is still missing

• In-flight builds are not yet interrupted: once the token is set, a lean process already running still elaborates to completion, so fail-fast exit time is bounded by the slowest in-flight module. Killing it cleanly needs the canceled state this PR introduces.
• --fail-fast is still the only thing that sets the token. Graceful Ctrl-C handling and build timeouts are natural future consumers.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-19 02:27:28)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 13:27:09)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fd0efc4306a7773c2cd4e079ddaa907426d0f5da --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-22 02:10:25)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8af42c4eb193246a86bf97c72f58dc03b29a4216 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-25 12:59:29)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14835 has successfully built against this PR. (2026-08-19 03:39:01) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03d7a4efd5f74dc886ba33eab424611146d49e03 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 13:27:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd0efc4306a7773c2cd4e079ddaa907426d0f5da --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-22 02:10:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8af42c4eb193246a86bf97c72f58dc03b29a4216 --onto fd0efc4306a7773c2cd4e079ddaa907426d0f5da. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 12:59:27)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8af42c4eb193246a86bf97c72f58dc03b29a4216 --onto 4620e4d946957ae7c582764c79eb93cc779f77e2. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 18:15:52)

[dennj]

@marcelolynch is this the kind of native cancellation you were looking for?

[tydeu]

Both these cases should probably be handled instead via a variant of wait? that checks the result for cancelled itself and rethrows on canceled (so, it would need to be JobM instead of BaseIO). The other uses of wait? are also impacted by the new cancellation (they are the job monitor caveats), which indicates that wait? is correct vector for this check.

[dennj]

Added Job.waitUnlessCanceled? : Job α → JobM (Option α), which rethrows via cancelJob on a canceled job, so both sites are back to their original let some x ← … | fallback shape.

Both callers run in FetchM, and lifting JobM into FetchM keeps only the log, not the canceled flag. So at these two sites a cancellation surfaces as a plain error without the flag (as it did with the hand-rolled version). The monitor's wait? uses are BaseIO, so they'd need an explicit isCanceled check instead. I left it here, since a canceled top-level job isn't reachable under --fail-fast alone