Production cleanup and worker reliability

Operations

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

Verification runtime

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

Semantic extraction

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

Product surfaces

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

Lean verifier and production ingest hardening

Verifier runtime

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

Cleanup

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

Production duct tape retired

Production foundations

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