For the legacy TauCeti project, TAUCETI_LEGACY_DATA_ROOT selects an absolute
directory containing state/, checkouts/, and logs/. Set it before starting
a worker to reuse its existing credentials, recovery records, and checkouts
with a different installed code revision. Round, verification, and cleanup
subprocesses inherit the same location; bundled scripts and prompts remain with
the code. Without this setting, the existing installation-relative layout is
preserved. Changing the setting does not move data or merge worker histories.
TauCetiFleet can supervise a separate worker configuration without adopting this
account's existing manager. Its TAUCETI_FLEET_ADMISSION_FILE names a private,
controller-owned version-1 JSON policy with expires_at and an allowed workers
list. The controller refreshes it while running. Missing, malformed, expired, or
clock-inconsistent policies prevent new rounds and paid Claude API admissions;
an already-started agent session runs to completion. Workers report
waiting-capacity while draining instead of being terminated. Workers without
the environment variable behave as before.
TAUCETI_FLEET_MACHINE_ID and TAUCETI_FLEET_EVENTS opt into a private JSONL
provenance journal. Successful PR creation and GitHub mutations record machine,
worker, repository and PR identity. Branch pushes record assistance when the PR
identity is known. These observations are statistics only: they never authorize
CI, reviews, merges, cache publication, or another GitHub mutation. No request
body, command line, credential or agent prompt is retained. Event reporting is
best effort and cannot fail a successful publication.
Fleet's admission policy may also contain advisory roadmap_focus: areas
(directory names), workers (designated slots), and optional fractional_worker
and fractional_percent for a fractional slot. Designated workers select an
area before their survey from the intersection of that list and their eligible
live areas, then run the normal maintenance, review, and authoring cascade within
that area. The fractional slot takes that draw with the supplied integer
percentage each round. Other workers retain the full random draw. Explicit --roadmap-only and
--roadmap-skip settings retain precedence; the usual maintenance and review
priorities apply within the chosen area. Stale/malformed focus or no remaining
eligible focus areas falls back to ordinary selection. Fleet controls this live through
tauceti-fleet focus HOST --percent 20 --areas PDE,SymplecticGeometry; changing
it does not restart workers or change admissions. The share describes focused
slots, not runtime or output quotas. Focused slots retain the shared account-wide
open-PR limit. If that limit prevents authoring and the selected area has no
available maintenance, the slot falls back to the ordinary global cascade.
Fleet installers can query _fleet-protocol to verify this integration before
starting workers. The response is local, contains no credentials, and launches
no agents.
On Linux, Fleet sets TAUCETI_WORKER_SLICE to keep each worker's entire process
tree in an independent systemd scope, sharing the existing pool's memory and CPU
limits. A manager-service restart preserves these workers and adopts them again.
Explicit Fleet updates stop the worker slice, including surviving scopes; a
manager-service stop alone is not a whole-fleet stop. manager-stop still stops
workers unless --leave-workers is selected. Scope setup errors are reported as
degraded isolation and work continues in the same wrapper process. Journal and
status storage are never required for recovery. Standalone and macOS managers
retain their existing launch and shutdown behavior.
Persistent workers are declarative. You describe the workers you want in
workers.toml, and a manager process reconciles reality against that file:
starting missing workers, stopping removed ones, restarting changed ones, and
backing off repeated failures. They do not belong to a terminal session.
Bot-authored bump-mathlib/ PRs hosted on TauCeti are repaired until they land.
Their build, rebase, review-error, review-fix and contest attempts are not permanently
capped. Existing loop backoff, quota pacing, branch claims,
and explicit holds still apply. Workers checkpoint coherent partial source repairs
before their round deadline; full CI, audits, and current-head reviews authorize merging.
Bump work comes before all other work in every round. Each enabled stage's
candidates on a bump PR (conflicts, a red build, review findings and pending
reviews) are offered first, in stage order, ahead of progress reports and
every other PR, and a bump review does not wait for its previous reviewer's
first-refusal window. Main lands large batches every half hour or so, so a bump
that waits its turn goes stale before it can be admitted. No worker is reserved
for bumps: one branch claim serializes edits anyway, and every worker whose
only list includes the stage picks the bump first.
After a host round pushes a new bump head, the worker runs the full local
verifier (tauceti verify, bump policy) on that exact commit with the same
build-cache view the agent used. If it succeeds and GitHub still reports that
commit as the PR head, the worker applies self-tested. The TauCeti picker
then checks eligibility itself (the labeler's team membership, bump-only paths
and the real bump-guard validation) and posts the PR-bound assertion, so
review and queue admission need not wait for the ordinary PR build. The agent's
own claims are never consulted. Bubble rounds, a dirty checkout, a moved head,
or a failed or incomplete verification (capped at 45 minutes) leave the PR on
ordinary CI, which the push has already started. If the push's own picker run
removes the label, the worker applies it once more. Set
TAUCETI_BUMP_SELF_TESTED=0 in a worker's env to turn this off.
For genuine Git conflicts, a tended PR gets three rebase attempts between verified progress checkpoints.
The ordinary survey records a checkpoint when the current head has a successful
build status, GitHub reports it mergeable, and it has no needs-rebase label.
A distinct green head can renew the allowance once; rebuilding or repeatedly
observing the same head cannot.
Unverified pushes, comments, agent exit codes, failed or pending CI, unknown
mergeability, drafts and hold labels do not renew it.
Trusted merge-sweep handoffs retain the existing three-attempt per-PR cap. A
handoff can start from a branch that is already green and mergeable, so another
green push does not establish that the reconciliation succeeded. A missing or
failed handoff-comment read never bypasses the needs-rebase label's hold on
budget renewal.
The evidence comes from the existing survey, without extra GitHub reads or agent sessions. Each worker keeps its checkpoints with its existing counters. A round charges and refunds the allowance it selected even if another survey observes new progress while that round is running. Old integer counter files remain intact; PRs with no verified checkpoint keep their existing allowance. This is a per-worker bound, as before, not a fleet-wide attempt limit. Unreadable or malformed checkpoint/counter evidence suppresses rebase work with a diagnostic reason. Counter and checkpoint writes use atomic, synced replacement.
Nothing needs to exist first. workers add creates the config, writes the
definition, and starts a manager:
tauceti workers add # an enabled worker1, the whole cascade
tauceti workers add reviewer --only review # a focused, named worker
tauceti workers # desired and actual state
tauceti workers logs --follow reviewer # its durable console logDay-to-day controls:
tauceti workers disable reviewer # persist desired stopped state
tauceti workers enable reviewer # and start it again
tauceti workers restart reviewer # without changing desired state
tauceti workers remove reviewer # drop the definition and stop itworkers add cannot express every field, and it rewrites the file in canonical
form, dropping comments and hand formatting. To keep those, or to set a field
add does not cover, edit the file and apply it:
tauceti workers edit # $VISUAL, else $EDITOR, else vi
tauceti workers apply --check # validate without reconciling
tauceti workers apply # reconcile, starting a manager if neededworkers edit does not start a manager on its own; workers apply is the
explicit follow-up. A later enable, disable, add, or remove normalizes
the file again, so comments do not survive one.
A small configuration might look like this. The repository also includes
workers.toml.example.
version = 1
[[workers]]
id = "worker1"
enabled = true
[[workers]]
id = "worker2"
enabled = true
agent = "codex"
only = ["rebase", "review"]
ignore_quota = trueYou can edit workers.toml while the manager is running. It reloads the file
each cycle. If your edit does not validate, the manager keeps the last good
generation, leaves running workers alone, and says so once:
tauceti workers: invalid configuration; keeping last good generation: ...
The first of these that is set wins:
| Source | Path |
|---|---|
tauceti workers --config PATH |
exactly that file |
$TAUCETI_WORKERS_CONFIG |
exactly that file |
$TAUCETI_CONFIG_HOME |
$TAUCETI_CONFIG_HOME/workers.toml |
$XDG_CONFIG_HOME |
$XDG_CONFIG_HOME/tauceti/workers.toml |
| macOS default | ~/Library/Application Support/tauceti/workers.toml |
| otherwise | ~/.config/tauceti/workers.toml |
--config belongs to tauceti workers itself, not to the action, so it goes
before the action name: tauceti workers --config ./workers.toml apply.
Writes take an flock on a sibling workers.toml.lock, then replace the file
atomically, so concurrent CLI and dashboard mutations serialize instead of
clobbering each other.
The file supports two top-level keys. version is required and must be 1;
workers is an optional array of tables and defaults to an empty array. Any
other top-level key is an error, as is any unrecognized field inside a
[[workers]] table. Duplicate ids are rejected.
| Field | Type | Default | Notes |
|---|---|---|---|
id |
string | required | [a-z0-9-]+, at most 40 characters; namespaces the worker's state, checkout, review store, and logs |
enabled |
bool | true |
Desired running state. false stops the worker without forgetting it |
agent |
string | "auto" |
auto, codex, claude, kiro, deepseek, or minimax |
github_account |
string | unset | GitHub login to select and verify for this worker. Independent of the agent account; changing it restarts the worker. Requires that account's stored gh credential or a matching environment token |
max_open_prs |
positive integer | 32 |
Open-PR cutoff for roadmap authoring. CLI --max-open-prs and TAUCETI_MAX_OPEN_PRS also configure it. Science-account workers use 128. |
github_state_url |
string | public Tau Ceti mirror | Shared GitHub state service. Clients use its newest available data, with direct fallback on unavailable coverage or transport. See service operations. |
github_state_token_file |
string | unset | Private client-token file for the service; installation credentials stay on the server. |
only |
string list | [] |
Work phases: rebase, bump, progress, fix-ci, fix, review, roadmap, lint-repair, overlap-scan, overlap-fix. Empty means the automatic cascade. Set TAUCETI_OVERLAP_BATCH_COMMITS through env to override the calibrated 160-commit scan batch. |
claude_billing |
string | "subscription" |
"api" requires agent = "claude"; API mode bypasses subscription quota polling |
budget |
bool | false |
Admit API sessions through the shared local grant ledger; active sessions are never cut off by funding |
anthropic_api_key_file |
string | unset | Private key-file path for API mode; otherwise use ANTHROPIC_API_KEY; never store a raw key in config |
sandbox |
string | "host" |
host or bubble. Progress-report rounds always run on the host |
ignore_quota |
bool | false |
Skip soft pacing. Provider hard limits still apply; an auto worker cannot launch with this enabled |
auto_refresh |
bool | false |
Renew this worker's Claude access token when it expires, instead of parking until a human runs claude. Only safe when nothing else uses the same credential file — the refresh token is single-use. See quota and pacing |
roadmap_only |
string | unset | The single roadmap area for roadmap rounds. "" means all areas; unset means a fresh random area each round |
roadmap_skip |
string list | [] |
Roadmap areas to exclude. roadmap_only wins on overlap |
roadmap_extra_identities |
string list | [] |
Extra GitHub logins whose claimed intentions count as this worker's own |
extra_roadmap_prompt |
string | unset | Operator guidance rendered into the roadmap prompt, steering target choice within the designated roadmap. Not blank, at most 4096 characters; other phases ignore it |
respect_claims |
bool | true |
Whether to avoid intentions others have claimed |
source |
string | unset | Supplementary repository directory or URL. Requires roadmap in only and a non-empty roadmap_only |
author_model |
string | unset | Exact authoring model. Requires an agent other than auto |
author_effort |
string | unset | Authoring reasoning effort for Codex, Claude, or Kiro. Requires an explicit agent |
pace |
string | unset | Pacing curve as time%:budget% points, for example 0:10,50:70,90:90; rejected by apply --check if malformed |
stream |
bool | false |
Keep the agent transcript in the console log instead of a separate file |
isolate_home |
bool | false |
Force credential isolation for the id default; every other id already enables it |
restart |
string | "always" |
always after any exit, on-failure after a nonzero exit, or never; explicit restart and re-enable still work |
env |
table of strings | {} |
Extra environment for this worker's process tree, for settings with no flag of their own. Values must be quoted strings, names POSIX-portable, and the table at most 16 KB. The variables the worker sets itself (TAUCETI_MANAGED, TAUCETI_LOG_FILE, TAUCETI_PARENT_PIPE_FD, TAUCETI_DATA_HOME, and the runtime-status path) are rejected. Not a secret store — see below |
The manager fingerprints each definition. It stops a worker when enabled
becomes false and restarts an enabled worker when any other field changes,
without disturbing unchanged workers.
env exists for running one worker differently from its peers when the
difference has no flag: an A/B of a build setting, for instance. It is part of
the fingerprint, so editing it restarts that worker and leaves the others alone,
and both workers status and the dashboard name the variables it sets, so the
odd worker out is visible rather than mysterious.
Put no secrets in it. The values are stored in plain workers.toml, and the
whole worker definition is handed to its runner on a command line, where any
process running as you can read it. Credentials belong in the provider
mechanisms tauceti already uses (CLAUDE_CONFIG_DIR, CODEX_HOME,
KIRO_API_KEY), which keep them in files rather than argv. Status output prints
only the variable names for the same reason.
Every worker enables LAKE_ARTIFACT_CACHE=1 and
LAKE_RESTORE_ARTIFACTS=1 by default. The second setting belongs with the first:
with the artifact cache writable, Lake may keep a build product in its store
instead of the build directory, and TauCeti's audits (lake exe axioms, lake exe module-system) resolve .oleans through the Lean search path. Restoring the
copy keeps them working, and measured on a 1500-declaration module, returning to
a previously built state still fell from 4s of recompilation to 0s of restore.
An explicit value in a worker's env table overrides either default.
The trade is disk: old build generations remain in the store, and Lake supplies
no selective eviction — lake cache clean empties it all or nothing. TauCeti
records the toolchain on canonical main for each worker and clears that
worker's default Lake cache when the pin changes. The first observed pin only
seeds that record. Worker-private build/cache generations also expire after
72 hours and are recycled at the next round boundary, even when a worker keeps
completing short rounds. An operator-supplied external LAKE_CACHE_DIR is never
deleted automatically.
Private generated data is recycled after 72 hours at an ordinary round boundary, under the worker's existing round lock. Storage age does not terminate rounds; configured deadlines and owned-process-group cleanup continue to apply. Cleanup requires no PID namespace or containment marker/proof. An active, mounted or uncertain candidate is skipped locally and retried later, without pausing other cleanup or worker progress.
tauceti cleanup --dry-run reports eligible generated paths without changing files
or stopping processes. Space-pressure snapshot collection may stop earlier in a
real run once headroom recovers; candidate counts do not estimate reclaimed bytes.
tauceti cleanup performs reclamation. Both discover retired
workers from local storage, without GitHub requests. A live loop recycles its own private cache generation under its round lock;
the hourly collector skips that loop's workspace whenever its instance-lock file
is open and never takes that lock itself. Independent verification job leases and pending
references protect their caches and source too. An inactive checkout can be removed in full only after source recovery
succeeds and its remaining Git state can be safely discarded. Failed source
preservation retains source while recognized build caches can still be reclaimed.
The existing cleanup service also processes retained checkout roots, using
resumable deletion batches. Safety checks finish before scheduling yields;
activity reporting only inventories and requests that background work when the
timer is installed. Uncertain candidates are skipped while unrelated work continues. It
archives extra commit/reflog tips in existing v1 bundles. Stashes, notes, native
Git operations and credential-like files keep their original checkout when the
recovery format cannot capture them. This is generated
data retention; it does not discard uncaptured Git history to meet an age target.
Credentials, review outboxes, source recovery, usage journals and budget accounting
are preserved. Existing installations get one 72-hour grace
period when their generation marker is first recorded, including checkout removal.
Without local process-file observations, diagnostic candidates are skipped; private
cache recycling can still run at the worker's own safe boundary.
Cleanup also expires closed diagnostic .log files, inactive verification attempts,
and unused immutable Mathlib snapshots in an existing login-wide pool after three
days. Snapshot GC uses existing reader leases; cleanup does not create an absent
pool or enable sharing. The default Mathlib archive pool now lives under the TauCeti-owned build-cache root
and is collected too. Operator-selected external caches and the old interactive
~/.cache/mathlib directory remain outside the collector.
Default session logs rotate daily even while a loop keeps running, without
redirecting helpers' result pipes or files. Diagnostic age is based on last write;
private workspace age is a generation timestamp, not dependency file modification time.
A partially blocked recycling attempt starts the next generation for other caches;
interrupted deletions retry without removing a younger replacement. Closed logs
and inactive verification attempts are collected even while the worker's round lock
is held, using their own open-file checks, leases and pending references.
On Linux, tauceti cleanup --install-timer installs a persistent hourly systemd
user timer at low CPU/I/O priority, including a catch-up run after downtime. It is
scoped to the selected project's storage roots; it does not discover other projects
from worker configuration files. There is no macOS cleanup schedule in this change;
private cache generations still recycle at round boundaries there. Installing the Linux
worker service installs this timer too; existing services can install it separately
without restarting workers. Cleanup uses one collector lock and resumes interrupted
directory deletions. The same background collector drains already-retired recovery trash
with a separate 30-second, 32-GiB deletion slice and the existing recovery lock/cursors.
It never archives or deletes unpublished recovery records in that pass. Retained caches
can be reclaimed while source preservation waits. Directed pressure requests prefer private
artifact archives and prefer workers without active rounds or verification continuations.
If every worker is busy, one is still selected for reclamation at its next safe boundary.
Ordinary pressure preserves young build trees. At critical headroom, workers retain their
independent emergency reclamation at safe round boundaries, including throughout the existing
recovery hysteresis band; a missing collector or damaged request cannot suppress that path.
A concrete out-of-space error during cache preparation also
unlinks closed diagnostics before the existing single retry, without synchronously
archiving source or recursively collecting other workers' workspaces. Further failures follow normal
worker backoff. Byte and free-space thresholds also trigger collection before the age limit.
Removing the worker service leaves the cleanup timer installed so retired workers
can still be reclaimed. To remove that schedule explicitly, run
systemctl --user disable --now tauceti-cleanup.timer.
The last cleanup result (counts, at most 100 sample paths per category, failures and remaining free bytes) is included in prepared activity data. Reading status does not scan storage or contact GitHub. Shared Mathlib rollout remains off; this collector does not change its policy or complete the natural rollout gates in #311.
Host preparation downloads CI metadata into a fresh temporary Lake cache, expands verified archives into the machine pool, and populates each worker's private native Lake cache. Unchanged artifacts can then be restored by Lake without repeated decompression. Publication checks archives and extracted files with the selected Lean toolchain's own content hash. Mutable output/revision metadata is copied, while immutable artifacts use hard links where possible. Recompilation unlinks outputs before replacing them. Unsupported toolchains, contended entries and unavailable shared storage use ordinary private caches automatically. Full-project verification and Lake's build-input invalidation remain enabled.
Each preparation decodes the fresh download mappings once and reuses them through transfer and expansion. Private metadata is checked again on the next preparation; there is no persistent readiness marker. Hydration writes only changed mappings and missing artifacts. Archive seeding skips duplicates, and an archive removed concurrently by pool collection is an individual cache miss for Lake to fetch. Native fetch arguments and Mathlib snapshot keys/inventory checks are unchanged.
The existing pool status receipt also records mapping/seed/install counts and per-phase elapsed and CPU seconds for seeding, fetching, transfer, expansion/hydration, and Mathlib view preparation. CPU includes the preparator and reaped children. Phases can be nested, so their durations must not be added together. These measurements never control admission.
The pool defaults to ~/.cache/tauceti/builds under the login user's home. Configure
TAUCETI_BUILD_CACHE_ROOT before installing services to use another filesystem;
TAUCETI_SHARED_ARTIFACTS=0 disables expanded-artifact sharing. Explicit Mathlib/Lake
cache overrides are preserved. Only directories carrying a valid TauCeti ownership record
are collected; an arbitrary nonempty directory is never adopted or deleted.
The collector measures allocated bytes across shared and worker-private caches, counting
hard-linked inodes once. Its eviction target defaults to 25% of filesystem capacity;
TAUCETI_CACHE_MAX_GIB sets an explicit target instead. Pressure collection begins when
that target is exceeded or free space falls below 15%, and aims to restore 20% free space.
Entries use explicit last-reuse timestamps. Unused entries expire after 72 hours; abandoned
publication/download staging can be removed after four hours when its publisher lock is free.
After pool eviction, the collector can request private-store reclamation from one older worker
with substantial unused artifacts. This runs at an ordinary round boundary, keeps the current
build tree warm, and has a 12-hour per-worker cooldown. Live build artifacts are protected;
a target larger than the reclaimable data does not trigger a fleet-wide cache wipe.
Mathlib's own cache clean runs at most daily in the private archive store, removing stale links
for dependency trees no longer in use so those archives cannot be perpetually re-promoted.
Below 5% free space, new rounds enter waiting-storage, without consuming repair attempts
or escalating failure backoff. Existing rounds continue; admission resumes automatically above
15% free. The existing cleanup service is requested asynchronously under pressure, with a
five-minute request cooldown, in addition to its hourly schedule. No root, GitHub requests,
whole-fleet drain, or human-resume action is needed.
Cleanup and expanded-artifact metrics are prepared in activity data: managed and live-worker-held
bytes, remaining free space, observed net space recovered, cleanup errors, and latest per-worker
expanded/reused artifact counts and preparation time. status reads prepared data without
walking cache trees. Space held by active work, preserved source or unrelated programs cannot
be reclaimed to enforce an eviction target; this is not a filesystem quota. Retained source,
usage/accounting records and credentials are never disposable cache data.
add takes an optional id, defaulting to the next free workerN, and writes an
entry with enabled = true.
| Flag | Sets |
|---|---|
worker_id |
id; omit it for the next free workerN |
--agent AGENT |
agent |
--only TASKS |
only, as a comma-separated list |
--sandbox {host,bubble} |
sandbox |
--claude-billing {subscription,api} |
claude_billing |
--budget |
budget |
--anthropic-api-key-file PATH |
anthropic_api_key_file |
--ignore-quota |
ignore_quota; use with an explicit subscription agent |
--auto-refresh |
auto_refresh |
--roadmap-only AREA |
roadmap_only |
--roadmap-skip AREAS |
roadmap_skip, as a comma-separated list |
--extra-roadmap-prompt TEXT |
extra_roadmap_prompt |
--source PATH_OR_URL |
source; also requires roadmap in --only and a non-empty --roadmap-only |
--author-model MODEL |
author_model |
--author-effort EFFORT |
author_effort; Codex, Claude, or Kiro only |
--pace CURVE |
pace |
--stream |
stream |
--isolate-home |
isolate_home; useful when the id is default |
add cannot set roadmap_extra_identities, respect_claims, or restart, and
always writes enabled = true. Use workers edit for those.
| Action | What it does |
|---|---|
| (none) | Same as status |
status [--json] [--watch] |
Desired and actual state. Exits nonzero if the manager is offline or a wanted worker is not alive |
apply [--check] |
Validate the TOML schema and manager-level rules, then reconcile. --check validates only |
add [ID] [flags] |
Append an enabled definition and reconcile |
enable ID / disable ID |
Persist desired running or stopped state |
restart ID |
Request a restart without changing desired state; a disabled worker stays stopped |
remove ID |
Drop the definition and stop the worker |
logs ID [--follow] [--lines N] |
The durable console log. --follow continues across worker restarts |
tmux [--no-attach] |
Build the optional tmux viewing workspace |
manager [--interval N] |
Run the reconciler in the foreground |
manager-stop [--leave-workers] |
Stop the detached manager. By default it also stops its workers |
service ACTION |
install, uninstall, start, stop, restart, or status for the native user service |
edit [--editor CMD] |
Create or open workers.toml in an editor; it does not apply the result |
import LEGACY [--force] |
One-shot migration from the legacy workers.conf format; it does not start a manager |
apply without --check, add, enable, disable, remove, and restart
start a manager if none is running and return only after it accepts control
requests. edit, import, and apply --check do not start one.
workers apply and related actions start a detached manager owned by the current
login session. To move an existing fleet to a native user service that survives
logout and comes back after a reboot, leave its workers running while the service
takes over the manager socket:
tauceti workers manager-stop --leave-workers
tauceti workers service install
tauceti workers service statusOmit manager-stop when no detached manager is running. One runtime directory
can host only one manager and one active configuration at a time. A reconcile
action that names a different --config file reports the conflict instead of
switching it.
That is a systemd user service on Linux and NixOS, or a LaunchAgent on macOS. Two platform caveats:
- On Linux systems that stop the user manager after the last logout,
loginctl enable-linger "$USER"keeps user services running with no login session. - A macOS LaunchAgent survives terminal and SSH-session loss, but starts only after a graphical login. Installation says so explicitly when no GUI login domain is active.
At startup the worker preserves an explicit SSL_CERT_FILE or discovers the
host's system CA bundle, including NixOS's /etc/ssl/certs/ca-certificates.crt,
so quota checks keep working when uv's standalone Python defaults to a different
OpenSSL trust store. A shell-provided Nix bundle carried into the service stays
a revalidated candidate rather than a pinned trust path, so garbage collection
cannot silently disable fallback discovery.
The reconciler and the worker control sockets are portable Unix code. No Linux
/proc interface is required.
Workers targeting TauCetiProject/TauCeti use
https://github-state.taucetiproject.org for surveys and mirrored GitHub reads
without URL flags, token files, or per-worker configuration. The service publishes
read-only data for that public repository; GitHub writes still use the worker's
own authenticated account. Installation credentials remain on the server.
Explicit CLI and worker settings override the project configuration and default.
Use --github-state-url "", github_state_url = "", or project
services.github_state.mode = "off" to select direct reads. Without a project
manifest, TAUCETI_GITHUB_STATE_URL= also disables the default; project bootstrap
sets service environment bindings from the manifest. Downstream
projects retain their configured service and explicit mode = "off" policy;
other repositories are never implicitly sent to the Tau Ceti mirror. Custom and
private services still require their scoped client-token file. If a token file
is explicitly configured but unreadable, the client reports the configuration
failure rather than silently switching identities.
Unavailable mirror coverage or transport retains the existing direct fallback. Fresh dispatch checks and GitHub mutations keep their existing behavior.
Every worker id namespaces its state, checkout, review store, logs, and Bubble home. Workers coordinate through GitHub rather than sharing local mutable state, so several workers can use one host without sharing a checkout. A maintenance branch claim lives in the PR head repository, where the worker that can update the branch can also maintain its lease; roadmap and progress claims use the canonical repository by default. Review markers, claims, and compare-and-swap push and PR helpers keep workers from overwriting one another when they select the same target.
Every id other than default also enables credential isolation. On Linux and
other non-macOS hosts, the worker gets a private $HOME containing private
Claude and Codex credential copies. GitHub CLI and Git configuration remain
shared so the worker still acts as the operator's gh account. --isolate-home
applies the same isolation when the id is literally default.
The Lean build caches are handled outside that isolation, in two different ways, because they are written differently.
Toolchains are shared outright: $ELAN_HOME points at the login user's
~/.elan, so one install serves every worker and your own checkouts. Installing
a toolchain takes a per-toolchain lock and lands by rename, so workers racing for
the same one is safe. Left per-worker, 22 installs covered 6 distinct toolchains.
Mathlib's .ltar cache is not shared as a download target. lake exe cache get takes no lock, and in any checkout older than
leanprover-community/mathlib4#42752 it writes fixed-name
temporary files, so two workers downloading into one directory can leave a
corrupt .ltar under a name every later run trusts — including yours. Each
worker therefore downloads into its own $MATHLIB_CACHE_DIR under its state
directory, and before each round it exchanges finished files with the pool by
hardlink: it promotes what it fetched last round and takes a link to everything
the pool has that it lacks. A hardlink is atomic and an existing name is never
replaced, so the pool only ever gains complete artifacts, costs no extra disk,
and a worker downloads only what nobody on the machine has. Left per-worker
entirely, half of one week's 10.2 GB of .ltar traffic was a file another worker
already had.
$LAKE_CACHE_DIR stays per-worker too. It normally sits under the toolchain
directory, and would otherwise follow $ELAN_HOME into the pool, but unlike an
install it is written throughout every build. That keeps the default
LAKE_ARTIFACT_CACHE store private to the worker that fills it. Once canonical
main moves to a different lean-toolchain, the next host checkout preparation
clears this private store while no agent is
running. Switching between PR branches does not count as a bump and therefore
does not churn the cache.
Setting any of the three yourself overrides this. scripts/share-build-caches
folds the private copies an already-running fleet accumulated into the pool
without re-downloading them.
On macOS, $HOME stays unchanged because both Claude Code and GitHub CLI use the
login Keychain. tauceti redirects $CLAUDE_CONFIG_DIR and $CODEX_HOME, which
isolates Codex, but host workers still share the login user's Claude account.
Bubble rounds copy that shared Claude credential into a private transient
directory without modifying the Keychain. See the sandbox notes
for that handoff.
What an isolated worker inherits is the credential, not your configuration. Its
.claude directory gets a settings.json of its own, no CLAUDE.md, and only
the one pi skill the worker itself dispatches through, so a round behaves the
same whoever ran it and your personal instructions cannot contradict the task
prompt. Edit that generated settings.json in place to tune a worker; it is
written once and never overwritten. TAUCETI_INHERIT_CLAUDE_CONFIG=1 restores
the previous behaviour of sharing your own CLAUDE.md, settings, and skills,
including on a worker already seeded the clean way; a settings.json you have
edited is kept rather than replaced.
| Path | Contents |
|---|---|
<state>/<id>.json |
Per-worker status, heartbeated every two seconds |
<state>/manager.log |
The detached manager's own console |
<state>/logs/<id>/work-*.log |
Durable per-run console logs |
<runtime>/manager.sock, w-<id>.sock |
Control sockets, mode 0600 |
<state> is $TAUCETI_WORKERS_STATE_DIR, else $XDG_STATE_HOME/tauceti/workers,
else ~/Library/Application Support/tauceti/state/workers on macOS, else
~/.local/state/tauceti/workers. <runtime> is $TAUCETI_RUNTIME_DIR, else
$XDG_RUNTIME_DIR/tauceti, else /tmp/tauceti-$(id -u); it must be owned by you
and inaccessible to other users, or the manager refuses to start.
Each managed worker publishes a structured state such as waiting-quota,
surveying, running, or backoff, along with its current phase and target and
the path to its logfile. That is what tauceti workers status and the
dashboard's workers view read.
Work rounds read kernel resource counters at start and finish, with live refreshes once a
minute. Telemetry never scans the host process table. Live statistics appear under
resources in workers status --json; completed rounds append structured records to
logs/<worker-id>/resources.jsonl. Cumulative completed-round statistics live in
state/<worker-id>/resources.json and survive restarts.
Completed-round CPU includes the round and its reaped descendants, using getrusage().
A live value excludes unreaped children and has cpu_complete=false. Average CPU uses
elapsed wall time: 100% means one logical core. The worker average includes time between
rounds since recording began; the round average covers just that round.
max_process_rss_bytes is the kernel's single-process high-water reading, including
reaped children. New records do not report sampled process-tree RSS.
resources.worker_scope separately reports cumulative CPU, anonymous/file/kernel/charged
memory, scope-lifetime peak charged memory, task count (including threads), and optional
per-device I/O and stall counters. This scope includes the wrapper, loop, coding rounds,
and independent background verification. Its CPU must not be added to round CPU totals.
Charged memory and its peak include cache and kernel memory; they are not RSS, PSS, or an
exclusive share of shared Mathlib files. Missing counters remain unavailable, and workers
without a dedicated Linux scope retain round CPU accounting without scope measurements.
All cgroup access is read-only; unavailable telemetry does not delay work.
Reporting does not control whether useful work may continue. Status lock waits are bounded and unsent fields retry on a later update; a failed status write leaves the supervisor's identity available over its control socket and retries the pending fields on a later heartbeat. Unavailable log files fall back to console output. Optional GitHub identity caches, CLI instrumentation and endpoint metrics may also fail without rejecting an authenticated request. A temporary CLI launcher preserves quota handling when the normal launcher directory is unavailable, without moving retained publications. Under these failures, retained metrics can be incomplete and worker status marks degraded instrumentation.
A final cost-receipt write failure preserves the native agent's exit status and result. The accounting bridge still attempts settlement, while missing receipts retain their spending reservations until recovery. Actual funding admission and provider quota handling continue to apply independently of reporting.
tauceti workers tmux opens one dashboard window plus one log-following window
per enabled worker. Killing that session does not stop any worker, and running
the command again rebuilds the view from the configuration and the durable logs.
tmux is optional; workers run without it.
workers.conf is a legacy line-oriented format: one tauceti work --loop
command per line, each with an explicit --worker-id. It is only ever read by
the one-shot import, which refuses to overwrite an existing workers.toml
without --force:
tauceti workers import workers.confAnything the legacy parser does not recognize is an error naming the file, line, and token, so a partial migration is never silently accepted.
Bors retries an unchanged automatically reviewed bump after main advances, with three retries per head. This uses the existing Bors heartbeat and leaves the branch and its reviews intact. Workers do not request queue retries.
Bors durably hands a confirmed singleton failure to proof repair when no retry
is currently possible or its budget is exhausted, then publishes
bump-integration. Later main advances cannot retry that handed-off head.
The bump phase recognizes that status alongside a green standalone build. Before
spending on an editor, it checks the live exact-head PR and Bors bump_repairs
handoff. Pending or active queue work, withdrawals, draft/closed PRs and holds
are excluded. A second check after taking the normal branch claim closes the
selection gap. Failed observations decline the candidate and leave unrelated
work available. Automatic dependency bumps continue under the existing loop backoff and quota limits. The repair session fetches
and merges current main, diagnoses the actual integration failure, preserves
the dependency target and verifies its changes before pushing. Healthy surveys
make no additional API calls.
Claim collisions skip to other candidates without consuming a repair attempt. An idle mechanical recovery probe returns immediately to normal work selection. Only consecutive all-busy passes use a small capped retry pause; they never enter the general failed-round backoff.