[Intrafere]

MOTO v1.1.08: Kimi Code, Mathlib recovery, and CI fixes

Bug fixes

Lean / Mathlib

• Mathlib setup never recovered after an interrupted update (for example
  when the disk filled up): every retry and restart failed with "would be
  overwritten by checkout". Setup now resets half-written package
  checkouts to their recorded commit (wiping .lake if that fails), and
  the same repair runs on the mid-run retry, so no restart is needed.
• Every backend start ran lake update, moving Mathlib to the newest
  version and downloading a new cache each time. Mathlib is now installed
  once and kept at its recorded version.
• Old Mathlib downloads were never deleted. Downloads now go to a
  MOTO-owned .moto_mathlib_cache, and archives the installed version does
  not use are pruned after each setup. The shared ~/.cache/mathlib is
  left alone because other Lean projects may use it.
• An import of a renamed or removed Mathlib module was treated as a
  broken workspace, so MOTO wiped Mathlib and stopped the run for repair.
  It is now proof feedback for the model.
• Wiping .lake blocked the backend event loop; it now runs off-thread.

Proof workflows

• A reply cut off at the output-token limit had its unfinished thinking
  used as the answer (in retries and Supercharge). It is now treated as
  empty.
• One very long Lean diagnostic could overflow proof prompts. Each
  attempt's Lean output (30k chars) and goal states (10k) are now bounded
  in prompts; stored feedback keeps everything.
• One candidate that overflowed the context stopped the whole round or
  Autonomous run, and ended manual pruning loops. That candidate is now
  set aside as a failed open target while the others continue; only a
  round where no candidate can reach the model stops.
• Manual checks of Autonomous sources were treated as the Autonomous
  workflow for that stop. They no longer are.
• Saved Lean timeouts of 600/900 s and an SMT timeout of 30 s were reset
  to defaults on every load. Proof settings are now versioned, so chosen
  values are kept.

Providers and settings

• Sakana Fugu and xAI model-load errors were never shown in the settings
  panels; every panel now shows a banner per provider.
• The Sakana reasoning-effort control kept unsupported values and stayed
  editable during a run in Aggregator/Compiler. It is now normalized per
  provider and locked while running.
• The OpenRouter/OAuth modal offered and polled providers the backend
  reported unavailable. It no longer does.
• The startup add-on card ignored Sakana. It is now also hidden in hosted
  mode.
• A failed provider status check kept the old "configured" state with
  the wrong message.
• Provider notifications fell back to "OAuth provider" instead of the
  provider's name.
• The legacy SAKANA_API_KEY / FUGU_API_KEY variables overrode
  MOTO_SAKANA_FUGU_API_KEY. The MOTO_ variable now wins.
• A keyring failure while saving an API key escaped the route unhandled.
  It now returns a clean error and keeps the previous key.
• One malformed entry broke the whole Sakana model list, and models MOTO
  did not already know had no context/output limits.
• The xAI Grok client was not closed at backend shutdown.

CI

• The SyntheticLib release-evidence workflow failed on every main push
  since v1.1.08: it installs only pytest, and tests/conftest.py imported
  pydantic at startup. It also ran only after merging, so the failure was
  first seen on main. The conftest guards now stand down when MOTO's
  dependencies are missing, the workflow also runs on pull requests and
  dev/** pushes, a test fails if any workflow loses those triggers, and
  npm run test:github runs these tests with only pytest installed.
• The frontend npm audit failed whenever npm's advisory service did not
  answer, because npm exits 1 for that just as for a vulnerability. The
  audit now retries only a failed advisory request, and still fails at
  once on high/critical findings or any other npm error.
• The README said the launcher runs npm audit fix. It runs a read-only
  audit and warns.

New

• Kimi Code subscription provider: membership API key, region detected
  on save, low/high/max reasoning, usage windows and a quota display.
• Cloud providers are driven by one registry (backend metadata mirrored
  in the frontend). Sakana Fugu moves onto the shared API-key client,
  and "max" reasoning is allowed for any provider that supports it.
• API keys are scrubbed from provider error text, and requests send a
  MOTO-Autonomous-ASI User-Agent.
• npm run test:codeql and npm run test:github run every GitHub check
  locally; a CI job fails dev pushes that add CodeQL alerts main lacks.
• API contract build6-v122: /api/features adds kimi_code_available
  and subscription_providers, plus the subscription_provider_error event.