Login

Production cleanup and worker reliability

Operations

  • Production Cleaned production database state on June 3, 2026 after the recent production ingest and runtime repair pass.
  • Deploys Kept deploy SSH sessions alive while workers drain, and labeled verifier runtimes so deploy cleanup removes the right orphaned containers.
  • Worker leases Renewed worker leases through graceful drain so long-running verifier jobs do not look stale during a restart.
  • Podman Repaired rootless Podman runtime store state, pinned runtime directories, and made production smoke checks run from a stable service path.

Verification runtime

  • Build executor Added a detached systemd build executor option with one-shot job entrypoints, heartbeat renewal, restart reattachment, and memory/runtime controls.
  • Isolation Allowed rootless verifier namespaces, made read-only source bind mounts create their source directories first, and pinned cache directories to absolute paths.
  • Timeouts Split semantic extraction and checker timeouts, and made OCI command cleanup idempotent after timeout paths.
  • Recovery Made startup workspace reaping aware of active job state so recovery avoids deleting work still owned by detached jobs.

Semantic extraction

  • Lean Parallelized the Lean semantic extractor across local modules while preserving proof-internal dependency edges.
  • Scopes Added verification-scope replay contracts, module-set checker jobs, and declaration-cone module builds.
  • Cache Split declaration semantic cache observations, skipped full extraction on cache hits, and added a Lean semantic runner cache smoke.
  • Scheduler Prioritized explicit scheduler work and treated poller heads as eager branch tips for fresher repository checks.

Product surfaces

  • Theorems Reworked the theorem page into a signal cockpit, then lightened the metadata sidebar and calmer collaboration surface.
  • Projects Added a cheap formalization-summary endpoint, registered it in the auth matrix, and stopped the projects registry from fanning out across heavier calls.
  • Review Shipped a unified review queue, clearer semantic-drift table names, and quick UI wins for maps, drift severity, dependency labels, project actions, and header behavior.
  • Settings Split settings by scope and promoted team AI controls into a live control panel.

Lean verifier and production ingest hardening

Verifier runtime

  • Toolchains Retired legacy non-elan verifier rows, guarded non-container image refs, and kept Lean toolchains on the shared elan-base image.
  • Rootless OCI Made Lean builds work in the rootless sandbox by disabling tar owner restoration for mathlib cache extraction.
  • Persistence Stopped per-phase Lean environment values from shadowing the shared elan volume, so offline checker phases reuse provisioned toolchains.
  • Extractor Resolved Lean and Lake binaries through elan inside the semantic extraction helper when they are not already on PATH.

Cleanup

  • Disk Reaped stale per-job source and runtime directories on worker startup to recover large dead checkouts after interrupted builds.
  • Jobs Self-healed per-repository build run number allocation so drifted counters cannot collide with existing run numbers.
  • Blueprints Ran blueprint generation as a non-fatal verifier phase and rebased generated absolute inputs under the collected artifact root.

Production duct tape retired

Production foundations

  • Worker Added heartbeat writes, graceful shutdown joins, and lease-based recovery for stale jobs.
  • Ops Added database health, worker-heartbeat, queue-depth, failure-rate, webhook alert, and admin telemetry paths.
  • Blueprints Detected LeanBlueprint artifacts after successful builds and queued background auto-import.
  • Deploys Pinned deploys to the GitHub SHA, checked out detached code on the host, and set systemd stop windows to match long verifier jobs.

Keyboard shortcuts