diff --git a/docs/analysis/cryptanalysis/report-mixer.md b/docs/analysis/cryptanalysis/report-mixer.md index fc7aead4b..fefa22a71 100644 --- a/docs/analysis/cryptanalysis/report-mixer.md +++ b/docs/analysis/cryptanalysis/report-mixer.md @@ -315,6 +315,8 @@ wall times above are under heavy sharing. | 19:3x | merge build/master, re-prove igneum-pow identical | done, IDENTICAL; pre-merge runs re-run and matched | | 19:3x | drop SIGSTOP yield, run on cores 8-95 only | no yield was ever added; run-box.sh band set to 8-95; direct nohup runs at nice 10 | | 20:20 | main: every hand-started sweep is killed by its pid file now and re-queued through `lease pool`; release builds and the class v5 suites outrank sweeps | killed cadical (box 2, 29 min lost, no result) and sibling 07 (box 1, 6 of 56 steps done, claim released); nothing started since; `lease pool` absent at 20:21, so the re-queue waits on it | +| 20:22 | `lease pool` live on both boxes (lease sha f814b447) | cadical re-queued the same minute through `lease pool 1 --owner adv-mixer --nice 10`, core 8, 1 h cap | +| 20:2x | pool rule: a sweep lease asks for at most 48 cores with --min at the least usable; when `lease status` shows a "v5 gate" or "v5 kit" waiter, finish the shard in hand and release; release builds and v5 suites outrank every sweep | adopted for any further lease; the one-core cadical lease is cleared by main to its 21:23 BST cap | ### Kill ledger (main's rule, 20:20 BST)