Renaming and ETA added

can now rename solves for remembering what they are and they have an ETA
for starting and finishing
This commit is contained in:
Pagwin 2026-06-19 15:31:56 -04:00
parent 0c94d94936
commit b27a73bc1f
2 changed files with 265 additions and 33 deletions

View file

@ -365,7 +365,7 @@
<fieldset> <fieldset>
<legend>Objective &mdash; scoring terms</legend> <legend>Objective &mdash; scoring terms</legend>
<p class="help">Each term scores a resource (or <code>renown</code>) at the end of a <p class="help">Each term scores a resource (or <code>renown</code>) at the end of a
turn (blank turn = final turn). For a <b>log</b> term, write a JS expression that turn. For a <b>log</b> term, write a JS expression that
evals to a one-argument function, e.g. <code>(x) =&gt; Math.log2(x + 1)</code>. evals to a one-argument function, e.g. <code>(x) =&gt; Math.log2(x + 1)</code>.
It is called over amounts <code>0..max_resource</code> in the browser to build the It is called over amounts <code>0..max_resource</code> in the browser to build the
lookup table.</p> lookup table.</p>
@ -556,9 +556,10 @@
return sel; return sel;
} }
// Multi-turn picker: a row of checkboxes ("final" + turn 0..count-1). // Multi-turn picker: a row of checkboxes for turn 0..count-1.
// _selected() returns the checked values as strings ("" = final). Registers // _selected() returns the checked turn values as strings; none checked is
// for refresh so its options track the Turns count, preserving selections. // interpreted by the caller as "every turn". Registers for refresh so its
// options track the Turns count, preserving selections.
const multiTurnGroups = new Set(); const multiTurnGroups = new Set();
function fillMultiTurnOptions(group) { function fillMultiTurnOptions(group) {
const prev = new Set((group._boxes || []).filter(b => b.checked).map(b => b.value)); const prev = new Set((group._boxes || []).filter(b => b.checked).map(b => b.value));
@ -572,7 +573,6 @@
return el("label", {style: "display:inline-block;margin-right:.6rem;font-size:.85rem"}, return el("label", {style: "display:inline-block;margin-right:.6rem;font-size:.85rem"},
[cb, " " + label]); [cb, " " + label]);
}; };
group.append(mk("", "final"));
for (let t = 0; t < turnsCount(); t++) group.append(mk(String(t), "turn " + t)); for (let t = 0; t < turnsCount(); t++) group.append(mk(String(t), "turn " + t));
} }
function multiTurnSelect(values) { function multiTurnSelect(values) {
@ -854,7 +854,7 @@
field("Resource", res), field("Resource", res),
field("Op", op), field("Op", op),
field("Value", value), field("Value", value),
field("Turn (blank=final)", turn), field("Turn", turn),
el("div", {class: "card-actions"}, removeBtn(card))); el("div", {class: "card-actions"}, removeBtn(card)));
document.getElementById("constraints").append(card); document.getElementById("constraints").append(card);
} }
@ -884,7 +884,7 @@
field("From amount", fromAmt), field("From amount", fromAmt),
field("To", to), field("To", to),
field("To amount", toAmt), field("To amount", toAmt),
field("Turn (blank=final)", turn), field("Turn", turn),
el("div", {class: "card-actions"}, removeBtn(card))); el("div", {class: "card-actions"}, removeBtn(card)));
document.getElementById("conversions").append(card); document.getElementById("conversions").append(card);
} }
@ -910,8 +910,11 @@
from_amount: +fromAmt.value, to_amount: +toAmt.value, from_amount: +fromAmt.value, to_amount: +toAmt.value,
max_count: +maxCount.value, max_count: +maxCount.value,
}; };
// No turn checked => make the conversion available on every turn.
const sel = turns._selected(); const sel = turns._selected();
return (sel.length ? sel : [""]).map(tv => { const chosen = sel.length ? sel
: [...Array(turnsCount()).keys()].map(String);
return chosen.map(tv => {
const o = {...base}; const o = {...base};
if (tv !== "") o.turn = +tv; if (tv !== "") o.turn = +tv;
return o; return o;
@ -923,7 +926,7 @@
field("To", to), field("To", to),
field("To amount", toAmt), field("To amount", toAmt),
field("Max count", maxCount), field("Max count", maxCount),
field("Turns (none=final)", turns), field("Turns (none = every turn)", turns),
el("div", {class: "card-actions"}, removeBtn(card))); el("div", {class: "card-actions"}, removeBtn(card)));
document.getElementById("optional_conversions").append(card); document.getElementById("optional_conversions").append(card);
} }
@ -987,6 +990,59 @@
: String(Date.now()) + Math.random(); : String(Date.now()) + Math.random();
} }
// Custom display names for solves, keyed by token. Persisted in
// localStorage so a rename survives reloads and shared-link loads in the
// same browser, and mirrored to the server (POST /rename) so it also
// shows for viewers who open the share link elsewhere. When unset a card
// falls back to its default "Solution n" label.
const SOLVE_NAMES_KEY = "dws_solve_names";
function loadSolveNames() {
try {
return new Map(Object.entries(
JSON.parse(localStorage.getItem(SOLVE_NAMES_KEY) || "{}")));
} catch (e) {return new Map();}
}
const solveNames = loadSolveNames();
function saveSolveNames() {
try {
localStorage.setItem(SOLVE_NAMES_KEY,
JSON.stringify(Object.fromEntries(solveNames)));
} catch (e) {/* storage may be unavailable; names just won't persist */}
}
// The label to show for a solve: its custom name, or "Solution n".
function solveLabel(token, n) {
return (token && solveNames.get(token)) || `Solution ${n}`;
}
// Adopt a server-provided name (from a status event) when this browser
// hasn't got one locally — so a shared solve renamed elsewhere shows it.
function adoptName(token, name) {
if (token && name && !solveNames.has(token)) {
solveNames.set(token, name);
saveSolveNames();
}
}
// A "Rename" button: prompts for a new name, stores it locally + on the
// server, then calls apply(label) so the card updates its displayed name.
function renameButton(token, n, apply) {
return el("button", {
class: "mini", type: "button",
onclick: () => {
const name = prompt("Rename solution:", solveLabel(token, n));
if (name == null) return; // cancelled
const trimmed = name.trim();
if (trimmed) solveNames.set(token, trimmed);
else solveNames.delete(token); // empty reverts to default
saveSolveNames();
fetch("/rename", {
method: "POST",
headers: {"Content-Type": "application/json"},
body: JSON.stringify({token, name: trimmed}),
}).catch(() => {/* local name still applies */});
apply(solveLabel(token, n));
},
}, "Rename");
}
// A share URL for a set of solve tokens. The schema is // A share URL for a set of solve tokens. The schema is
// ?solves=<id1>,<id2>,… so anyone who knows the ids can compose an // ?solves=<id1>,<id2>,… so anyone who knows the ids can compose an
// arbitrary set; a single ?solve=<id> link is also still understood. // arbitrary set; a single ?solve=<id> link is also still understood.
@ -1021,6 +1077,54 @@
reset(); reset();
} }
// --- time formatting (for queue ETAs and actual begin/finish times) ---
// Server timestamps are epoch *seconds*. fmtClock shows a wall-clock time;
// fmtRel shows a coarse "in ~Xm Ys" / "Xm Ys ago" relative to now; fmtDur
// shows an elapsed span between two epochs.
function fmtClock(sec) {
return sec ? new Date(sec * 1000).toLocaleTimeString() : "—";
}
function fmtSpan(s) {
s = Math.max(0, Math.round(s));
const m = Math.floor(s / 60), sec = s % 60;
return m ? `${m}m ${sec}s` : `${sec}s`;
}
function fmtRel(sec) {
if (!sec) return "—";
const d = sec * 1000 - Date.now();
return d >= 0 ? `in ~${fmtSpan(d / 1000)}` : `${fmtSpan(-d / 1000)} ago`;
}
function fmtDur(fromSec, toSec) {
if (!fromSec || !toSec) return "—";
return fmtSpan(toSec - fromSec);
}
// Render a pending card's status line from its latest timing snapshot
// (card._timing, set by handleJobEvent). The relative ETAs are recomputed
// here so the ticker can refresh them in place without a new server event.
function renderPendingStatus(card) {
const j = card._timing;
if (!j || !card._status) return;
if (j.status === "queued") {
const ahead = j.position > 0 ? `${j.position} ahead` : "next up";
let msg = `Queued (${ahead})`;
if (j.eta_start) msg += ` — begins ${fmtRel(j.eta_start)}`;
if (j.eta_finish) msg += `, finishes by ${fmtRel(j.eta_finish)}`;
card._status.textContent = msg + "…";
} else if (j.status === "running") {
let msg = "Solving";
if (j.started_at) msg += ` — began ${fmtClock(j.started_at)}`;
if (j.eta_finish) msg += `, finishes by ${fmtRel(j.eta_finish)}`;
card._status.textContent = msg + "…";
}
}
// Keep the relative ETAs on every still-pending card ticking without
// waiting for the next server event.
setInterval(() => {
for (const e of pending.values()) renderPendingStatus(e.card);
}, 1000);
// Build the reserved card for a queued/running solve: a spinner + status, // Build the reserved card for a queued/running solve: a spinner + status,
// the (already valid) share link, and a Cancel button. // the (already valid) share link, and a Cancel button.
function makePendingCard(token, n) { function makePendingCard(token, n) {
@ -1028,8 +1132,12 @@
card.dataset.token = token; card.dataset.token = token;
const status = el("span", {}, "Queued…"); const status = el("span", {}, "Queued…");
card._status = status; card._status = status;
// The name part of the head, updated in place when renamed.
const nameSpan = el("span", {}, solveLabel(token, n));
card._nameSpan = nameSpan;
const actions = el("p", {}, [ const actions = el("p", {}, [
copyLinkButton("Copy share link", () => shareUrl([token])), " ", copyLinkButton("Copy share link", () => shareUrl([token])), " ",
renameButton(token, n, (label) => {nameSpan.textContent = label;}), " ",
el("button", { el("button", {
class: "mini", type: "button", class: "mini", type: "button",
onclick: () => cancelPending(token), onclick: () => cancelPending(token),
@ -1038,7 +1146,8 @@
card._actions = actions; card._actions = actions;
card.append( card.append(
el("div", {class: "pending-head"}, el("div", {class: "pending-head"},
[el("span", {class: "spinner"}), `Solution ${n} — `, status]), [el("span", {class: "spinner"}), nameSpan,
document.createTextNode(" — "), status]),
actions); actions);
return card; return card;
} }
@ -1098,17 +1207,22 @@
function handleJobEvent(j) { function handleJobEvent(j) {
const entry = pending.get(j.token); const entry = pending.get(j.token);
if (!entry) return; // already finished/dismissed if (!entry) return; // already finished/dismissed
// A name set on another tab/browser arrives with the status event;
// adopt it (if we have none locally) and reflect it on the card.
adoptName(j.token, j.name);
if (entry.card._nameSpan)
entry.card._nameSpan.textContent = solveLabel(j.token, entry.n);
switch (j.status) { switch (j.status) {
case "queued": case "queued":
entry.card._status.textContent =
j.position > 0 ? `Queued (${j.position} ahead)…` : "Queued (next up)…";
break;
case "running": case "running":
entry.card._status.textContent = "Solving…"; // Stash the latest timing snapshot and (re)render the status
// line; a ticker keeps its relative ETAs fresh between events.
entry.card._timing = j;
renderPendingStatus(entry.card);
break; break;
case "done": case "done":
finishPending(j.token, (e) => finishPending(j.token, (e) =>
renderSolution(j.solution, e.card, j.token, e.n)); renderSolution(j.solution, e.card, j.token, e.n, j));
break; break;
case "cancelled": case "cancelled":
// Leave a visible "cancelled" card (whether this tab cancelled // Leave a visible "cancelled" card (whether this tab cancelled
@ -1162,7 +1276,7 @@
}).catch((e) => pendingError(token, e.message)); }).catch((e) => pendingError(token, e.message));
} }
function renderSolution(s, placeholder, token, n) { function renderSolution(s, placeholder, token, n, timing) {
// Collapse any previously-shown solutions so the new one is the focus. // Collapse any previously-shown solutions so the new one is the focus.
for (const d of document.querySelectorAll("#output details.solution")) d.open = false; for (const d of document.querySelectorAll("#output details.solution")) d.open = false;
@ -1170,14 +1284,22 @@
const details = el("details", {class: "solution", open: ""}); const details = el("details", {class: "solution", open: ""});
// Tag the card with its token so "Share visible solutions" can collect it. // Tag the card with its token so "Share visible solutions" can collect it.
if (token) details.dataset.token = token; if (token) details.dataset.token = token;
details.append(el("summary", {}, // The name part of the summary is its own span so a rename can update
`Solution ${n} — ${s.status}, objective ${s.objective_value ?? "—"}`)); // it in place without rebuilding the rest of the summary text.
const nameSpan = el("span", {}, solveLabel(token, n));
const summary = el("summary", {}, [nameSpan,
document.createTextNode(
` — ${s.status}, objective ${s.objective_value ?? "—"}`)]);
details.append(summary);
const out = details; const out = details;
// A shareable permalink to this stored solve, looked up by its UUID. // A shareable permalink to this stored solve, looked up by its UUID,
// plus a Rename button (only meaningful for a stored/shareable solve).
if (token) { if (token) {
out.append(el("p", {}, copyLinkButton("Copy share link", out.append(el("p", {}, [
() => shareUrl([token])))); copyLinkButton("Copy share link", () => shareUrl([token])), " ",
renameButton(token, n, (label) => {nameSpan.textContent = label;}),
]));
} }
out.append(el("p", { out.append(el("p", {
html: html:
@ -1185,6 +1307,18 @@
`<b>Final renown total:</b> ${s.final_renown_total}` `<b>Final renown total:</b> ${s.final_renown_total}`
})); }));
// When this tab watched the solve run, show when it actually began,
// finished and how long it took. (Solves loaded fresh from a share
// link carry no timing, so this is omitted for them.)
if (timing && timing.started_at) {
out.append(el("p", {
html:
`<b>Began:</b> ${fmtClock(timing.started_at)} &nbsp; ` +
`<b>Finished:</b> ${fmtClock(timing.finished_at)} &nbsp; ` +
`<b>Took:</b> ${fmtDur(timing.started_at, timing.finished_at)}`
}));
}
const fr = el("p", {}); const fr = el("p", {});
fr.append(el("b", {}, "Final resources: ")); fr.append(el("b", {}, "Final resources: "));
fr.append(document.createTextNode( fr.append(document.createTextNode(

122
main.py
View file

@ -52,25 +52,39 @@ def init_db():
conn.execute( conn.execute(
"CREATE TABLE IF NOT EXISTS solves (" "CREATE TABLE IF NOT EXISTS solves ("
"token TEXT PRIMARY KEY, ts REAL NOT NULL, status TEXT, " "token TEXT PRIMARY KEY, ts REAL NOT NULL, status TEXT, "
"problem TEXT NOT NULL, solution TEXT NOT NULL)") "name TEXT, problem TEXT NOT NULL, solution TEXT NOT NULL)")
conn.execute("CREATE INDEX IF NOT EXISTS idx_solves_ts ON solves(ts)") conn.execute("CREATE INDEX IF NOT EXISTS idx_solves_ts ON solves(ts)")
# Add the custom-name column to pre-existing DBs that lack it.
cols = [r[1] for r in conn.execute("PRAGMA table_info(solves)")]
if "name" not in cols:
conn.execute("ALTER TABLE solves ADD COLUMN name TEXT")
finally: finally:
conn.close() conn.close()
# Custom display names for solves, keyed by token. A solve can be renamed while
# it is still queued/running (before its row exists), so names are tracked in
# memory and written into the row when the solve is stored; renaming an
# already-stored solve also updates the row directly (see _handle_rename).
_names = {}
_names_lock = threading.Lock()
def store_solve(token, problem, solution): def store_solve(token, problem, solution):
# token is client-generated; skip blanks. INSERT OR REPLACE means a repeated # token is client-generated; skip blanks. INSERT OR REPLACE means a repeated
# token overwrites (a client could clobber its own/another's row — acceptable # token overwrites (a client could clobber its own/another's row — acceptable
# for this app; switch to a server-issued id if that ever matters). # for this app; switch to a server-issued id if that ever matters).
if not token: if not token:
return return
with _names_lock:
name = _names.get(token)
conn = _db() conn = _db()
try: try:
with conn: with conn:
conn.execute( conn.execute(
"INSERT OR REPLACE INTO solves (token, ts, status, problem, solution) " "INSERT OR REPLACE INTO solves (token, ts, status, name, problem, solution) "
"VALUES (?, ?, ?, ?, ?)", "VALUES (?, ?, ?, ?, ?, ?)",
(token, time.time(), solution.get("status"), (token, time.time(), solution.get("status"), name,
json.dumps(problem), json.dumps(solution))) json.dumps(problem), json.dumps(solution)))
conn.execute( conn.execute(
"DELETE FROM solves WHERE token NOT IN " "DELETE FROM solves WHERE token NOT IN "
@ -84,14 +98,14 @@ def fetch_solve(token):
conn = _db() conn = _db()
try: try:
row = conn.execute( row = conn.execute(
"SELECT token, ts, status, problem, solution FROM solves WHERE token = ?", "SELECT token, ts, status, name, problem, solution FROM solves WHERE token = ?",
(token,)).fetchone() (token,)).fetchone()
finally: finally:
conn.close() conn.close()
if row is None: if row is None:
return None return None
return {"token": row[0], "ts": row[1], "status": row[2], return {"token": row[0], "ts": row[1], "status": row[2], "name": row[3],
"problem": json.loads(row[3]), "solution": json.loads(row[4])} "problem": json.loads(row[4]), "solution": json.loads(row[5])}
# Solves are queued and run one at a time by a single background worker, so any # Solves are queued and run one at a time by a single background worker, so any
# number of viewers can pile requests on without being rejected — each request # number of viewers can pile requests on without being rejected — each request
@ -138,6 +152,7 @@ def _solve_worker():
if job is None or job["status"] != "queued": if job is None or job["status"] != "queued":
continue # cancelled (or vanished) before it ran continue # cancelled (or vanished) before it ran
job["status"] = "running" job["status"] = "running"
job["started_at"] = time.time()
problem = job["problem"] problem = job["problem"]
raw_problem = job["raw_problem"] raw_problem = job["raw_problem"]
max_time = job["max_time"] max_time = job["max_time"]
@ -159,10 +174,12 @@ def _solve_worker():
store_solve(token, raw_problem, sol_dict) store_solve(token, raw_problem, sol_dict)
with _cond: with _cond:
job["status"] = "done" job["status"] = "done"
job["finished_at"] = time.time()
_cond.notify_all() _cond.notify_all()
except Exception as exc: except Exception as exc:
with _cond: with _cond:
job["status"] = "error" job["status"] = "error"
job["finished_at"] = time.time()
job["error"] = f"{type(exc).__name__}: {exc}" job["error"] = f"{type(exc).__name__}: {exc}"
_cond.notify_all() _cond.notify_all()
finally: finally:
@ -171,6 +188,28 @@ def _solve_worker():
_active["solver"] = None _active["solver"] = None
def _estimate_start(token):
# Caller holds _cond. Estimate the wall-clock time (epoch seconds) at which a
# still-queued token will *begin* running: now, plus the running solve's
# remaining time budget, plus the full time budget of every queued solve
# ahead of it. Each solve's max_time is an upper bound (a search can stop
# early), so this is a worst-case "no later than" estimate.
now = time.time()
wait = 0.0
active_token = _active["token"]
if active_token:
aj = _jobs.get(active_token)
if aj is not None:
started = aj.get("started_at") or now
wait += max(0.0, aj["max_time"] - (now - started))
if token in _queue:
for ahead in _queue[:_queue.index(token)]:
j = _jobs.get(ahead)
if j is not None:
wait += j.get("max_time", 0.0)
return now + wait
def _stop_search(solver): def _stop_search(solver):
# StopSearch() exists in OR-Tools 9.x+; degrade gracefully on older builds # StopSearch() exists in OR-Tools 9.x+; degrade gracefully on older builds
# (the solve then just runs to max_time_seconds). # (the solve then just runs to max_time_seconds).
@ -215,23 +254,44 @@ class Handler(BaseHTTPRequestHandler):
# Report a queued/running solve's live state, falling back to SQLite for # Report a queued/running solve's live state, falling back to SQLite for
# a finished (or evicted-from-memory) one. The client polls this to drive # a finished (or evicted-from-memory) one. The client polls this to drive
# each pending card: queued -> running -> done (render) / error / cancelled. # each pending card: queued -> running -> done (render) / error / cancelled.
# Timing carried through to terminal states so the UI can show when a
# solve actually began/finished (and how long it took).
timing = {}
# Read the custom name without holding _cond (kept separate to avoid any
# lock-ordering coupling between _names_lock and _cond).
with _names_lock:
name = _names.get(token)
with _cond: with _cond:
job = _jobs.get(token) job = _jobs.get(token)
if job is not None: if job is not None:
status = job["status"] status = job["status"]
for k in ("started_at", "finished_at"):
if job.get(k) is not None:
timing[k] = job[k]
max_time = job.get("max_time")
if status == "queued": if status == "queued":
pos = _queue.index(token) if token in _queue else 0 pos = _queue.index(token) if token in _queue else 0
return {"status": "queued", "position": pos} eta_start = _estimate_start(token)
return {"status": "queued", "position": pos,
"eta_start": eta_start,
"eta_finish": eta_start + (max_time or 0.0),
"max_time": max_time, "name": name}
if status == "running": if status == "running":
return {"status": "running"} started = job.get("started_at")
return {"status": "running", "started_at": started,
"eta_finish": (started + max_time)
if (started and max_time) else None,
"max_time": max_time, "name": name}
if status == "error": if status == "error":
return {"status": "error", "error": job.get("error")} return {"status": "error", "error": job.get("error"),
"name": name, **timing}
if status == "cancelled": if status == "cancelled":
return {"status": "cancelled"} return {"status": "cancelled", "name": name, **timing}
# status == "done": fall through to load the stored solution. # status == "done": fall through to load the stored solution.
rec = fetch_solve(token) rec = fetch_solve(token)
if rec is not None: if rec is not None:
return {"status": "done", "solution": rec["solution"]} return {"status": "done", "solution": rec["solution"],
"name": name or rec.get("name"), **timing}
return {"status": "unknown"} return {"status": "unknown"}
# Statuses a job can't move on from — once a tracked token reaches one we # Statuses a job can't move on from — once a tracked token reaches one we
@ -289,6 +349,9 @@ class Handler(BaseHTTPRequestHandler):
if path.path == "/cancel": if path.path == "/cancel":
self._handle_cancel(parse_qs(path.query)) self._handle_cancel(parse_qs(path.query))
return return
if path.path == "/rename":
self._handle_rename()
return
if path.path != "/solve": if path.path != "/solve":
self._send(404, json.dumps({"error": "not found"})) self._send(404, json.dumps({"error": "not found"}))
return return
@ -319,6 +382,40 @@ class Handler(BaseHTTPRequestHandler):
except Exception as exc: # surface errors to the browser except Exception as exc: # surface errors to the browser
self._send(400, json.dumps({"error": f"{type(exc).__name__}: {exc}"})) self._send(400, json.dumps({"error": f"{type(exc).__name__}: {exc}"}))
def _handle_rename(self):
# Set (or clear) a solve's custom display name. Works whether the solve
# is still queued/running (name kept in memory, applied when stored) or
# already stored (the row is updated too). An empty name clears it,
# reverting the card to its default "Solution n" label.
try:
length = int(self.headers.get("Content-Length", 0))
payload = json.loads(self.rfile.read(length) or b"{}")
except Exception as exc:
self._send(400, json.dumps({"error": f"{type(exc).__name__}: {exc}"}))
return
token = str(payload.get("token") or "")
raw = payload.get("name")
name = (str(raw).strip() or None) if raw is not None else None
if not token:
self._send(400, json.dumps({"error": "missing token"}))
return
with _names_lock:
if name is None:
_names.pop(token, None)
else:
_names[token] = name
# Persist onto the stored row if the solve has already been saved.
conn = _db()
try:
with conn:
conn.execute("UPDATE solves SET name = ? WHERE token = ?", (name, token))
finally:
conn.close()
# Push the change to anyone watching this token's status stream.
with _cond:
_cond.notify_all()
self._send(200, json.dumps({"ok": True, "name": name}), no_cache=True)
def _handle_cancel(self, query): def _handle_cancel(self, query):
# Cancel iff the request's token matches a queued/running solve, so a # Cancel iff the request's token matches a queued/running solve, so a
# Cancel click (or closing tab) can't cancel a *different* viewer's # Cancel click (or closing tab) can't cancel a *different* viewer's
@ -333,6 +430,7 @@ class Handler(BaseHTTPRequestHandler):
job = _jobs.get(token) job = _jobs.get(token)
if job is not None: if job is not None:
job["status"] = "cancelled" job["status"] = "cancelled"
job["finished_at"] = time.time()
result = "dequeued" result = "dequeued"
_cond.notify_all() _cond.notify_all()
elif token and token == _active["token"] and _active["solver"] is not None: elif token and token == _active["token"] and _active["solver"] is not None: