diff --git a/.cursor/rules/api-key-controls.mdc b/.cursor/rules/api-key-controls.mdc index cfc4e8a..0862b80 100644 --- a/.cursor/rules/api-key-controls.mdc +++ b/.cursor/rules/api-key-controls.mdc @@ -12,9 +12,10 @@ Enables cloud provider access with LM Studio fallback in default mode (OpenRoute **Key Features:** - **Per-Role Cloud Provider Selection**: Each role independently uses LM Studio, OpenRouter, or a desktop-only OAuth/subscription provider where available (OpenAI Codex OAuth, xAI Grok OAuth, Sakana Fugu API key; default mode); generic mode remains OpenRouter-only. - **OpenRouter/OAuth**: Header overlay manages OpenRouter API keys and desktop OAuth/provider logins (OpenAI Codex, xAI Grok/SuperGrok OAuth, Sakana Fugu subscription API key). The post-disclaimer startup wizard requires OpenRouter or LM Studio first and presents OAuth/provider add-ons later. The provider UI is registry-driven (`openai_codex_oauth`, `xai_grok_oauth`, `sakana_fugu`) so future providers can be added without changing saved profile shape. OAuth attribution identifiers must refer to MOTO Autonomous ASI, never the bare nickname `moto`; compact OAuth identifier fields use `moto-autonomous-asi` unless a provider explicitly requires the full display name. +- **Credential State Refresh**: Adding/removing OpenRouter keys or desktop OAuth/subscription credentials must immediately invalidate mounted settings panels so provider buttons and model lists refresh without tab navigation. Credential presence and model-list loading are distinct: a valid OpenRouter key stays enabled if `/models` transiently fails; failed OAuth/subscription model loads clear stale model lists and show provider-specific errors. - **SyntheticLib4 Access**: SyntheticLib4 backend/search scaffolding remains in place, but the user-facing connectivity pill is currently a `Coming soon` explainer rather than a ready/configuration surface. The modal explains the reciprocal proof-contribution/access model until production corpus access is enabled. - **Session History Memory**: The connectivity toggle defaults enabled for new users and maps to local MOTO/manual/LeanOJ proof-history memory used by Assistant workflow-memory search during brainstorming, writing, proof work, and LeanOJ solving. It is not raw provider transcript or chain-of-thought storage. Disabling it persists as non-secret runtime state, removes local proof-history corpora from Assistant retrieval, and must not delete proof records or alter internal retry/rejection/prompt memory. -- **Assistant Role**: Aggregator, Compiler, Autonomous Research, and LeanOJ expose one shared non-blocking Assistant LLM role per workflow surface for verified proof-memory support. Assistant selects up to 7 prior verified proof supports, never replaces validators or submitters, never blocks parent workflows, and is disabled when Session History Memory is disabled. Useful Assistant packs may be reused by two eligible receiver reads before the next refresh. True no-history targets are skipped because Assistant only performs proof-memory retrieval for now. Durable cooldown groups transient task IDs/roles by workflow run while preserving real source/session separation: repeated zero-useful retrieval backs off and may shut down for the run; repeated stagnant same-pack retrieval backs off without shutdown. Stale live packs/state clear only on explicit reset/clear or Session History Memory disable. User live activity should show normal Assistant retrieval result logs only, not skip/backoff/shutdown turns. +- **Assistant Role**: Aggregator, Compiler, Autonomous Research, and LeanOJ expose one shared non-blocking Assistant LLM role per workflow surface for verified proof-memory support. Assistant selects up to 7 prior verified proof supports, never replaces validators or submitters, never blocks parent workflows, and is disabled when Session History Memory is disabled. Useful Assistant packs may be reused by two eligible receiver reads before the next refresh. True no-history targets are skipped because Assistant only performs proof-memory retrieval for now. Durable cooldown groups transient task IDs/roles by workflow run while preserving real source/session separation: repeated zero-useful retrieval backs off and may shut down for the run; repeated stagnant same-pack retrieval backs off without shutdown. Stale live packs/state clear only on explicit reset/clear or Session History Memory disable. User live activity should show normal Assistant retrieval result logs and explicit Assistant model-output failures, not skip/backoff/shutdown turns. - **Startup provider requirement**: OAuth providers are supplementary role providers, not a standalone startup path, because RAG embeddings route through LM Studio, OpenRouter, or generic-mode FastEmbed. First-run startup and workflow start preflights must require OpenRouter, generic FastEmbed, or LM Studio with an embedding model available before OAuth-only role selection is allowed. - **OpenRouter Auto-Fill**: OpenRouter selectors fetch provider endpoint metadata and compute host-aware context/output settings from a capable endpoint set. Auto mode ignores known weak hosts (currently Venice) and low/missing-cap outliers before computing context/max-output; manual host selection uses that exact host and its largest exposed endpoint output cap. - **OAuth Auto-Fill**: OAuth model selectors auto-fill only from provider model metadata, documented provider-specific limits, or curated provider-backed public aliases. Do not invent generic fallback context windows for unknown OAuth models; preserve current settings when metadata is unknown. GPT-5.5 Codex uses the Codex 400K product window, not the 1M regular API window; Codex Spark high is exposed as a curated alias for Codex Spark with high reasoning and its documented 128K window. Grok/SuperGrok OAuth uses xAI model metadata when available and may expose known Grok subscription limits only for known model IDs; model listings must filter xAI catalog entries that are not accepted by the OAuth chat-completions route, such as multi-agent-only models. @@ -105,7 +106,7 @@ Enables cloud provider access with LM Studio fallback in default mode (OpenRoute - This includes: aggregator submitters/validator/Assistant, compiler Writing/Rigor & Proofs/validator/Assistant, autonomous agents/Assistant, Tier 3 final answer agents, and LeanOJ roles/topic/brainstorm submitters/Assistant - Role configs must preserve `supercharge_enabled` when copied into proof snapshots, manual proof helpers, child Aggregator/Compiler coordinators, and LeanOJ grouped roles. - **Proof agents (Part 3/manual, optional)** use the visible Rigor & Proofs Submitter settings for proof-solving submitter work. Internal proof role IDs are still configured through `api_client_manager.configure_role()` by copying from the `ProofRuntimeConfigSnapshot` (Rigor & Proofs submitter, validator, optional Assistant) captured by `autonomous_coordinator._build_proof_runtime_config_snapshot()` and persisted via `research_metadata.set_proof_runtime_config()`, or supplied directly on manual `POST /api/proofs/check`. Manual checks require `lean4_enabled=True` and either a stored or request-provided runtime snapshot. -- Assistant is the preferred owner of routine proof-history memory retrieval for eligible non-validator, non-critique flows. It watches the current prompt/phase/target, searches proactively against verified proof corpora, ranks a diverse up-to-7 memory-support pack with cached target/goal reuse and visit-count exploration, reuses useful packs for two eligible receiver reads before refresh, and never blocks the parent workflow. Run-scoped cooldown prevents repeated empty/stagnant retrieval from calling Assistant every turn; ordinary stop preserves that state, while explicit clear/reset removes it. In-role `search_lean_proofs` calls should be explicit legacy/debug or narrow emergency-repair paths only, not the normal retrieval path. +- Assistant is the preferred owner of routine proof-history memory retrieval for eligible non-validator, non-critique flows. Assistant proof-memory injection is centralized in `APIClientManager`, optional, budget-bounded, excluded from validators/Assistant-like roles, and consumed only by eligible receiver calls. It watches the current prompt/phase/target, searches proactively against verified proof corpora, ranks a diverse up-to-7 memory-support pack with cached target/goal reuse and visit-count exploration, reuses useful packs for two eligible receiver reads before refresh, and never blocks the parent workflow. Run-scoped cooldown prevents repeated empty/stagnant retrieval from calling Assistant every turn; ordinary stop preserves that state, while explicit clear/reset removes it. In-role `search_lean_proofs` calls should be explicit legacy/debug or narrow emergency-repair paths only, not the normal retrieval path. **Boost Mode Priority** (`should_use_boost(task_id)`): 1. Always Prefer Boost: `boost_always_prefer=True` → True @@ -247,7 +248,9 @@ Workflow, boost, fallback/reset, provider pause/resume, hung-connection, rate-li **Credit Exhaustion:** HTTP 402 or keywords "credit"/"insufficient"/"balance"/"quota"/"key limit"/"limit exceeded" → `CreditExhaustionError` → default mode: LM Studio fallback for that role when configured; proof workflows with no fallback checkpoint progress and pause, while currently waiting tasks can be woken by `POST /api/openrouter/reset-exhaustion`; ordinary non-proof generic-mode calls still raise provider/config errors when no fallback exists. Fallback state is resettable via `POST /api/openrouter/reset-exhaustion` or by re-setting the API key. -**OAuth provider transient failures:** gateway/timeout/stream disconnect responses use bounded exponential backoff (4 retries) where the provider adapter supports it and must preserve proof checkpoints instead of becoming hard "no fallback configured" stops, `no_candidates`, or proof-attempt exhaustion. Auth/config failures remain hard; when an OAuth model call cannot recover through LM Studio fallback, broadcast a user-visible OAuth reconnect notification with a stable provider/role/reason/model `notification_key` so user-dismissed alerts do not replay after restart. +**Retryable provider failures:** transient gateway/timeout/stream disconnect responses use provider-adapter retries first, then raise the shared `RetryableProviderError` so workflow loops use one exponential backoff path and preserve checkpoints instead of becoming rejects, `no_candidates`, or stops. Auth/config failures remain hard; when an OAuth model call cannot recover through LM Studio fallback, broadcast a user-visible OAuth reconnect notification with a stable provider/role/reason/model `notification_key` so user-dismissed alerts do not replay after restart. + +**Provider Context Limits:** OAuth/provider `context_length_exceeded` / context-window rejections are hard context mismatch failures, not retryable OAuth errors. Try the configured LM Studio fallback once when present; otherwise raise the workflow's context-overflow path and emit that preset live activity notification instead of repeatedly broadcasting OAuth failure events. **OAuth provider usage limits:** Codex `usage_limit_reached` responses carry `resets_at`/`resets_in_seconds`; `APIClientManager` tracks in-memory provider cooldown, emits one durable `oauth_provider_usage_limited` notification per cooldown window, uses LM Studio fallback when configured, otherwise raises `OAuthProviderCooldownError` so submitter/validator loops wait until reset instead of retry-spamming. Assistant OAuth refreshes reuse the latest cached/deterministic shortlist during cooldown instead of making new OAuth selection calls. diff --git a/.cursor/rules/hosted-web-contract.mdc b/.cursor/rules/hosted-web-contract.mdc index d443880..e7834b5 100644 --- a/.cursor/rules/hosted-web-contract.mdc +++ b/.cursor/rules/hosted-web-contract.mdc @@ -9,7 +9,7 @@ MOTO is ONE codebase serving TWO deployment targets. A single `generic_mode` boo ## Two Deployment Targets -- **Default mode (`generic_mode=False`)**: GitHub open-source release. Desktop app with `.bat` / PowerShell launchers. LM Studio + OpenRouter + desktop OAuth providers such as OpenAI Codex and xAI Grok. User runs locally. +- **Default mode (`generic_mode=False`)**: GitHub open-source release. Desktop app with `.bat` / PowerShell launchers. LM Studio + OpenRouter + desktop provider add-ons such as OpenAI Codex OAuth, xAI Grok OAuth, and Sakana Fugu API key. User runs locally. - **Generic mode (`generic_mode=True`)**: Hosted web backend. API-only sandbox on Blaxel, fronted by the Intrafere website/control plane on AWS. FastEmbed embeddings and OpenRouter-only LLM inference; hosted clients should not use LM Studio diagnostics even if legacy endpoints still exist for the shared route surface. ## Two-Team Boundary (Strict) @@ -97,7 +97,7 @@ Build 0 lands the public identity subset first. Returns: The current Build 5 runtime preserves the four identity fields while exposing the stable capability flags above. `proof_downshifted` is a proof workflow event for Lean-accepted proofs preserved under a narrower actual theorem statement, not a `/api/features` field. Later hosted work may extend `/api/features` with additional capability flags such as `max_submitters` and `tier3_available`, but the existing fields above remain stable and `api_contract_version` must bump when that happens. -Current Build 5 contract notes: v53 includes desktop-only Sakana Fugu direct subscription API access (`sakana_fugu_available`, `/api/cloud-access/sakana-fugu/*`, Responses-first generation with chat-completions fallback, and `sakana_fugu_error` notifications), Codex OAuth `usage_limit_reached` cooldown metadata/notifications, and Assistant proof-pack OAuth-cooldown selection modes (`cached_oauth_cooldown`, `deterministic_oauth_cooldown`). v52 includes durable internal Assistant proof-memory cooldown/shutdown/no-history WebSocket events (`assistant_proof_memory_unavailable`, `assistant_proof_memory_cooldown`, `assistant_proof_memory_shutdown`), but user live activity should display only normal Assistant retrieval result logs such as `assistant_proof_pack_updated`. +Current Build 5 contract notes: v54 includes `assistant_proof_pack_failed` for Assistant proof-memory model-output/selection failures, which should display as live activity errors instead of successful empty proof-pack updates. Autonomous proof provider pauses with `reason="openrouter_credit_exhaustion"` remain credit-reset prompts; `reason="transient_provider_error"` is an automatic retry pause, not a credit notification. v53 includes desktop-only Sakana Fugu direct subscription API access (`sakana_fugu_available`, `/api/cloud-access/sakana-fugu/*`, Responses-first generation with chat-completions fallback, and `sakana_fugu_error` notifications), Codex OAuth `usage_limit_reached` cooldown metadata/notifications, and Assistant proof-pack OAuth-cooldown selection modes (`cached_oauth_cooldown`, `deterministic_oauth_cooldown`). v52 includes durable internal Assistant proof-memory cooldown/shutdown/no-history WebSocket events (`assistant_proof_memory_unavailable`, `assistant_proof_memory_cooldown`, `assistant_proof_memory_shutdown`), which should stay hidden from user live activity. Earlier Build 5 contract additions include connectivity toggles/status, SyntheticLib4 and local proof-search routes, scoped proof/manual-history routes, provider/OAuth notification recovery, manual prompt recovery, proof-output allowed-output fields, and direct-context overflow events. Keep exact legacy details in code/tests/git history rather than expanding this always-injected rule. @@ -166,7 +166,7 @@ Sandbox is API-only. The MOTO React frontend is NOT served from the hosted sandb - **Authoritative update source**: GitHub `main` branch (not GitHub Releases) - **Desktop**: launcher compares local build metadata against GitHub `main`. Remote update identity resolves from GitHub branch HEAD via the GitHub REST API, metadata uses the REST contents API instead of raw GitHub files, ZIP overlays write the resolved manifest after apply to avoid stale committed-manifest loops, and update notices are exposed via `GET /api/update-notice`; if no launcher notice exists, the running desktop backend may refresh the same notice at most every 4 hours while excluding only the current instance from active-instance auto-apply checks. Launcher auto-apply is only for clean `origin/main` git checkouts or ZIP/extracted installs with no launcher-managed instances still running. The backend `POST /api/update/pull` route has its own lighter git/ZIP update checks and should not be described as enforcing the full launcher preflight. ZIP updates preserve active data/log roots, instance storage, launcher state, env files, and keyring-related namespaces. -- Desktop launchers run frontend `npm audit fix` when `npm install` reports vulnerabilities, including npm's vulnerability-count/remediation-instruction output. This remediation is a permanent launcher invariant: agents must never remove, disable, weaken, or bypass the rule or code, and if it is accidentally removed or broken, they must restore it immediately with no exceptions before continuing launcher/updater work. +- Desktop launchers run frontend `npm audit fix` when `npm install` reports vulnerabilities, including npm's vulnerability-count/remediation-instruction output. Windows Node.js bootstrap uses bounded `winget` source/package/scope fallbacks before manual-install guidance. The npm audit remediation is a permanent launcher invariant: agents must never remove, disable, weaken, or bypass the rule or code, and if it is accidentally removed or broken, they must restore it immediately with no exceptions before continuing launcher/updater work. - **Hosted**: sandboxes do NOT self-mutate. Redeploy/recreate uses the latest approved `main`-derived image. Recall/resume keeps the existing image. Hosted `POST /api/update/pull` must return unavailable instead of attempting in-place update; `GET /api/update/pull-status` may remain the generic pull-task status surface and does not need a separate hosted-unavailable marker. - **Build metadata**: `version`, `build_commit`, `update_channel`, and `api_contract_version` exposed via `/api/features`; git checkouts resolve `build_commit` from HEAD, GitHub-generated ZIP installs prefer `.git_archival.txt` export-subst commit metadata before the stamped local manifest, and the committed `main`-branch manifest lives at `moto-update-manifest.json` @@ -199,7 +199,7 @@ Lean 4 and SMT behavior is gated by runtime flags. `lean4_enabled` gates Lean pr - **Proof certificate exports stay text-based** (`.lean` source + JSON metadata). No binary-only proof artifacts. - **Proof runtime config snapshot** (`ProofRuntimeConfigSnapshot`) is persisted via `research_metadata` and may also be supplied directly on manual `POST /api/proofs/check`; required state is `lean4_enabled=True` AND either a stored or request-provided snapshot. - **SyntheticLib4 / MOTO proof search** is additive proof-history/corpus navigation. The shared `search_lean_proofs` tool adapter returns bounded retrieved proof context and provenance; it must not bypass MOTO's proof registration, Lean/integrity gates for MOTO-generated artifacts, or existing proof-runtime disablement in hosted generic mode. -- **Assistant memory-support role** is an additive workflow/settings surface. It is one shared non-blocking LLM role per workflow surface, not a per-lane submitter clone; validators never receive Assistant context and parent workflows never wait for it. Assistant may provide up to 7 verified proof supports, reuse useful packs for two eligible receiver reads before refresh, and skip true no-external-history targets with `assistant_proof_memory_unavailable` because it only performs proof-memory retrieval for now. Durable cooldown is keyed to stable run scope, grouping transient task IDs/roles while keeping real source/session IDs separate; it emits internal `assistant_proof_memory_cooldown` during zero-useful or stagnant backoff and internal `assistant_proof_memory_shutdown` only when repeated zero-useful retrieval disables retrieval for the run scope. Stagnant same-pack retrieval must not shut down. User live activity should not show skip/backoff/shutdown turns; show only normal Assistant retrieval result summaries. Session History Memory disabled disables Assistant and prevents stale pack injection. REST/WebSocket/profile schema additions for Assistant require this contract, `/openapi.json`, and `api_contract_version` to update in the same merge. +- **Assistant memory-support role** is an additive workflow/settings surface. It is one shared non-blocking LLM role per workflow surface, not a per-lane submitter clone; validators never receive Assistant context and parent workflows never wait for it. Assistant may provide up to 7 verified proof supports, reuse useful packs for two eligible receiver reads before refresh, and skip true no-external-history targets with `assistant_proof_memory_unavailable` because it only performs proof-memory retrieval for now. Durable cooldown is keyed to stable run scope, grouping transient task IDs/roles while keeping real source/session IDs separate; it emits internal `assistant_proof_memory_cooldown` during zero-useful or stagnant backoff and internal `assistant_proof_memory_shutdown` only when repeated zero-useful retrieval disables retrieval for the run scope. Stagnant same-pack retrieval must not shut down. User live activity should not show skip/backoff/shutdown turns; show normal Assistant retrieval summaries and explicit Assistant model-output failures. Session History Memory disabled disables Assistant and prevents stale pack injection. REST/WebSocket/profile schema additions for Assistant require this contract, `/openapi.json`, and `api_contract_version` to update in the same merge. - **`api_contract_version` bumps** apply the same way to proof additions as to the base contract: any new proof route or event added after Build 5 must bump the contract version in the same merge. ## Hosting Ownership diff --git a/.cursor/rules/json-prompt-design.mdc b/.cursor/rules/json-prompt-design.mdc index c03be3c..c19d090 100644 --- a/.cursor/rules/json-prompt-design.mdc +++ b/.cursor/rules/json-prompt-design.mdc @@ -166,7 +166,7 @@ CORRECT RESPONSE: - Maintain existing prompt assembly order: System → JSON Schema → User Prompt → Context → RAG → Final Instruction - **MATH VARIANT**: Mathematical theorem/exposition validation focuses on rigor, logical correctness, and established mathematical principles rather than mandatory citation format. Empirical, artifact, and literature claims still require explicit support/citations or conservative wording where compiler validators enforce claim provenance. Models with web search capabilities are encouraged to use them for verification. - **Proof Candidate JSON Contract**: Automated proof identification is impact-first, not a known-knowledge-base builder. Candidate JSON must use `{"has_provable_theorems": bool, "theorems": [{"theorem_id": str, "statement": str, "formal_sketch": str, "expected_novelty_tier": "major_mathematical_discovery|mathematical_discovery|novel_variant|novel_formulation", "prompt_relevance_rationale": str, "novelty_rationale": str, "why_not_standard_known_result": str}]}`. Every automated proof JSON prompt must treat the USER RESEARCH PROMPT as the primary filter; bounded source-title/brainstorm-topic metadata is context only. Order candidates by direct impact on the user's prompt: direct solutions or impossibility results first, then decisive reductions, obstructions, and structural theorems that themselves make major progress. The three rationale fields must be non-empty or the candidate is skipped before Lean cost. Reject supporting lemmas, routine helpers, standard/textbook/Mathlib restatements, program-local firsts, minor reformulations/local formalizations, trivial/easy proofs, single-tactic/routine proof goals, and general verified background-library entries. Never impose an artificial theorem-count cap unless explicitly requested; user-configurable proof concurrency batching limits simultaneous attempts only and must not truncate identified candidates. -- **Assistant Proof-Support Pack Contract**: Assistant is a separate shared non-blocking proof-support role for the active workflow, not a per-submitter role, proof candidate identifier, or validator. Assistant prompt/output schemas should keep the final model-visible pack capped at 7 fully Lean-verified proof supports by default, each with source/provenance, theorem statement/name, relevance/transfer reason, dependencies/imports, code/hash metadata, and target/freshness metadata. Useful packs are reused for two eligible receiver reads before refresh. Assistant skips true no-external-history targets because it only performs proof-memory retrieval for now. Durable run-scoped cooldown backs off repeated zero-useful retrieval and may shut off Assistant for that run; repeated stagnant same-pack retrieval backs off without shutdown. User live activity should show normal Assistant retrieval result summaries only, not skip/backoff/shutdown turns. Assistant may use current solver feedback/rejections/Lean errors as query material, but outputs must state when support is stale/cached and must not broaden proof-candidate eligibility beyond the user's prompt. Partial/failed artifacts are excluded from the final support pack unless a future explicit obstruction-debug mode says otherwise. +- **Assistant Proof-Support Pack Contract**: Assistant is a separate shared non-blocking proof-support role for the active workflow, not a per-submitter role, proof candidate identifier, or validator. Assistant prompt/output schemas should keep the final model-visible pack capped at 7 fully Lean-verified proof supports by default, each with source/provenance, theorem statement/name, relevance/transfer reason, dependencies/imports, code/hash metadata, and target/freshness metadata. Useful packs are reused for two eligible receiver reads before refresh. Assistant skips true no-external-history targets because it only performs proof-memory retrieval for now. Durable run-scoped cooldown backs off repeated zero-useful retrieval and may shut off Assistant for that run; repeated stagnant same-pack retrieval backs off without shutdown. User live activity should show normal Assistant retrieval result summaries and explicit Assistant model-output failures, not skip/backoff/shutdown turns. Assistant may use current solver feedback/rejections/Lean errors as query material, but outputs must state when support is stale/cached; receivers must independently judge relevance and may ignore any support. Assistant support must not broaden proof-candidate eligibility beyond the user's prompt. Partial/failed artifacts are excluded from the final support pack unless a future explicit obstruction-debug mode says otherwise. - **Optional `lean_proof` Submission Contract**: Aggregator and LeanOJ brainstorm submitters that choose `submission_type="lean_proof"` should include the same novelty fields (`expected_novelty_tier`, `prompt_relevance_rationale`, `novelty_rationale`, `why_not_standard_known_result`) as ranking context. Submitter-side novelty means public/citable prompt-relevant novelty absent from standard references or Mathlib; program-local firsts do not qualify. The shared Lean proof gate rejects missing/invalid novelty tiers and missing prompt-relevance/novelty/anti-standard-result rationales before Lean cost, in addition to malformed submissions, failed Lean attempts, placeholders, and fake proof devices. Once Lean accepts real proof code, preserve/register the artifact and let novelty/triviality ranking decide context retention, even for not-novel or downshifted actual-theorem artifacts. This preservation rule is not permission to target supporting lemmas. Normal Aggregator validation may reject Lean-verified proof artifacts from the accepted-submission database when the actual theorem is low-impact, trivial, routine, or redundant. LeanOJ brainstorm flow is template-solution-specific: proof-gated `lean_proof` artifacts may be accepted only when useful for exact template obligations. LeanOJ final master-proof editing is template-solution-first and may use standard facts inline when they directly solve current obligations, but it must not accumulate a general known-knowledge library in `master_proof.lean`. - **Compiler Outline Injection**: The compiler outline is always fully injected (never truncated, never RAGed) for all modes because it provides the structural framework for document construction and validation. - **TEMPERATURE POLICY**: Default all prompts to `temperature=0.0`. Only two exceptions are allowed: Supercharge candidate attempts and parallel brainstorm submitter lanes. Validators, compiler roles, proof/final roles, and JSON retries must stay deterministic. diff --git a/.cursor/rules/main-rule-3-code-interaction-and-rule-interaction-rules.mdc b/.cursor/rules/main-rule-3-code-interaction-and-rule-interaction-rules.mdc index 366747d..45ec9f9 100644 --- a/.cursor/rules/main-rule-3-code-interaction-and-rule-interaction-rules.mdc +++ b/.cursor/rules/main-rule-3-code-interaction-and-rule-interaction-rules.mdc @@ -31,6 +31,7 @@ alwaysApply: true 10.) LeanOJ initial topic generation and brainstorm submitters always run in parallel and feed one validator that batch-validates up to 3 topics/submissions. Initial topic candidates/selection must be broad locked foundation questions covering the whole LeanOJ solution route, not narrow sublemma/tactic/local-repair topics. Recursive brainstorming has no separate recursive-topic prepass and must not re-inject the initial selected topic as active steering context; it uses the shared accepted proof-memory database plus the current proof/failure context. Accepted brainstorm memory must preserve occurrence-specific chronological metadata even for duplicate idea text. Never implement active LeanOJ topic or brainstorm phases as round-robin/serial submitter calls; one hung submitter must not halt the phase. 10b.) Developer-enabled LeanOJ Creativity Emphasis Boost applies to every fifth valid queued initial-topic and brainstorm submission per submitter. It only adds optional near-solution/adjacent-solution creativity pressure when apparent and potentially very helpful; validation remains unchanged, accepted/rejected WebSocket payloads mark `creativity_emphasized`, and the block is skipped for that slot if it would overflow the configured prompt budget. +10c.) LeanOJ brainstorm memory prune review is conservative and may apply at most one remove/update/add operation only when it improves exact-template proof-solving context. 11.) LeanOJ stop/crash/restart preserves resumable state by default. `Clear Progress` / `/api/leanoj/clear?confirm=true` is the only intentional reset path. Start/restart should choose the best matching/resumable persisted session by proof context, not blindly create a new session or pick the latest file; automatic model-work restart on backend boot is opt-in via runtime config. @@ -43,3 +44,5 @@ alwaysApply: true 15.) Parent/user-selected phases have hierarchy precedence over child branches. When a parent phase starts (LeanOJ forced final loop, autonomous paper writing, Tier 3 final answer/final selection), lower-tier brainstorm/topic/path child tasks must stop or be ignored. LeanOJ `Skip Brainstorm` locks the run into the final loop until the configured final-attempt cycle is exhausted; model/path requests for more brainstorming cannot override that user action early. `Force Brainstorm` is a separate explicit user override that returns to recursive brainstorming while preserving proof progress. 16.) LeanOJ prompt flows must guard formal/informal mismatches: treat the Lean template as the formal source of truth, do not silently reinterpret operations such as `Nat` subtraction, sanity-check exact-template formulas on small cases when feasible, and never claim Lean acceptance alone proves the informal problem unless that correspondence is justified. + +17.) LeanOJ final answers must give an explicit formula/value when the template asks for one; supremum-style encodings of the feasible set are intermediate progress, not final readiness. diff --git a/.cursor/rules/part-1-aggregator-tool-design-specifications.mdc b/.cursor/rules/part-1-aggregator-tool-design-specifications.mdc index 8c2ac53..16657fe 100644 --- a/.cursor/rules/part-1-aggregator-tool-design-specifications.mdc +++ b/.cursor/rules/part-1-aggregator-tool-design-specifications.mdc @@ -65,7 +65,7 @@ All Aggregator offload order and source-exclusion rules are centralized in `rag- ## Role Selection -User selects model per role. Multiple roles can share a model. Models load with user-set context sizes. Aggregator settings also expose one shared `aggregator_assistant` memory-search LLM role for optional verified proof-memory support; built-in/default profiles set Assistant equal to the primary Validator, and Session History Memory disabled greys Assistant out. Assistant may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, uses run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns from live activity, and never injects into validator prompts. +User selects model per role. Multiple roles can share a model. Models load with user-set context sizes. Aggregator settings also expose one shared `aggregator_assistant` memory-search LLM role for optional verified proof-memory support; built-in/default profiles set Assistant equal to the primary Validator, and Session History Memory disabled greys Assistant out. Assistant may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, uses run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns while showing Assistant model-output failures in live activity, and never injects into validator prompts. Per-role Supercharge is optional. When enabled for a submitter or validator, `api_client_manager.generate_completion()` runs 4 parallel full answer attempts for that role call, then a 5th same-model synthesis call and returns only the synthesis result. Supercharge candidate attempts intentionally use temperatures `[0.0, 0.2, 0.4, 0.8]` to diversify parallel outputs; synthesis remains `0.0`. Candidate attempts are sanitized to reusable visible answer text before synthesis; private thought/channel/control transcript text must never be fed back as feedback, brainstorm memory, or synthesis context. The synthesis prompt frames candidates as optional working material: the model may use one, combine several, ignore all, or write a stronger new answer, while preserving the original role output contract. If Boost applies to that role/task, all internal Supercharge calls use the Boost config first. Tool-call requests bypass Supercharge. @@ -123,4 +123,4 @@ JSON validation failure: reject submission, send reason + content to submitter's When `lean4_enabled`, submitters may use `submission_type="lean_proof"` only for high-impact prompt-directed proof candidates whose claimed novelty is public/citable and absent from standard references or Mathlib, not merely new to the program. The shared Lean proof gate rejects missing/invalid novelty tiers and missing prompt-relevance/novelty/anti-standard-result rationales before Lean cost. Supporting lemmas, routine helpers, local facts, trivial/easy proofs, and weakened substitutes are not valid targets. Once Lean accepts real proof code, preserve/register the actual artifact for novelty/triviality ranking, but normal brainstorm validation may still reject it from the accepted-submission database when the actual theorem is low-impact, trivial, routine, or redundant. Hard rejection always applies to non-Lean-verified attempts, malformed submissions, or fake proof devices such as new `axiom`/`constant`/`opaque` declarations. -Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It uses standard proof discovery, asking for candidates that directly solve the user prompt first and then candidates that substantially build toward solving it. When Session History Memory is enabled, the separate Assistant LLM role runs in parallel during brainstorming and proof checks, maintaining a freshness-tagged up-to-7 pack of fully Lean-verified local/SyntheticLib4 memory supports for eligible submitter/proof roles; proof discovery/formalization may use the latest pack but must not wait for it, and useful packs refresh only after two eligible receiver reads. Assistant cooldown state is run-scoped across transient task IDs/roles, survives ordinary stop/restart for that same run scope, is cleared only by explicit workflow/session reset, and hides skip/backoff/shutdown turns from live activity; zero-useful retrieval can shut down for the run, while stagnant same-pack retrieval only backs off. Validators never receive Assistant context. Any non-duplicate Lean-verified proof from that user-triggered check is stored in the active manual proof database and appended to the active manual Aggregator database proof appendix for user-visible display/download, regardless of novelty rating. This known-proof preservation is intentional for RALPH looping: the user can see validated work, and later proof checks can avoid redoing exact verified proofs instead of losing them because they ranked `not_novel`. Progress is also persisted to the manual Aggregator event log so live activity can recover missed WebSocket events. Later proof-check prompts strip that generated-proof appendix and receive verified proofs through the manual proof database injection instead. Manual Aggregator clear archives the active manual proof database to history and resets active proof context to empty; clear is rejected while manual proof verification is active. +Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It uses standard proof discovery, asking for candidates that directly solve the user prompt first and then candidates that substantially build toward solving it. When Session History Memory is enabled, the separate Assistant LLM role runs in parallel during brainstorming and proof checks, maintaining a freshness-tagged up-to-7 pack of fully Lean-verified local/SyntheticLib4 memory supports for eligible submitter/proof roles; proof discovery/formalization may use the latest pack but must not wait for it, and useful packs refresh only after two eligible receiver reads. Assistant cooldown state is run-scoped across transient task IDs/roles, survives ordinary stop/restart for that same run scope, is cleared only by explicit workflow/session reset, hides skip/backoff/shutdown turns from live activity, and shows Assistant model-output failures as errors; zero-useful retrieval can shut down for the run, while stagnant same-pack retrieval only backs off. Validators never receive Assistant context. Any non-duplicate Lean-verified proof from that user-triggered check is stored in the active manual proof database and appended to the active manual Aggregator database proof appendix for user-visible display/download, regardless of novelty rating. This known-proof preservation is intentional for RALPH looping: the user can see validated work, and later proof checks can avoid redoing exact verified proofs instead of losing them because they ranked `not_novel`. Progress is also persisted to the manual Aggregator event log so live activity can recover missed WebSocket events. Later proof-check prompts strip that generated-proof appendix and receive verified proofs through the manual proof database injection instead. Manual Aggregator clear archives the active manual proof database to history and resets active proof context to empty; clear is rejected while manual proof verification is active. diff --git a/.cursor/rules/part-1-and-part-2-cointeraction-architecture.mdc b/.cursor/rules/part-1-and-part-2-cointeraction-architecture.mdc index 17341a8..f683312 100644 --- a/.cursor/rules/part-1-and-part-2-cointeraction-architecture.mdc +++ b/.cursor/rules/part-1-and-part-2-cointeraction-architecture.mdc @@ -81,7 +81,7 @@ Parent workflow actions override child agents immediately. Manual paper writing, ## Assistant Proof-Retrieval Role -Aggregator, Compiler, Autonomous Research, and LeanOJ expose one shared `Assistant` LLM model role per workflow surface for non-blocking verified proof-memory retrieval. Assistant is not a submitter, validator, proof checker, workflow phase, or per-lane clone. Eligible main roles may consume the latest up-to-7 verified proof pack opportunistically, and useful packs are refreshed only after two eligible receiver reads; validators and dedicated critique phases never receive Assistant context. The configured Assistant LLM owns live pack selection, parent workflows never wait on it, and no-history targets are skipped because Assistant only performs proof-memory retrieval for now. Durable cooldown is run-scoped across transient task IDs/roles while preserving real source/session separation; zero-useful retrieval can shut down for the current run, while stagnant same-pack retrieval only backs off. Live activity should show normal Assistant retrieval result summaries only, not skip/backoff/shutdown turns. Built-in/default profiles copy Assistant settings from the primary Validator; if Session History Memory is disabled, Assistant is greyed out and does not run. +Aggregator, Compiler, Autonomous Research, and LeanOJ expose one shared `Assistant` LLM model role per workflow surface for non-blocking verified proof-memory retrieval. Assistant is not a submitter, validator, proof checker, workflow phase, or per-lane clone. Eligible main roles may consume the latest up-to-7 verified proof pack opportunistically, and useful packs are refreshed only after two eligible receiver reads; validators and dedicated critique phases never receive Assistant context. The configured Assistant LLM owns live pack selection, parent workflows never wait on it, and no-history targets are skipped because Assistant only performs proof-memory retrieval for now. Durable cooldown is run-scoped across transient task IDs/roles while preserving real source/session separation; zero-useful retrieval can shut down for the current run, while stagnant same-pack retrieval only backs off. Live activity should show normal Assistant retrieval result summaries and explicit Assistant model-output failures, not skip/backoff/shutdown turns. Retrieved supports are advisory: receivers must judge relevance, ignore unrelated supports, and never let Assistant packs broaden candidate eligibility, replace targets, or alter phase decisions. Built-in/default profiles copy Assistant settings from the primary Validator; if Session History Memory is disabled, Assistant is greyed out and does not run. ## Additional Traits Shared Between Aggregator-Submitters and Compiler-Submitters diff --git a/.cursor/rules/part-2-compiler-tool-design-specification.mdc b/.cursor/rules/part-2-compiler-tool-design-specification.mdc index 228e011..033e27a 100644 --- a/.cursor/rules/part-2-compiler-tool-design-specification.mdc +++ b/.cursor/rules/part-2-compiler-tool-design-specification.mdc @@ -32,7 +32,7 @@ Before every `_pre_validate_exact_string_match()`, system calls `paper_memory.en **Provider Selection**: Each visible compiler role (Validator, Writing, Rigor & Proofs, Assistant) can independently use LM Studio, OpenRouter, or desktop-only cloud providers such as OpenAI Codex OAuth, xAI Grok OAuth, or Sakana Fugu API key with optional LM Studio fallback for cloud providers (default mode). Deprecated `critique_submitter_*` request fields are compatibility aliases for Rigor & Proofs. OpenRouter keeps optional host-provider selection. In generic mode, all roles use OpenRouter only; LM Studio/OAuth options are hidden or unavailable. Built-in/default profiles set Assistant equal to the primary Validator unless the user edits it. -**Assistant memory support**: When Session History Memory is enabled, compiler/manual writer uses one shared `compiler_assistant` memory role, not one Assistant per writer/rigor/proof lane. Assistant runs beside eligible non-validator, non-critique compiler writing/review/rigor/proof roles as optional verified proof-memory support. It may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, and never blocks compiler progress. Durable cooldown is run-scoped across transient compiler task IDs/roles: zero-useful retrieval can eventually shut down for that run, while stagnant same-pack retrieval only backs off. Live activity should show normal Assistant retrieval result summaries only, not skip/backoff/shutdown turns. Compiler validators and dedicated critique/self-review phases never receive Assistant context. +**Assistant memory support**: When Session History Memory is enabled, compiler/manual writer uses one shared `compiler_assistant` memory role, not one Assistant per writer/rigor/proof lane. Assistant runs beside eligible non-validator, non-critique compiler writing/review/rigor/proof roles as optional verified proof-memory support. It may provide up to 7 prior verified proofs, reuses useful packs for two eligible receiver reads before refresh, skips true no-external-history targets because it only performs proof-memory retrieval for now, and never blocks compiler progress. Durable cooldown is run-scoped across transient compiler task IDs/roles: zero-useful retrieval can eventually shut down for that run, while stagnant same-pack retrieval only backs off. Live activity should show normal Assistant retrieval result summaries and explicit Assistant model-output failures, not skip/backoff/shutdown turns. Compiler validators and dedicated critique/self-review phases never receive Assistant context. **Allowed Outputs**: Single Paper Writer start requests include `allow_mathematical_proofs` and `allow_research_papers`; at least one must be true. Both true preserves today's paper-writing plus optional proof behavior. The Mathematical Proofs checkbox is the user-facing proof-output enable path and must not imply proof work when Lean is unavailable; proofs-only starts should reject clearly if Lean is disabled/unavailable. Papers-only suppresses rigor/save-time proof work for that run. Proofs-only runs proof verification over the current Aggregator database instead of compiling a paper, exposes running/stoppable status while the background proof check is active, and remains separate from developer-mode Creativity Emphasis Boost. Manual writer proof output (rigor proofs, save-time checks, proof-only checks, and "Try to Prove This") stores in the active manual proof database and appears in the Manual Mathematical Proofs tab, not in the autonomous session proof tab/activity/graph. Manual Aggregator/Compiler clear actions archive the active manual proof database into manual proof-run history, reset active proof context to empty, and remove the manual Aggregator proof appendix when needed, so old proofs never seed a new manual run; clears are rejected while manual proof verification is active. Manual proof checks always use standard proof discovery: candidates that directly solve the user prompt first, then candidates that substantially build toward solving it. When Session History Memory is enabled, the Assistant role may run in parallel for manual proof checks and live-paper proof checks, but checks continue without waiting for Assistant. Manual Aggregator proof checks (button or proofs-only Single Paper Writer) append any non-duplicate Lean-verified proof to the active Aggregator proof appendix for live display/download and future proof checks in the same active run, regardless of novelty rating; preserving known verified proofs here is intentional RALPH-loop state and exact duplicate avoidance, not a bug. Proof-check source prompts strip existing generated-proof appendices because verified proofs enter through the active manual proof database injection. Manual Aggregator proof checks must recover the persisted manual Aggregator prompt when the live coordinator prompt is unavailable after stop/restart. Manual `Try to Prove This` role resolution must use the active/manual Aggregator or Compiler role settings, including validator and Assistant settings, and must not fall back to autonomous proof runtime snapshots. The manual live paper exposes a read-only "Try to Prove This" check over the current paper plus current Aggregator context; it appends any non-duplicate Lean-verified proof to the live paper proof appendix regardless of novelty rating for the same manual RALPH-loop reason, while save-time proof checks append novel proofs to the saved paper text file. diff --git a/.cursor/rules/part-3-autonomous-research-mode.mdc b/.cursor/rules/part-3-autonomous-research-mode.mdc index 8faffaf..acc147a 100644 --- a/.cursor/rules/part-3-autonomous-research-mode.mdc +++ b/.cursor/rules/part-3-autonomous-research-mode.mdc @@ -328,9 +328,9 @@ The autonomous brainstorm aggregator inherits batch validation from Part 1 infra - Behavior: Immediately transition to paper writing, skip completion review - WebSocket event: `brainstorm_hard_limit_reached` - **TOTAL across all rounds**: When `continue_existing` resumes an incomplete brainstorm, the 30-cap applies to the TOTAL acceptance count (prior + new). The aggregator loop tracks a `resume_acceptance_base` offset so `_acceptance_count` always reflects the true total. If a topic already has >= 30 acceptances on entry, aggregation is skipped entirely and paper writing is forced immediately. -6. **Rejection Hard Limit**: 10 consecutive rejections (with minimum 5 acceptances) FORCE transition to paper writing +6. **Rejection Hard Limit**: 10 consecutive rejections (with minimum 7 acceptances) FORCE transition to paper writing - Purpose: Prevents infinite rejection loops when brainstorm is exhausted - - Trigger: After rejection, check if consecutive rejections >= 10 AND acceptances >= 5 + - Trigger: After rejection, check if consecutive rejections >= 10 AND acceptances >= 7 - Behavior: Immediately transition to paper writing, skip completion review - WebSocket event: `brainstorm_rejection_limit_reached` @@ -357,7 +357,7 @@ Runs after each configured interval of accepted submissions (default 10). Cleanu **Hard Limit Override**: If brainstorm reaches 30 accepted submissions, completion review is SKIPPED and paper writing is forced. -**Early Review Triggers**: The coordinator may also run completion review early when accepted-submission polling observes exhaustion signals. The 10-consecutive-rejection rule force-transitions only after the minimum acceptance threshold is met. +**Early Review Triggers**: The coordinator may also run completion review early when accepted-submission polling observes exhaustion signals, but model-driven completion reviews are deferred until at least 7 accepted submissions. The 10-consecutive-rejection rule force-transitions only after the minimum acceptance threshold is met. **Example trigger behavior**: - Review runs once the accepted-event count has advanced by the configured interval since the last review; parallel submitters may jump past exact multiples @@ -1205,7 +1205,7 @@ Runs automatically after every completed brainstorm (Tier 1) and completed Tier **Automatic proof rounds**: Proofs-only autonomous runs let brainstorm proof checkpoints run the pipeline below for up to 4 rounds. Round 1 uses normal candidate identification. After each completed round, the coordinator asks again whether there are any remaining proofs in the same source that directly solve the user's prompt or substantially advance a solution path, with newly verified proofs visible through the proof-library context. The checkpoint stops early when a round finds no candidates. When research papers and mathematical proofs are both enabled, automatic proof checkpoints after brainstorming and after completed paper writing are single-round so paper generation remains the main output path. Manual proof checks, deferred paper retry checks, compiler rigor, and LeanOJ are single-round unless their own mode rules say otherwise. The per-source reservation spans the whole automatic multi-round checkpoint, and completed earlier rounds must never overwrite an active later-round resume cursor. -**Assistant memory-support role**: When Session History Memory is enabled, each active workflow uses one shared Assistant memory role (`autonomous_assistant` for autonomous, `leanoj_assistant` for LeanOJ), not one Assistant per submitter/proof candidate/solver lane. Assistant runs beside eligible non-validator, non-critique brainstorming, selection, writing, proof, and Tier 3 roles as optional verified proof-memory support; short-lived topic/title exploration candidate mini-aggregators are excluded. It may provide up to 7 prior verified proof supports from enabled proof-history corpora and reuse useful packs for two eligible receiver reads before refresh, but validators never receive Assistant context and parent workflows never wait on Assistant. Assistant skips true no-external-history targets because it only performs proof-memory retrieval for now. Durable cooldown is keyed to stable run scope, grouping transient task IDs/roles while preserving real source/session separation; zero-useful retrieval can eventually shut down for the run, while stagnant same-pack retrieval backs off without shutdown. User live activity should show normal Assistant retrieval result summaries only, not skip/backoff/shutdown turns. Stale live packs/state clear only on explicit reset/clear or Session History Memory disable. +**Assistant memory-support role**: When Session History Memory is enabled, each active workflow uses one shared Assistant memory role (`autonomous_assistant` for autonomous, `leanoj_assistant` for LeanOJ), not one Assistant per submitter/proof candidate/solver lane. Assistant runs beside eligible non-validator, non-critique brainstorming, selection, writing, proof, and Tier 3 roles as optional verified proof-memory support; short-lived topic/title exploration candidate mini-aggregators are excluded. It may provide up to 7 prior verified proof supports from enabled proof-history corpora and reuse useful packs for two eligible receiver reads before refresh, but validators never receive Assistant context and parent workflows never wait on Assistant. Assistant skips true no-external-history targets because it only performs proof-memory retrieval for now. Durable cooldown is keyed to stable run scope, grouping transient task IDs/roles while preserving real source/session separation; zero-useful retrieval can eventually shut down for the run, while stagnant same-pack retrieval backs off without shutdown. User live activity should show normal Assistant retrieval result summaries and explicit Assistant model-output failures, not skip/backoff/shutdown turns. Stale live packs/state clear only on explicit reset/clear or Session History Memory disable. **Pipeline** (`backend/autonomous/core/proof_verification_stage.py`): 1. **Candidate identification** — `ProofIdentificationAgent` (`build_proof_identification_prompt`) extracts prompt-relevant, high-impact new/novel theorem candidates from brainstorm or paper content. For brainstorms, the brainstorm topic is bounded source-local metadata only and must not broaden eligibility beyond proofs that directly solve, or visibly build toward solving, the user prompt. This stage is not a general known-knowledge-base builder: candidates are ordered by impact on the user prompt (direct solutions/impossibility results first, then decisive reductions, obstructions, and structural theorems that themselves make major progress). Candidate JSON includes non-empty `expected_novelty_tier`, `prompt_relevance_rationale`, `novelty_rationale`, and `why_not_standard_known_result`; invalid, missing-rationale, or `not_novel` candidates are skipped before Lean 4 cost is incurred. Routine helpers, supporting lemmas, trivial/easy proofs, standard/textbook/Mathlib restatements, off-prompt curiosities, program-local firsts, minor reformulations, and single-tactic/routine proof goals are rejected even as fallback targets. @@ -1251,7 +1251,7 @@ Runs automatically after every completed brainstorm (Tier 1) and completed Tier 14. Post-Lean integrity scanning rejects newly introduced `axiom`, `constant`, and `opaque` declarations even when the declaration name appears on following lines. Generated source text is not an authorization baseline unless explicitly passed as allowed baseline. 15. Lean-accepted real proof code is preservation-worthy even when it misses the intended candidate. Alignment classifiers may downshift the stored theorem statement and ranking may classify it as `not_novel`, but the proof artifact must not be discarded except for hard integrity failures. 16. Unified proof/history search is bounded retrieval support only. It must never broaden proof candidate identification beyond the user's prompt, replace mandatory source context, or count SyntheticLib4 retrieved records as new MOTO proofs without the normal MOTO artifact path. -17. Assistant memory-support retrieval is a parallel, non-blocking configured LLM role across eligible non-validator, non-critique brainstorming, writing, proof, selection/path, and final-answer roles. It provides optional up-to-7 verified proof supports, reuses useful packs for two eligible receiver reads before refresh, skips no-external-history targets, uses durable run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns from live activity, clears stale live packs/state on explicit reset/clear or Session History Memory disable, and never alters phase transitions or candidate eligibility. +17. Assistant memory-support retrieval is a parallel, non-blocking configured LLM role across eligible non-validator, non-critique brainstorming, writing, proof, selection/path, and final-answer roles. It provides optional up-to-7 verified proof supports, reuses useful packs for two eligible receiver reads before refresh, skips no-external-history targets, uses durable run-scoped cooldown for repeated zero-useful or stagnant retrieval, shuts down only for repeated zero-useful retrieval in the current run, hides skip/backoff/shutdown turns from live activity while showing Assistant model-output failures, clears stale live packs/state on explicit reset/clear or Session History Memory disable, and never alters phase transitions or candidate eligibility. --- @@ -1662,7 +1662,7 @@ Normal GUI/API startup must pass explicit context-window and max-output-token se 24. **Critiques append as self-review, never rewrite** - Post-body critique runs 3 total attempts and appends validator-accepted critiques as `AI Self-Review and Limitations`; no partial or total body rewrites are allowed 25. **Self-review follows proofs/conclusion** - The self-review section is inserted immediately before the paper anchor as the final reader-facing section, and later proof appends must stay before it 26. **Critique declines remain valid** - If no critiques are accepted after the 3 attempts, the workflow proceeds to conclusion without adding a self-review section -27. **Rejection hard limit is 10 consecutive rejections (with 5+ acceptances)** - Forces paper writing. Ten consecutive rejections before 5 acceptances may trigger an early completion review instead. +27. **Rejection hard limit is 10 consecutive rejections (with 7+ acceptances)** - Forces paper writing. Model-driven completion reviews and rejection-limit handoff are deferred before 7 acceptances. 28. **Retroactive brainstorm corrections during Tier 2 paper compilation** - Submitter sees unified paper+brainstorm workspace; operations validated independently by validator (paper-only context for paper ops, brainstorm-only context for brainstorm ops); each operation must stand alone without requiring the other for correctness 29. **Max 3 papers per brainstorm** - hard limit, continuation decision skipped after 3rd paper 30. **Prior brainstorm papers ALWAYS auto-included** for paper 2/3 as `is_user_file=True` in RAG, separate from 6-paper cross-topic reference limit diff --git a/.cursor/rules/program-directory-and-file-definitions.mdc b/.cursor/rules/program-directory-and-file-definitions.mdc index 03d2624..535133d 100644 --- a/.cursor/rules/program-directory-and-file-definitions.mdc +++ b/.cursor/rules/program-directory-and-file-definitions.mdc @@ -406,7 +406,7 @@ project-root/ - `Click To Launch MOTO.bat`: The only Windows consumer entrypoint. It bootstraps a usable Python 3.10+ interpreter on fresh Windows installs when `winget` is available, refreshes/relaunches once if the current console cannot see the new runtime, then delegates to the Python launcher. - `linux-ubuntu-launcher.sh`: The Linux/Ubuntu consumer entrypoint. Same thin-wrapper contract as the `.bat`; delegates to `moto_launcher.py`. -- `moto_launcher.py`: Orchestrates the launcher flow in order: update check, runtime resolution, dependency install, LM Studio detection, detached backend/frontend startup, and browser launch. After fresh Windows Node.js installs, it refreshes/prepends Node paths so npm child scripts can resolve `node` immediately. +- `moto_launcher.py`: Orchestrates the launcher flow in order: update check, runtime resolution, dependency install, LM Studio detection, detached backend/frontend startup, and browser launch. Windows Node.js bootstrap uses bounded `winget` source/package/scope fallbacks, then refreshes/prepends Node paths so npm child scripts can resolve `node` immediately. - `moto_updater.py`: Owns Build 1 updater behavior, including GitHub REST contents metadata + branch-HEAD resolution, install-state classification, clean-git fast-forward apply, ZIP overlay apply with post-apply manifest stamping, rollback-aware relaunch, and launcher-managed instance safety checks. - `.moto_launcher_state.json`: Local-only state written by the launcher so future launches can detect still-open backend/frontend windows from the same install and skip update-apply until those windows are closed. diff --git a/README.md b/README.md index 986b1bf..b40f325 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # MOTO Autonomous ASI ## Autonomous Prototype Superintelligence - Automated Theorem Generation with Lean 4 Math Proof Verification -**Version: 1.1.01** +**Version: 1.1.02** [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) [![Python 3.10+](https://img.shields.io/badge/python-3.10+-blue.svg)](https://www.python.org/downloads/) @@ -482,4 +482,3 @@ Because the heavy model inference happens in the cloud, MOTO can run on very mod --- Intrafere™ and Intrafere Research Group™ are trademarks of Intrafere LLC. All rights reserved. - diff --git a/backend/aggregator/agents/submitter.py b/backend/aggregator/agents/submitter.py index 4826bdd..304908a 100644 --- a/backend/aggregator/agents/submitter.py +++ b/backend/aggregator/agents/submitter.py @@ -12,7 +12,7 @@ from backend.shared.config import rag_config, system_config from backend.shared.models import Submission, SubmitterState from backend.shared.lm_studio_client import lm_studio_client -from backend.shared.api_client_manager import OAuthProviderCooldownError, api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.brainstorm_proof_gate import is_lean_proof_submission, verify_brainstorm_proof_candidate from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json, sanitize_model_output_for_retry_context @@ -190,15 +190,16 @@ async def _run_loop(self) -> None: # All free models exhausted after retries - wait briefly and retry logger.warning(f"Submitter {self.submitter_id}: all free models exhausted: {e}") await asyncio.sleep(120) # Wait before retrying (all models exhausted) - except OAuthProviderCooldownError as e: + except RetryableProviderError as e: logger.warning( - "Submitter %s paused for OAuth provider cooldown: %s", + "Submitter %s paused for retryable provider failure: %s", self.submitter_id, e, ) - await api_client_manager.wait_for_oauth_provider_cooldown( + await api_client_manager.wait_for_retryable_provider_error( e, role_id=self.role_id, + should_stop=lambda: not self.is_running, ) except ContextAllocationError as e: logger.error("Submitter %s context overflow: %s", self.submitter_id, e) @@ -360,6 +361,23 @@ async def _generate_submission(self) -> Optional[Submission]: except (httpx.HTTPStatusError, ValueError) as e: error_msg = str(e) is_400_or_context = "400" in error_msg or "context" in error_msg.lower() + + if "context" in error_msg.lower(): + if self.task_tracking_callback: + self.task_tracking_callback("completed", task_id) + raise ContextAllocationError( + f"Submitter {self.submitter_id} context overflow or provider context mismatch: " + f"the assembled prompt requires {actual_prompt_tokens:,} tokens and the configured " + f"input budget is {max_allowed_tokens:,} tokens (context window: {self.context_window:,}, " + f"output reserve: {self.max_output_tokens:,}). The provider rejected the request " + "as too large, so the loaded/provider context is smaller than configured. Please condense " + "into a new prompt and restart, select a larger-context model, or reload the local model " + "with the configured context window.", + required_tokens=actual_prompt_tokens, + available_tokens=max_allowed_tokens, + context_window=self.context_window, + output_reserve=self.max_output_tokens, + ) from e if is_400_or_context and attempt < max_retries - 1: backoff_time = min(2 ** attempt, 16) @@ -374,20 +392,6 @@ async def _generate_submission(self) -> Optional[Submission]: logger.error( f"Submitter {self.submitter_id}: Failed to generate completion after {attempt + 1} attempts: {e}" ) - if "context" in error_msg.lower(): - raise ContextAllocationError( - f"Submitter {self.submitter_id} context overflow or provider context mismatch: " - f"the assembled prompt requires {actual_prompt_tokens:,} tokens and the configured " - f"input budget is {max_allowed_tokens:,} tokens (context window: {self.context_window:,}, " - f"output reserve: {self.max_output_tokens:,}). The provider still rejected the request " - "as too large, so the loaded/provider context is smaller than configured. Please condense " - "into a new prompt and restart, select a larger-context model, or reload the local model " - "with the configured context window.", - required_tokens=actual_prompt_tokens, - available_tokens=max_allowed_tokens, - context_window=self.context_window, - output_reserve=self.max_output_tokens, - ) from e # Notify task completed (failed but still completed) if self.task_tracking_callback: self.task_tracking_callback("completed", task_id) @@ -395,7 +399,7 @@ async def _generate_submission(self) -> Optional[Submission]: except FreeModelExhaustedError: raise - except OAuthProviderCooldownError: + except RetryableProviderError: raise except RuntimeError as e: if "credits exhausted" in str(e).lower(): diff --git a/backend/aggregator/agents/validator.py b/backend/aggregator/agents/validator.py index 11afd3c..6a95575 100644 --- a/backend/aggregator/agents/validator.py +++ b/backend/aggregator/agents/validator.py @@ -10,7 +10,7 @@ from backend.shared.config import rag_config from backend.shared.models import Submission, ValidationResult from backend.shared.lm_studio_client import lm_studio_client -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json, sanitize_model_output_for_retry_context from backend.shared.response_extraction import extract_message_text @@ -111,7 +111,7 @@ async def validate_submission(self, submission: Submission) -> ValidationResult: return quality_result - except (FreeModelExhaustedError, ContextAllocationError): + except (FreeModelExhaustedError, ContextAllocationError, RetryableProviderError): raise except Exception as e: logger.error(f"Validation failed: {e}") @@ -271,6 +271,8 @@ async def _assess_quality(self, submission: Submission) -> ValidationResult: json_valid=False ) + except RetryableProviderError: + raise except Exception as e: logger.error(f"Validator: Unexpected error during validation: {e}") # Notify task completed (failed but still completed) @@ -396,6 +398,8 @@ async def _assess_quality(self, submission: Submission) -> ValidationResult: logger.warning(f"Validator: Retry failed - {error}") else: logger.warning("Validator: Retry request returned no choices") + except RetryableProviderError: + raise except Exception as e: logger.error(f"Validator: Retry request failed - {e}") @@ -763,7 +767,7 @@ async def _assess_batch_quality(self, submissions: List[Submission]) -> List[Val return results - except (FreeModelExhaustedError, ContextAllocationError): + except (FreeModelExhaustedError, ContextAllocationError, RetryableProviderError): raise except Exception as e: error_text = str(e) @@ -891,6 +895,8 @@ async def _retry_batch_json_parse( parsed = parse_json(retry_output) logger.info("Batch validator: Conversational retry succeeded!") return parsed, call_metadata + except RetryableProviderError: + raise except Exception as e: logger.warning(f"Batch validator: Retry failed - {e}") @@ -1105,6 +1111,8 @@ async def perform_cleanup_review(self) -> Optional[Dict]: except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"CLEANUP DEBUG: EXCEPTION in perform_cleanup_review: {e}", exc_info=True) logger.error(f"Cleanup review failed: {e}", exc_info=True) @@ -1292,6 +1300,8 @@ async def validate_removal( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"CLEANUP DEBUG: EXCEPTION in validate_removal: {e}", exc_info=True) logger.error(f"Removal validation failed: {e}", exc_info=True) diff --git a/backend/aggregator/core/coordinator.py b/backend/aggregator/core/coordinator.py index 00f3802..a9c278c 100644 --- a/backend/aggregator/core/coordinator.py +++ b/backend/aggregator/core/coordinator.py @@ -13,7 +13,7 @@ from backend.shared.models import SystemStatus, Submission, ValidationResult, SubmitterConfig, WorkflowTask, ModelConfig, ProofAttemptFeedback from backend.shared.lm_studio_client import lm_studio_client from backend.shared.rag_lock import rag_operation_lock -from backend.shared.api_client_manager import OAuthProviderCooldownError, api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.free_model_manager import free_model_manager from backend.shared.path_safety import resolve_path_within_root, validate_single_path_component @@ -864,11 +864,12 @@ async def _validator_loop(self) -> None: "message": "All free models exhausted, waiting to retry", }) await asyncio.sleep(120) # Wait before retrying (all models exhausted) - except OAuthProviderCooldownError as e: - logger.warning("Validator paused for OAuth provider cooldown: %s", e) - await api_client_manager.wait_for_oauth_provider_cooldown( + except RetryableProviderError as e: + logger.warning("Validator paused for retryable provider failure: %s", e) + await api_client_manager.wait_for_retryable_provider_error( e, role_id="aggregator_validator", + should_stop=lambda: not self.is_running, ) except ContextAllocationError as e: await self._handle_context_overflow(e, role_id="aggregator_validator") @@ -980,11 +981,12 @@ async def _single_model_workflow(self) -> None: "message": "All free models exhausted, waiting to retry", }) await asyncio.sleep(120) # Wait before retrying (all models exhausted) - except OAuthProviderCooldownError as e: - logger.warning("Single-model workflow paused for OAuth provider cooldown: %s", e) - await api_client_manager.wait_for_oauth_provider_cooldown( + except RetryableProviderError as e: + logger.warning("Single-model workflow paused for retryable provider failure: %s", e) + await api_client_manager.wait_for_retryable_provider_error( e, role_id="aggregator_single_model", + should_stop=lambda: not self.is_running, ) except ContextAllocationError as e: await self._handle_context_overflow(e, role_id="aggregator_single_model") diff --git a/backend/api/routes/proofs.py b/backend/api/routes/proofs.py index bb7d9ca..efbb5e9 100644 --- a/backend/api/routes/proofs.py +++ b/backend/api/routes/proofs.py @@ -141,13 +141,18 @@ def _compact(value: object, limit: int = 1200) -> str: def _lean_response() -> str: if data.get("lean_response"): - return _compact(data.get("lean_response")) + response = _compact(data.get("lean_response")) + if "timed out after" in response.lower() and "Advanced Settings" not in response: + response = f"{response} You can change this timeout in Advanced Settings." + return response if data.get("proof_verified") is True: return "Lean 4 response: proof verified." error = _compact( data.get("error_summary") or data.get("error_output") or data.get("reason"), limit=1800, ) + if error and "timed out after" in error.lower() and "Advanced Settings" not in error: + error = f"{error} You can change this timeout in Advanced Settings." return f"Lean 4 response: {error} - proof not verified." if error else "" def _attempt_message(prefix: str) -> str: diff --git a/backend/autonomous/agents/completion_reviewer.py b/backend/autonomous/agents/completion_reviewer.py index 7708f9a..5a92d67 100644 --- a/backend/autonomous/agents/completion_reviewer.py +++ b/backend/autonomous/agents/completion_reviewer.py @@ -11,7 +11,7 @@ import logging from typing import Optional, Tuple, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -282,6 +282,8 @@ async def _generate_assessment( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"CompletionReviewer: Error generating assessment: {e}") if self.task_tracking_callback and 'task_id' in dir(): @@ -393,6 +395,8 @@ async def _self_validate( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"CompletionReviewer: Error in self-validation: {e}") if self.task_tracking_callback and 'task_id' in dir(): diff --git a/backend/autonomous/agents/final_answer/answer_format_selector.py b/backend/autonomous/agents/final_answer/answer_format_selector.py index 21ef922..eb8e1bb 100644 --- a/backend/autonomous/agents/final_answer/answer_format_selector.py +++ b/backend/autonomous/agents/final_answer/answer_format_selector.py @@ -15,7 +15,7 @@ import logging from typing import Optional, List, Dict, Any, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.model_error_utils import ( is_non_retryable_model_error, @@ -38,7 +38,8 @@ def _is_tier3_model_call_failure(exc: Exception) -> bool: message = str(exc or "").lower() return ( - is_non_retryable_model_error(exc) + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "upstream provider timeout" in message or "response missing 'choices'" in message diff --git a/backend/autonomous/agents/final_answer/certainty_assessor.py b/backend/autonomous/agents/final_answer/certainty_assessor.py index cf526d2..65ebf49 100644 --- a/backend/autonomous/agents/final_answer/certainty_assessor.py +++ b/backend/autonomous/agents/final_answer/certainty_assessor.py @@ -14,7 +14,7 @@ import logging from typing import Optional, List, Dict, Any, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.model_error_utils import ( is_non_retryable_model_error, @@ -39,7 +39,8 @@ def _is_tier3_model_call_failure(exc: Exception) -> bool: message = str(exc or "").lower() return ( - is_non_retryable_model_error(exc) + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "upstream provider timeout" in message or "response missing 'choices'" in message diff --git a/backend/autonomous/agents/final_answer/volume_organizer.py b/backend/autonomous/agents/final_answer/volume_organizer.py index b3a26d4..b65f7f8 100644 --- a/backend/autonomous/agents/final_answer/volume_organizer.py +++ b/backend/autonomous/agents/final_answer/volume_organizer.py @@ -17,7 +17,7 @@ import logging from typing import Optional, List, Dict, Any, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.model_error_utils import ( is_non_retryable_model_error, @@ -44,7 +44,8 @@ def _is_tier3_model_call_failure(exc: Exception) -> bool: message = str(exc or "").lower() return ( - is_non_retryable_model_error(exc) + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "upstream provider timeout" in message or "response missing 'choices'" in message diff --git a/backend/autonomous/agents/lemma_search_agent.py b/backend/autonomous/agents/lemma_search_agent.py index f0f8934..c0bf1e5 100644 --- a/backend/autonomous/agents/lemma_search_agent.py +++ b/backend/autonomous/agents/lemma_search_agent.py @@ -10,7 +10,7 @@ from typing import Dict, List from backend.autonomous.prompts.proof_prompts import build_lemma_search_prompt -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text from backend.shared.lean4_client import get_lean4_client @@ -305,6 +305,8 @@ async def suggest_relevant_lemmas( return confirmed_hits[:max_candidates] except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as exc: if is_non_retryable_model_error(exc): raise diff --git a/backend/autonomous/agents/paper_title_selector.py b/backend/autonomous/agents/paper_title_selector.py index 125527b..e1794e4 100644 --- a/backend/autonomous/agents/paper_title_selector.py +++ b/backend/autonomous/agents/paper_title_selector.py @@ -10,7 +10,7 @@ import logging from typing import Optional, Dict, Any, List, Tuple, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.model_error_utils import ( is_non_retryable_model_error, @@ -32,7 +32,8 @@ def _is_title_model_call_failure(exc: Exception) -> bool: message = str(exc or "").lower() return ( - is_non_retryable_model_error(exc) + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "upstream provider timeout" in message or "response missing 'choices'" in message diff --git a/backend/autonomous/agents/proof_formalization_agent.py b/backend/autonomous/agents/proof_formalization_agent.py index c8330db..06a2858 100644 --- a/backend/autonomous/agents/proof_formalization_agent.py +++ b/backend/autonomous/agents/proof_formalization_agent.py @@ -8,7 +8,7 @@ import logging from typing import Any, Awaitable, Callable, List, Optional, Tuple -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text from backend.shared.lean4_client import get_lean4_client @@ -72,10 +72,6 @@ def _assistant_workflow_mode_for_role(role_id: str) -> str: "MODEL OUTPUT INCOMPLETE: provider stopped before returning usable proof output " "(max_output_tokens). Preserve the proof checkpoint and retry with adjusted output budget or prompt size." ) -_TRANSIENT_PROVIDER_ERROR = ( - "TRANSIENT PROVIDER ERROR: provider connection failed before usable proof output. " - "Preserve the proof checkpoint and retry later." -) _LEAN_WORKSPACE_ERROR_PREFIX = "LEAN 4 WORKSPACE ERROR" _MANDATORY_FULL_SOURCE_CONTEXT_OVERFLOW_PREFIX = "MANDATORY FULL SOURCE CONTEXT OVERFLOW" _PROOF_SEARCH_CONTEXT_OMITTED = ( @@ -419,13 +415,22 @@ async def _run_full_script_attempt( return theorem_name, source_excerpt, feedback except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as exc: if is_non_retryable_model_error(exc): raise if is_retryable_model_output_error(exc): raise RuntimeError(_INCOMPLETE_MODEL_OUTPUT_ERROR) from exc if is_transient_model_call_error(exc): - raise RuntimeError(format_transient_provider_error(exc)) from exc + raise RetryableProviderError( + provider="unknown", + provider_label="Inference provider", + role_id=self.role_id, + model=self.model_id, + reason="transient_provider_error", + message=format_transient_provider_error(exc), + ) from exc is_parse_error = _is_json_parse_error(exc) feedback = ProofAttemptFeedback( attempt=attempt_number, @@ -835,13 +840,22 @@ async def prove_candidate_tactic_script( attempt_offset += 1 except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as exc: if is_non_retryable_model_error(exc): raise if is_retryable_model_output_error(exc): raise RuntimeError(_INCOMPLETE_MODEL_OUTPUT_ERROR) from exc if is_transient_model_call_error(exc): - raise RuntimeError(format_transient_provider_error(exc)) from exc + raise RetryableProviderError( + provider="unknown", + provider_label="Inference provider", + role_id=self.role_id, + model=self.model_id, + reason="transient_provider_error", + message=format_transient_provider_error(exc), + ) from exc is_parse_error = _is_json_parse_error(exc) feedback = ProofAttemptFeedback( attempt=attempt_number, diff --git a/backend/autonomous/agents/proof_identification_agent.py b/backend/autonomous/agents/proof_identification_agent.py index 170f34b..c98c4b7 100644 --- a/backend/autonomous/agents/proof_identification_agent.py +++ b/backend/autonomous/agents/proof_identification_agent.py @@ -4,7 +4,7 @@ import logging from typing import List, Tuple -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text from backend.shared.model_error_utils import ( @@ -125,7 +125,11 @@ async def translate_candidate_to_smt( except FreeModelExhaustedError: raise except Exception as exc: - if is_non_retryable_model_error(exc) or is_transient_model_call_error(exc): + if ( + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) + or is_transient_model_call_error(exc) + ): raise logger.debug( "ProofIdentificationAgent SMT translation failed for theorem %s: %s", @@ -286,7 +290,11 @@ async def identify_candidates( except FreeModelExhaustedError: raise except Exception as exc: - if is_non_retryable_model_error(exc) or is_transient_model_call_error(exc): + if ( + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) + or is_transient_model_call_error(exc) + ): raise logger.error( "ProofIdentificationAgent failed for %s %s: %s", diff --git a/backend/autonomous/agents/reference_selector.py b/backend/autonomous/agents/reference_selector.py index 52c82cb..96af3ca 100644 --- a/backend/autonomous/agents/reference_selector.py +++ b/backend/autonomous/agents/reference_selector.py @@ -22,7 +22,7 @@ import logging from typing import Optional, Dict, Any, List, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.model_error_utils import ( is_non_retryable_model_error, @@ -47,7 +47,8 @@ def _is_reference_model_call_failure(exc: Exception) -> bool: message = str(exc or "").lower() return ( - is_non_retryable_model_error(exc) + isinstance(exc, RetryableProviderError) + or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "upstream provider timeout" in message or "response missing 'choices'" in message diff --git a/backend/autonomous/agents/topic_selector.py b/backend/autonomous/agents/topic_selector.py index 63c0135..18d5252 100644 --- a/backend/autonomous/agents/topic_selector.py +++ b/backend/autonomous/agents/topic_selector.py @@ -15,7 +15,7 @@ import logging from typing import Optional, Dict, Any, List, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -222,6 +222,8 @@ async def select_topic( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"TopicSelector: Error generating submission: {e}") if self.task_tracking_callback and 'task_id' in dir(): diff --git a/backend/autonomous/agents/topic_validator.py b/backend/autonomous/agents/topic_validator.py index 87a2ac0..cca367e 100644 --- a/backend/autonomous/agents/topic_validator.py +++ b/backend/autonomous/agents/topic_validator.py @@ -14,7 +14,7 @@ import logging from typing import Optional, Dict, Any, List, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -208,6 +208,8 @@ async def validate( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"TopicValidator: Error during validation: {e}") if self.task_tracking_callback and 'task_id' in dir(): diff --git a/backend/autonomous/core/autonomous_coordinator.py b/backend/autonomous/core/autonomous_coordinator.py index 1fad7c2..140bdd9 100644 --- a/backend/autonomous/core/autonomous_coordinator.py +++ b/backend/autonomous/core/autonomous_coordinator.py @@ -24,7 +24,7 @@ WorkflowTask, ModelConfig ) -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.free_model_manager import free_model_manager from backend.shared.token_tracker import token_tracker @@ -92,6 +92,7 @@ _PARENT_PHASE_SHUTDOWN_TIMEOUT_SECONDS = 60 * 60 _WORKFLOW_PHASE_UNSET = object() _BRAINSTORM_ACCEPTANCE_HARD_LIMIT = 30 +_BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF = 7 _TIER2_RESUME_PHASES = { "outline", "body", @@ -103,6 +104,16 @@ "paper_proof_verification", "paper_title_exploration", } + + +def _brainstorm_rejection_handoff_allowed( + consecutive_rejections: int, + acceptance_count: int, +) -> bool: + return ( + consecutive_rejections >= 10 + and acceptance_count >= _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + ) _TIER1_RESUME_PHASES = { "topic_exploration", } @@ -742,6 +753,56 @@ async def run_single_proof_round( "reason": "openrouter_credit_exhaustion", }, ) + except RetryableProviderError as exc: + checkpoint = await research_metadata.get_proof_checkpoint(source_type, source_id) + if checkpoint and checkpoint.get("trigger") == round_trigger: + ( + checkpoint_candidates, + proof_candidate_indexes, + checkpoint_attempts, + checkpoint_theorem_names, + ) = self._deserialize_proof_checkpoint(checkpoint) + retry_candidates = checkpoint_candidates or retry_candidates + message = str(exc) + logger.warning( + "Autonomous proof verification paused for retryable provider failure (%s %s): %s", + source_type, + source_id, + message, + ) + await self._save_workflow_state(phase=f"{source_type}_proof_verification") + await self._broadcast( + "autonomous_proof_provider_paused", + { + "source_type": source_type, + "source_id": source_id, + "source_title": source_title, + "trigger": round_trigger, + "proof_round_index": proof_round_index, + "proof_max_rounds": proof_max_rounds, + "reason": exc.reason or "transient_provider_error", + "message": message, + }, + ) + await api_client_manager.wait_for_retryable_provider_error( + exc, + role_id=exc.role_id or role_suffix_override or "autonomous_proof", + should_stop=self._stop_event.is_set, + ) + if self._stop_event.is_set(): + return "stopped", None + await self._broadcast( + "autonomous_proof_provider_resumed", + { + "source_type": source_type, + "source_id": source_id, + "source_title": source_title, + "trigger": round_trigger, + "proof_round_index": proof_round_index, + "proof_max_rounds": proof_max_rounds, + "reason": exc.reason or "transient_provider_error", + }, + ) except Exception as exc: if not is_provider_credit_pause_error(exc): raise @@ -3126,6 +3187,15 @@ async def log_callback(task_id, role_id, model, provider, prompt, response, "message": "All free models exhausted, waiting to retry", }) await asyncio.sleep(120) # Wait before retrying (all models exhausted) + except RetryableProviderError as e: + logger.warning("AutonomousCoordinator paused for retryable provider failure: %s", e) + await self._save_workflow_state() + await api_client_manager.wait_for_retryable_provider_error( + e, + role_id=e.role_id or "autonomous", + should_stop=self._stop_event.is_set, + ) + continue except Exception as e: logger.error(f"AutonomousCoordinator error: {e}") @@ -4768,11 +4838,26 @@ async def handle_manual_override() -> bool: proof_status = await self._run_brainstorm_completion_proofs() return proof_status == "complete" - # Check for early completion triggers - early_trigger = await self._check_early_completion_triggers() + # Model-driven completion handoff is only allowed after the + # minimum accepted brainstorm size. Manual overrides and the + # hard cap are handled separately above/below. + handoff_minimum_met = ( + self._acceptance_count >= _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + ) + early_trigger = False + if handoff_minimum_met: + early_trigger = await self._check_early_completion_triggers() + elif self._consecutive_rejections >= 10: + logger.info( + "Deferring early completion review: %s consecutive rejections " + "but only %s/%s acceptances", + self._consecutive_rejections, + self._acceptance_count, + _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF, + ) # Check for completion review trigger (regular interval OR early trigger) - if self._should_run_completion_review() or early_trigger: + if handoff_minimum_met and (self._should_run_completion_review() or early_trigger): if early_trigger: logger.info("EARLY completion trigger detected - bypassing interval check") @@ -4806,9 +4891,12 @@ async def handle_manual_override() -> bool: # NOTE: Don't broadcast here - the aggregator already broadcasts # individual 'submission_rejected' events with submitter_id per submission - # Check for hard limit of 10 consecutive rejections (with minimum 5 acceptances) + # Check for hard limit of 10 consecutive rejections (with minimum 7 acceptances) # This FORCES paper writing, similar to the 30 acceptance hard limit - if self._consecutive_rejections >= 10 and self._acceptance_count >= 5: + if _brainstorm_rejection_handoff_allowed( + self._consecutive_rejections, + self._acceptance_count, + ): logger.info(f"Hard limit: {self._consecutive_rejections} consecutive rejections with {self._acceptance_count} acceptances. Forcing paper writing.") # Broadcast rejection hard limit event diff --git a/backend/autonomous/core/proof_verification_stage.py b/backend/autonomous/core/proof_verification_stage.py index 9816d2e..2d001cf 100644 --- a/backend/autonomous/core/proof_verification_stage.py +++ b/backend/autonomous/core/proof_verification_stage.py @@ -23,6 +23,7 @@ is_non_retryable_model_error, is_transient_model_call_error, ) +from backend.shared.api_client_manager import RetryableProviderError from backend.shared.models import ProofAttemptFeedback, ProofAttemptResult, ProofCandidate, ProofStageResult, SmtHint from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.provider_pause import is_provider_credit_pause_error @@ -50,7 +51,7 @@ class _LeanVerificationOutcome: class ProofVerificationProviderPause(Exception): - """Raised when proof verification must pause for provider credits.""" + """Raised when proof verification must pause for provider retry/resume.""" def __init__(self, message: str, remaining_candidates: Optional[list[ProofCandidate]] = None): super().__init__(message) @@ -200,6 +201,8 @@ def _lean_response_summary(self, feedback: ProofAttemptFeedback) -> str: return "Lean 4 response: proof verified." error_summary = self._summarize_error(feedback.error_output, limit=960) if error_summary: + if "timed out after" in error_summary.lower() and "Advanced Settings" not in error_summary: + error_summary = f"{error_summary} You can change this timeout in Advanced Settings." return f"Lean 4 response: {error_summary} - proof not verified." return "Lean 4 response: proof not verified." @@ -761,6 +764,10 @@ async def cancel_and_drain(extra_tasks=()) -> None: str(exc), remaining_unprocessed_candidates(), ) from exc + except RetryableProviderError: + await cancel_and_drain(set(done_tasks) - {future}) + await save_checkpoint("provider_paused") + raise except asyncio.CancelledError: continue except Exception as exc: @@ -1107,6 +1114,9 @@ async def cancel_and_drain(extra_tasks=()) -> None: return result except ProofVerificationProviderPause: raise + except RetryableProviderError: + await save_checkpoint("provider_paused") + raise except FreeModelExhaustedError: await save_checkpoint("provider_paused") raise @@ -1115,36 +1125,22 @@ async def cancel_and_drain(extra_tasks=()) -> None: await save_checkpoint("provider_paused") raise if is_transient_model_call_error(exc): - await save_checkpoint("error") - result.had_error = True - result.error_message = format_transient_provider_error(exc) + await save_checkpoint("provider_paused") logger.warning( "Proof verification transient provider failure for %s %s; preserving checkpoint: %s", source_type, source_id, exc, ) - await self._broadcast( - broadcast_fn, - "proof_check_complete", - { - "source_type": source_type, - "source_id": source_id, - "source_title": source_title, - "trigger": trigger, - "proof_round_index": proof_round_index, - "proof_max_rounds": proof_max_rounds, - "novel_count": result.novel_count, - "verified_count": result.verified_count, - "total_candidates": result.total_candidates, - "message": ( - "Proof verification hit a transient provider error after retries; " - "the proof checkpoint was preserved for retry: " - f"{self._summarize_error(str(exc), limit=1800)}" - ), - }, - ) - return result + role_suffix = self._role_suffix(source_type, role_suffix_override) + raise RetryableProviderError( + provider="unknown", + provider_label="Inference provider", + role_id=f"autonomous_proof_{role_suffix}", + model=submitter_model, + reason="transient_provider_error", + message=format_transient_provider_error(exc), + ) from exc await save_checkpoint("error") result.had_error = True result.error_message = str(exc) diff --git a/backend/autonomous/validation/paper_redundancy_checker.py b/backend/autonomous/validation/paper_redundancy_checker.py index 3fcba01..e10a8a2 100644 --- a/backend/autonomous/validation/paper_redundancy_checker.py +++ b/backend/autonomous/validation/paper_redundancy_checker.py @@ -10,7 +10,7 @@ import logging from typing import Optional, Dict, Any, List, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -157,6 +157,8 @@ async def check_redundancy( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"PaperRedundancyChecker: Error during check: {e}") if self.task_tracking_callback and 'task_id' in dir(): diff --git a/backend/compiler/agents/critique_submitter.py b/backend/compiler/agents/critique_submitter.py index 885cbf7..b8a518f 100644 --- a/backend/compiler/agents/critique_submitter.py +++ b/backend/compiler/agents/critique_submitter.py @@ -8,7 +8,7 @@ from backend.shared.config import rag_config from backend.shared.models import Submission -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -214,6 +214,8 @@ async def submit_critique( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except RuntimeError as e: if "credits exhausted" in str(e).lower(): raise diff --git a/backend/compiler/agents/high_param_submitter.py b/backend/compiler/agents/high_param_submitter.py index 2e38362..ff7b5e7 100644 --- a/backend/compiler/agents/high_param_submitter.py +++ b/backend/compiler/agents/high_param_submitter.py @@ -76,9 +76,11 @@ def _is_rigor_model_call_failure(exc: Exception) -> bool: """Return true for provider/config failures that must not become declines.""" + from backend.shared.api_client_manager import RetryableProviderError + message = str(exc or "").lower() return ( - isinstance(exc, OpenRouterInvalidResponseError) + isinstance(exc, (OpenRouterInvalidResponseError, RetryableProviderError)) or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "model output incomplete" in message @@ -903,6 +905,8 @@ def _lean_response_summary(feedback: ProofAttemptFeedback) -> str: if len(error) > 960: error = f"{error[:960]}..." if error: + if "timed out after" in error.lower() and "Advanced Settings" not in error: + error = f"{error} You can change this timeout in Advanced Settings." return f"Lean 4 response: {error} - proof not verified." return "Lean 4 response: proof not verified." diff --git a/backend/compiler/agents/writer_submitter.py b/backend/compiler/agents/writer_submitter.py index d7c3e4e..e763ee0 100644 --- a/backend/compiler/agents/writer_submitter.py +++ b/backend/compiler/agents/writer_submitter.py @@ -8,7 +8,7 @@ import uuid from typing import Optional, Dict, Any, List, Callable -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.models import CompilerSubmission, ContextPack from backend.shared.config import system_config, rag_config @@ -366,6 +366,8 @@ async def submit_outline_create(self) -> CompilerSubmission: except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"Failed to generate outline creation submission: {e}", exc_info=True) # Notify task completed (failed but still completed) @@ -519,6 +521,8 @@ async def submit_outline_update(self) -> Optional[CompilerSubmission]: except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"Failed to generate outline update submission: {e}", exc_info=True) # Notify task completed (failed but still completed) @@ -701,6 +705,8 @@ async def submit_construction( task_id=task_id, initial_prompt=prompt, ) + except RetryableProviderError: + raise except Exception as exc: # Any tool-loop failure falls back to the plain single-shot # path so construction still makes forward progress. @@ -840,6 +846,8 @@ async def submit_construction( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except ValueError: raise except RuntimeError as e: @@ -1003,6 +1011,8 @@ async def submit_review(self, review_focus: str = "general") -> Optional[Compile except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except ValueError: raise except RuntimeError as e: @@ -1323,6 +1333,8 @@ async def _parse_json_response_with_retry( else: logger.warning(f"Compiler writing submitter ({mode}): Retry returned empty response") + except RetryableProviderError: + raise except Exception as e: if "retry prompt exceeds context limit" in str(e).lower(): raise diff --git a/backend/compiler/core/compiler_coordinator.py b/backend/compiler/core/compiler_coordinator.py index 890295a..4f690c8 100644 --- a/backend/compiler/core/compiler_coordinator.py +++ b/backend/compiler/core/compiler_coordinator.py @@ -12,7 +12,7 @@ from backend.shared.config import system_config, rag_config from backend.shared.models import CompilerState, CompilerSubmission, CompilerValidationResult, WorkflowTask, ValidationResult, ModelConfig -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError, OpenRouterInvalidResponseError from backend.shared.brainstorm_proof_gate import BRAINSTORM_LEAN_PROOF_MARKER from backend.shared.free_model_manager import free_model_manager @@ -53,9 +53,11 @@ def _is_rigor_model_call_failure(exc: Exception) -> bool: """Return true for provider/config failures that must not become proof declines.""" + from backend.shared.api_client_manager import RetryableProviderError + message = str(exc or "").lower() return ( - isinstance(exc, OpenRouterInvalidResponseError) + isinstance(exc, (OpenRouterInvalidResponseError, RetryableProviderError)) or is_non_retryable_model_error(exc) or is_transient_model_call_error(exc) or "model output incomplete" in message @@ -879,6 +881,15 @@ async def _main_workflow(self) -> None: await asyncio.sleep(120) # Wait before retrying (all models exhausted) if self.is_running: self._main_task = asyncio.create_task(self._main_workflow()) + except RetryableProviderError as e: + logger.warning("Compiler paused for retryable provider failure: %s", e) + await api_client_manager.wait_for_retryable_provider_error( + e, + role_id=e.role_id or "compiler", + should_stop=lambda: not self.is_running, + ) + if self.is_running: + self._main_task = asyncio.create_task(self._main_workflow()) except ValueError as e: is_context_overflow = ( "mandatory full source context" in str(e).lower() diff --git a/backend/compiler/validation/compiler_validator.py b/backend/compiler/validation/compiler_validator.py index 7a10553..69d4e90 100644 --- a/backend/compiler/validation/compiler_validator.py +++ b/backend/compiler/validation/compiler_validator.py @@ -6,7 +6,7 @@ import uuid from typing import Optional, Dict, Any, Callable, Tuple -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.openrouter_client import FreeModelExhaustedError from backend.shared.models import CompilerSubmission, CompilerValidationResult from backend.shared.json_parser import parse_json, sanitize_model_output_for_retry_context @@ -557,6 +557,8 @@ async def _parse_json_with_retry( logger.warning(f"CompilerValidator: Retry parse failed: {retry_parse_error}") return self._fallback_parse(response) + except RetryableProviderError: + raise except Exception as retry_error: logger.error(f"CompilerValidator: Retry request failed - {retry_error}") return self._fallback_parse(response) @@ -1173,6 +1175,8 @@ async def validate_submission( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"Validation failed: {e}") if self.task_tracking_callback: @@ -1275,6 +1279,8 @@ async def validate_brainstorm_operation( except FreeModelExhaustedError: raise + except RetryableProviderError: + raise except Exception as e: logger.error(f"Brainstorm operation validation failed: {e}") if self.task_tracking_callback: diff --git a/backend/leanoj/core/leanoj_coordinator.py b/backend/leanoj/core/leanoj_coordinator.py index f1157cf..15c0f71 100644 --- a/backend/leanoj/core/leanoj_coordinator.py +++ b/backend/leanoj/core/leanoj_coordinator.py @@ -46,7 +46,7 @@ ) from backend.autonomous.memory.autonomous_api_logger import autonomous_api_logger from backend.autonomous.memory.proof_database import proof_database -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.brainstorm_proof_gate import is_lean_proof_submission, verify_brainstorm_proof_candidate from backend.shared.config import rag_config, system_config from backend.shared.context_overflow import ( @@ -4904,6 +4904,34 @@ async def _call_json( raise except LeanOJConfigurationError: raise + except RetryableProviderError as exc: + duration_ms = round((time.monotonic() - started) * 1000) + message = self._summarize_error(str(exc), limit=700) + logger.warning( + "Proof Solver model call paused for retryable provider failure (role=%s, task=%s, phase=%s, duration_ms=%s): %s", + role_id, + task_id, + call_payload["phase"], + duration_ms, + message, + ) + await self._broadcast( + "leanoj_model_call_failed", + { + **call_payload, + "duration_ms": duration_ms, + "retryable": True, + "reason": exc.reason or "transient_provider_error", + "message": message, + }, + ) + await api_client_manager.wait_for_retryable_provider_error( + exc, + role_id=exc.role_id or role_id, + should_stop=lambda: not self._running or self._stop_event.is_set(), + ) + current_prompt = prompt + continue except Exception as exc: duration_ms = round((time.monotonic() - started) * 1000) if is_provider_credit_pause_error(exc): diff --git a/backend/shared/api_client_manager.py b/backend/shared/api_client_manager.py index 5251c0d..2b3664d 100644 --- a/backend/shared/api_client_manager.py +++ b/backend/shared/api_client_manager.py @@ -34,6 +34,7 @@ from backend.shared.json_parser import sanitize_model_output_for_retry_context from backend.shared.log_redaction import redact_log_text from backend.shared.models import ModelConfig +from backend.shared.model_error_utils import is_transient_model_call_error from backend.shared.provider_notification_store import record_provider_notification from backend.shared.proof_search.assistant_coordinator import assistant_proof_search_coordinator from backend.shared.proof_search.assistant_models import AssistantTargetSnapshot @@ -107,7 +108,45 @@ def oauth_live_activity_error_message(error: Exception) -> str: return _cap_oauth_live_error_text(raw) -class OAuthProviderCooldownError(RuntimeError): +def _is_provider_context_length_error(error: Exception) -> bool: + """Return true when the provider rejected the request as too large.""" + detail = oauth_live_activity_error_message(error).lower() + raw = str(error or "").lower() + markers = ( + "context_length_exceeded", + "context length exceeded", + "context window", + "input exceeds", + "request too large", + "prompt is too long", + ) + return any(marker in detail or marker in raw for marker in markers) + + +class RetryableProviderError(RuntimeError): + """Raised when a provider failure should be retried by the workflow.""" + + def __init__( + self, + *, + provider: str, + provider_label: str, + role_id: str, + model: str, + reason: str, + message: str, + retry_after_seconds: Optional[int] = None, + ) -> None: + self.provider = provider + self.provider_label = provider_label + self.role_id = role_id + self.model = model + self.reason = reason + self.retry_after_seconds = retry_after_seconds + super().__init__(message) + + +class OAuthProviderCooldownError(RetryableProviderError): """Raised when an OAuth provider is cooling down until a provider reset time.""" def __init__( @@ -122,17 +161,21 @@ def __init__( plan_type: str = "", message: str = "", ) -> None: - self.provider = provider - self.provider_label = provider_label - self.role_id = role_id - self.model = model self.resets_at = resets_at self.resets_in_seconds = resets_in_seconds self.plan_type = plan_type base = message or f"{provider_label} usage limit reached" if resets_in_seconds is not None: base = f"{base}; resets in {resets_in_seconds} seconds" - super().__init__(base) + super().__init__( + provider=provider, + provider_label=provider_label, + role_id=role_id, + model=model, + reason="usage_limit_reached", + message=base, + retry_after_seconds=resets_in_seconds, + ) def _response_shape_for_logging(response: Any) -> str: @@ -252,6 +295,8 @@ def __init__(self): self._oauth_provider_cooldowns: Dict[str, Dict[str, Any]] = {} self._oauth_cooldown_notified: set[str] = set() self._oauth_cooldown_fallback_roles: set[str] = set() + self._oauth_error_notified: set[str] = set() + self._retryable_provider_backoff_state: Dict[str, int] = {} # Lock for thread-safe state updates self._state_lock = asyncio.Lock() @@ -284,6 +329,10 @@ async def _broadcast_unrecoverable_codex_error( error: Exception, ) -> None: """Notify the UI when a Codex role cannot recover through fallback.""" + notification_key = f"openai_codex_oauth:{role_id}:unrecoverable_codex_error:{model}" + if notification_key in self._oauth_error_notified: + return + self._oauth_error_notified.add(notification_key) payload = { "role_id": role_id, "model": model, @@ -314,6 +363,10 @@ async def _broadcast_unrecoverable_sakana_fugu_error( error: Exception, ) -> None: """Notify the UI when a Sakana Fugu role cannot recover through fallback.""" + notification_key = f"sakana_fugu:{role_id}:unrecoverable_sakana_fugu_error:{model}" + if notification_key in self._oauth_error_notified: + return + self._oauth_error_notified.add(notification_key) payload = { "role_id": role_id, "model": model, @@ -343,6 +396,10 @@ async def _broadcast_unrecoverable_xai_grok_error( error: Exception, ) -> None: """Notify the UI when a Grok OAuth role cannot recover through fallback.""" + notification_key = f"xai_grok_oauth:{role_id}:unrecoverable_xai_grok_error:{model}" + if notification_key in self._oauth_error_notified: + return + self._oauth_error_notified.add(notification_key) payload = { "role_id": role_id, "model": model, @@ -395,11 +452,106 @@ def get_provider_cooldown(self, provider: str) -> Optional[Dict[str, Any]]: def is_provider_cooling_down(self, provider: str) -> bool: return self.get_provider_cooldown(provider) is not None + @staticmethod + def _retryable_provider_key( + provider: str, + role_id: str, + model: str, + reason: str = "", + ) -> str: + return "|".join( + part.strip().lower() + for part in (provider or "unknown", role_id or "unknown", model or "unknown", reason or "retryable") + ) + + @staticmethod + async def _sleep_with_optional_stop( + seconds: int, + should_stop: Optional[Callable[[], bool]] = None, + ) -> None: + seconds = max(1, int(seconds)) + if should_stop is not None and should_stop(): + return + if seconds <= 1: + await asyncio.sleep(seconds) + return + deadline = time.monotonic() + seconds + while time.monotonic() < deadline: + if should_stop is not None and should_stop(): + return + await asyncio.sleep(min(1.0, max(0.0, deadline - time.monotonic()))) + + def _clear_retryable_provider_backoff(self, provider: str, role_id: str, model: str) -> None: + prefix = self._retryable_provider_key(provider, role_id, model).rsplit("|", 1)[0] + "|" + self._retryable_provider_backoff_state = { + key: value + for key, value in self._retryable_provider_backoff_state.items() + if not key.startswith(prefix) + } + + @staticmethod + def _as_retryable_provider_error( + *, + provider: str, + provider_label: str, + role_id: str, + model: str, + error: Exception, + ) -> RetryableProviderError: + message = ( + f"{provider_label} transient provider failure for role '{role_id}' " + f"after internal retries: {error}" + ) + return RetryableProviderError( + provider=provider, + provider_label=provider_label, + role_id=role_id, + model=model, + reason="transient_provider_error", + message=message, + ) + + async def wait_for_retryable_provider_error( + self, + error: RetryableProviderError, + *, + role_id: str = "", + should_stop: Optional[Callable[[], bool]] = None, + ) -> None: + """Apply one standard workflow-level backoff for retryable provider failures.""" + if isinstance(error, OAuthProviderCooldownError): + await self.wait_for_oauth_provider_cooldown( + error, + role_id=role_id, + should_stop=should_stop, + ) + return + + provider = str(error.provider or "").strip() or "unknown" + active_role = error.role_id or role_id or "unknown" + display_role = role_id or active_role + model = str(error.model or "").strip() + key = self._retryable_provider_key(provider, active_role, model, error.reason) + failure_count = self._retryable_provider_backoff_state.get(key, 0) + 1 + self._retryable_provider_backoff_state[key] = failure_count + wait_seconds = int(error.retry_after_seconds or min(60 * (2 ** (failure_count - 1)), 900)) + logger.warning( + "%s retryable provider failure for role '%s' (attempt %s after provider retries); " + "waiting %s seconds before retry: %s", + error.provider_label or provider, + display_role, + failure_count, + wait_seconds, + error, + ) + await self._sleep_with_optional_stop(wait_seconds, should_stop) + async def wait_for_oauth_provider_cooldown( self, error: OAuthProviderCooldownError, *, role_id: str = "", + should_stop: Optional[Callable[[], bool]] = None, ) -> None: """Sleep until an OAuth provider usage-limit cooldown expires.""" provider = str(error.provider or "").strip() or "openai_codex_oauth" @@ -418,7 +570,7 @@ async def wait_for_oauth_provider_cooldown( active_role, wait_seconds, ) - await asyncio.sleep(wait_seconds) + await self._sleep_with_optional_stop(wait_seconds, should_stop) def _mark_oauth_provider_cooldown( self, @@ -2054,6 +2206,7 @@ async def _generate_completion_once( # Track model usage for Tier 3 await self._track_model_usage(openrouter_model) + self._clear_retryable_provider_backoff("openrouter", role_id, openrouter_model) return result @@ -2283,6 +2436,14 @@ async def _generate_completion_once( f"OpenRouter error for role '{role_id}': {e}, " f"and no LM Studio fallback configured" ) + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="openrouter", + provider_label="OpenRouter", + role_id=role_id, + model=openrouter_model, + error=e, + ) from e raise if fallback_state == "sakana_fugu" and role_config: @@ -2354,6 +2515,7 @@ async def _generate_completion_once( ) await self._track_model_usage(sakana_model) + self._clear_retryable_provider_backoff("sakana_fugu", role_id, sakana_model) return result except SakanaFuguError as e: duration_ms = (time.time() - start_time) * 1000 @@ -2382,6 +2544,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="sakana_fugu", + provider_label="Sakana Fugu", + role_id=role_id, + model=sakana_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"Sakana Fugu context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_sakana_fugu_error( role_id=role_id, model=sakana_model, @@ -2418,6 +2592,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="sakana_fugu", + provider_label="Sakana Fugu", + role_id=role_id, + model=sakana_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"Sakana Fugu context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_sakana_fugu_error( role_id=role_id, model=sakana_model, @@ -2529,6 +2715,7 @@ async def _generate_completion_once( ) await self._track_model_usage(codex_model) + self._clear_retryable_provider_backoff("openai_codex_oauth", role_id, codex_model) return result except OAuthUsageLimitError as e: @@ -2602,6 +2789,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="openai_codex_oauth", + provider_label="OpenAI Codex", + role_id=role_id, + model=codex_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"OpenAI Codex context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_codex_error( role_id=role_id, model=codex_model, @@ -2638,6 +2837,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="openai_codex_oauth", + provider_label="OpenAI Codex", + role_id=role_id, + model=codex_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"OpenAI Codex context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_codex_error( role_id=role_id, model=codex_model, @@ -2716,6 +2927,7 @@ async def _generate_completion_once( ) await self._track_model_usage(xai_model) + self._clear_retryable_provider_backoff("xai_grok_oauth", role_id, xai_model) return result except XAIGrokError as e: @@ -2745,6 +2957,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="xai_grok_oauth", + provider_label="xAI Grok", + role_id=role_id, + model=xai_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"xAI Grok context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_xai_grok_error( role_id=role_id, model=xai_model, @@ -2781,6 +3005,18 @@ async def _generate_completion_once( ) model = role_config.lm_studio_fallback_id else: + if is_transient_model_call_error(e): + raise self._as_retryable_provider_error( + provider="xai_grok_oauth", + provider_label="xAI Grok", + role_id=role_id, + model=xai_model, + error=e, + ) from e + if _is_provider_context_length_error(e): + raise ValueError( + f"xAI Grok context_length_exceeded for role '{role_id}': {e}" + ) from e await self._broadcast_unrecoverable_xai_grok_error( role_id=role_id, model=xai_model, diff --git a/backend/shared/brainstorm_proof_gate.py b/backend/shared/brainstorm_proof_gate.py index 7c52ce8..43132b5 100644 --- a/backend/shared/brainstorm_proof_gate.py +++ b/backend/shared/brainstorm_proof_gate.py @@ -6,7 +6,7 @@ from typing import Any, Optional from backend.autonomous.prompts.proof_prompts import LEAN4_COMMON_PITFALLS -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.config import system_config from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -490,7 +490,7 @@ async def verify_brainstorm_proof_candidate( "reasoning": str(repaired.get("reasoning") or "").strip(), } except Exception as exc: - if is_non_retryable_model_error(exc): + if isinstance(exc, RetryableProviderError) or is_non_retryable_model_error(exc): raise logger.warning("Brainstorm proof repair attempt setup failed: %s", exc) current = { diff --git a/backend/shared/build_info.py b/backend/shared/build_info.py index 1fa7ab7..d8019dd 100644 --- a/backend/shared/build_info.py +++ b/backend/shared/build_info.py @@ -25,7 +25,7 @@ "version": "0.0.0-dev", "build_commit": "dev", "update_channel": "main", - "api_contract_version": "build5-v53", + "api_contract_version": "build5-v54", } _ENV_OVERRIDES = { diff --git a/backend/shared/config.py b/backend/shared/config.py index ddc806b..ac2c3e2 100644 --- a/backend/shared/config.py +++ b/backend/shared/config.py @@ -270,7 +270,7 @@ class SystemConfig(BaseSettings): validation_alias=AliasChoices("MOTO_LEAN4_WORKSPACE_DIR", "LEAN4_WORKSPACE_DIR"), ) lean4_proof_timeout: int = Field( - default=600, + default=900, validation_alias=AliasChoices("MOTO_LEAN4_PROOF_TIMEOUT", "LEAN4_PROOF_TIMEOUT"), ) lean4_lsp_idle_timeout: int = Field( diff --git a/backend/shared/json_parser.py b/backend/shared/json_parser.py index 4884a77..736d6d3 100644 --- a/backend/shared/json_parser.py +++ b/backend/shared/json_parser.py @@ -172,6 +172,22 @@ def _strip_control_tokens_outside_json_strings(content: str) -> str: return "".join(result) +def _strip_leading_private_channel_for_json(content: str) -> str: + """Keep the answer payload after private channel transcripts.""" + final_matches = _find_matches_outside_json_strings(_FINAL_CHANNEL_PATTERN, content) + if final_matches: + return content[final_matches[-1].end():].strip() + + if not _has_match_outside_json_strings(_PRIVATE_CHANNEL_PATTERN, content): + return content + + legacy_boundaries = _find_matches_outside_json_strings(_LEGACY_CHANNEL_BOUNDARY_PATTERN, content) + if legacy_boundaries: + return content[legacy_boundaries[-1].end():].strip() + + return content + + def _strip_leading_private_reasoning_blocks(content: str) -> str: """ Remove leading private reasoning transcript blocks without touching visible content. @@ -375,12 +391,13 @@ def sanitize_json_response(raw_content: str) -> str: content = '\n'.join(content_lines).strip() logger.debug(f"Stripped markdown code block wrapper") - # STEP 3: Strip control tokens that some models emit + # STEP 3: Strip private channel transcripts and control tokens that some models emit # Common patterns: <|channel|>...<|message|>, <|constrain|>JSON, etc. # Some models emit these BEFORE the JSON, some WITHIN the content # Strategy: Remove ALL control token patterns using regex original_content = content + content = _strip_leading_private_channel_for_json(content).strip() content = _strip_control_tokens_outside_json_strings(content).strip() if content != original_content: logger.debug( diff --git a/backend/shared/lean_proof_integrity.py b/backend/shared/lean_proof_integrity.py index c26ace1..4b10979 100644 --- a/backend/shared/lean_proof_integrity.py +++ b/backend/shared/lean_proof_integrity.py @@ -7,7 +7,7 @@ from typing import Optional from backend.autonomous.prompts.proof_prompts import build_proof_statement_alignment_prompt -from backend.shared.api_client_manager import api_client_manager +from backend.shared.api_client_manager import RetryableProviderError, api_client_manager from backend.shared.config import rag_config from backend.shared.json_parser import parse_json from backend.shared.response_extraction import extract_message_text @@ -243,7 +243,7 @@ async def validate_lean_statement_alignment( if not isinstance(data, dict): data = {} except Exception as exc: - if is_non_retryable_model_error(exc): + if isinstance(exc, RetryableProviderError) or is_non_retryable_model_error(exc): raise logger.warning("Lean statement alignment validation failed: %s", exc) return LeanProofIntegrityResult( diff --git a/backend/shared/model_error_utils.py b/backend/shared/model_error_utils.py index 093ab34..538de2a 100644 --- a/backend/shared/model_error_utils.py +++ b/backend/shared/model_error_utils.py @@ -4,6 +4,7 @@ from backend.shared.openrouter_client import ( CreditExhaustionError, FreeModelExhaustedError, + OpenRouterInvalidResponseError, OpenRouterPrivacyPolicyError, ) @@ -36,12 +37,20 @@ "connection timeout", "disconnect/reset before headers", "gateway timeout", + "http 500", + "http 502", + "http 503", + "http 504", "incomplete chunked read", "openai codex connection failed", "openai codex transient", + "openrouter connection failed", "peer closed connection", "readerror", "remoteprotocolerror", + "response missing 'choices'", + "sakana fugu connection failed", + "sakana fugu transient", "server_error", "service unavailable", "temporarily unavailable", @@ -55,10 +64,21 @@ _TRANSIENT_MODEL_PROVIDER_MARKERS = ( "codex", "grok", + "openrouter", + "sakana", "xai", ) _TRANSIENT_PROVIDER_ERROR_PREFIX = "TRANSIENT PROVIDER ERROR" +_TRANSIENT_INVALID_RESPONSE_BODY_MARKERS = ( + "bad gateway", + "cloudflare", + "gateway error", + "gateway timeout", + "service unavailable", + "temporarily unavailable", + "upstream connect error", +) def format_transient_provider_error(exc: Exception) -> str: @@ -81,6 +101,13 @@ def is_retryable_model_output_error(exc: Exception) -> bool: def is_transient_model_call_error(exc: Exception) -> bool: """Return true for provider/network failures that should not be treated as config errors.""" + if isinstance(exc, OpenRouterInvalidResponseError): + content_type = str(getattr(exc, "content_type", "") or "").lower() + body_preview = str(getattr(exc, "body_preview", "") or "").lower() + status_code = int(getattr(exc, "status_code", 0) or 0) + if status_code >= 500: + return True + return any(marker in body_preview for marker in _TRANSIENT_INVALID_RESPONSE_BODY_MARKERS) message = str(exc or "").lower() if not any(marker in message for marker in _TRANSIENT_MODEL_PROVIDER_MARKERS): return False diff --git a/backend/shared/proof_search/assistant_coordinator.py b/backend/shared/proof_search/assistant_coordinator.py index 60b0d22..8a3f4a8 100644 --- a/backend/shared/proof_search/assistant_coordinator.py +++ b/backend/shared/proof_search/assistant_coordinator.py @@ -451,9 +451,40 @@ async def _select_and_publish_assistant_pack(self, *, snapshot: AssistantTargetS try: selected_search_ids, selection_reasoning = await self._select_with_assistant(snapshot, shortlist, assistant_role_id=assistant_role_id, assistant_model_id=assistant_model_id, task_id=task_id) except Exception as exc: - warnings.append(f"Assistant LLM selection failed: {exc}") - await self._broadcast_event("assistant_proof_pack_warning", {"target_hash": snapshot.target_hash, "workflow_mode": snapshot.workflow_mode, "target_kind": snapshot.target_kind, "workflow_phase": snapshot.workflow_phase, "source_type": snapshot.source_type, "source_id": snapshot.source_id, "warnings": warnings[-3:], "assistant_role_id": assistant_role_id, "assistant_model_id": assistant_model_id, "candidate_count": candidate_count, "shortlist_count": len(shortlist)}) - await self._publish_pack(snapshot, [], warnings=warnings, selection_mode="unavailable", assistant_role_id=assistant_role_id, assistant_model_id=assistant_model_id, candidate_count=candidate_count, shortlist_count=len(shortlist), selection_reasoning="Assistant LLM selection failed.") + error_message = _compact_for_assistant_selection(str(exc), 240) + failure_warning = f"Assistant LLM selection failed: {error_message}" + await self._broadcast_event( + "assistant_proof_pack_failed", + { + "target_hash": snapshot.target_hash, + "workflow_mode": snapshot.workflow_mode, + "target_kind": snapshot.target_kind, + "workflow_phase": snapshot.workflow_phase, + "source_type": snapshot.source_type, + "source_id": snapshot.source_id, + "assistant_role_id": assistant_role_id, + "assistant_model_id": assistant_model_id, + "candidate_count": candidate_count, + "shortlist_count": len(shortlist), + "reason": "assistant_llm_selection_failed", + "error_message": error_message, + }, + ) + latest_pack = self.get_latest_pack(snapshot.target_hash) + if latest_pack and latest_pack.results: + return + await self._publish_pack( + snapshot, + [], + warnings=[*warnings, failure_warning], + selection_mode="unavailable", + assistant_role_id=assistant_role_id, + assistant_model_id=assistant_model_id, + candidate_count=candidate_count, + shortlist_count=len(shortlist), + selection_reasoning="Assistant LLM selection failed; no proof supports were published.", + broadcast_update=False, + ) return selected_supports = _supports_for_selected_ids(shortlist, selected_search_ids) @@ -506,7 +537,7 @@ async def _select_with_assistant(self, snapshot: AssistantTargetSnapshot, shortl reasoning = _compact_for_assistant_selection(reasoning, 300) return clean_ids[:_ASSISTANT_FINAL_PACK_LIMIT], reasoning - async def _publish_pack(self, snapshot: AssistantTargetSnapshot, supports: list[AssistantProofSupport], *, warnings: list[str], selection_mode: str, assistant_role_id: str = "", assistant_model_id: str = "", candidate_count: int, shortlist_count: int, selection_reasoning: str = "") -> None: + async def _publish_pack(self, snapshot: AssistantTargetSnapshot, supports: list[AssistantProofSupport], *, warnings: list[str], selection_mode: str, assistant_role_id: str = "", assistant_model_id: str = "", candidate_count: int, shortlist_count: int, selection_reasoning: str = "", broadcast_update: bool = True) -> None: pack = AssistantProofPack(workflow_mode=snapshot.workflow_mode, target_kind=snapshot.target_kind, target_hash=snapshot.target_hash, query_summary=_compact_query_summary(snapshot), results=supports[:_ASSISTANT_FINAL_PACK_LIMIT], warnings=warnings, selection_mode=selection_mode, assistant_role_id=assistant_role_id, assistant_model_id=assistant_model_id, candidate_count=candidate_count, shortlist_count=shortlist_count, selection_reasoning=selection_reasoning) source_counts: dict[str, int] = {} for support in pack.results: @@ -532,7 +563,8 @@ async def _publish_pack(self, snapshot: AssistantTargetSnapshot, supports: list[ self._goal_target_hashes[goal_hash] = snapshot.target_hash await asyncio.to_thread(self._cache.record_pack, snapshot=snapshot, pack=pack, selected_search_ids=[support.search_id for support in pack.results]) await self._persist_pack(pack) - await self._broadcast_event("assistant_proof_pack_updated", {"target_hash": pack.target_hash, "workflow_mode": pack.workflow_mode, "target_kind": pack.target_kind, "result_count": len(pack.results), "local_result_count": sum(count for corpus, count in source_counts.items() if corpus != "syntheticlib4"), "syntheticlib4_result_count": source_counts.get("syntheticlib4", 0), "source_counts": source_counts, "max_result_count": _ASSISTANT_FINAL_PACK_LIMIT, "workflow_phase": snapshot.workflow_phase, "source_type": snapshot.source_type, "source_id": snapshot.source_id, "warnings": pack.warnings[:3], "selection_mode": pack.selection_mode, "assistant_role_id": pack.assistant_role_id, "assistant_model_id": pack.assistant_model_id, "candidate_count": pack.candidate_count, "shortlist_count": pack.shortlist_count}) + if broadcast_update: + await self._broadcast_event("assistant_proof_pack_updated", {"target_hash": pack.target_hash, "workflow_mode": pack.workflow_mode, "target_kind": pack.target_kind, "result_count": len(pack.results), "local_result_count": sum(count for corpus, count in source_counts.items() if corpus != "syntheticlib4"), "syntheticlib4_result_count": source_counts.get("syntheticlib4", 0), "source_counts": source_counts, "max_result_count": _ASSISTANT_FINAL_PACK_LIMIT, "workflow_phase": snapshot.workflow_phase, "source_type": snapshot.source_type, "source_id": snapshot.source_id, "warnings": pack.warnings[:3], "selection_mode": pack.selection_mode, "assistant_role_id": pack.assistant_role_id, "assistant_model_id": pack.assistant_model_id, "candidate_count": pack.candidate_count, "shortlist_count": pack.shortlist_count}) await self._record_cooldown_outcome(snapshot, pack) def _on_task_done(self, target_hash: str, task: asyncio.Task) -> None: @@ -697,13 +729,28 @@ def _extract_valid_selected_search_ids(payload: dict[str, Any], shortlist: list[ if not clean_ids: return [] valid_ids = {support.search_id for support in shortlist} - invalid_ids = [search_id for search_id in clean_ids if search_id not in valid_ids] + proof_id_to_search_ids: dict[str, list[str]] = {} + for support in shortlist: + proof_id = str(support.proof_id or "").strip() + if proof_id: + proof_id_to_search_ids.setdefault(proof_id, []).append(support.search_id) + normalized_ids: list[str] = [] + invalid_ids: list[str] = [] + for search_id in clean_ids: + if search_id in valid_ids: + normalized_ids.append(search_id) + continue + proof_id_matches = proof_id_to_search_ids.get(search_id, []) + if len(proof_id_matches) == 1: + normalized_ids.append(proof_id_matches[0]) + continue + invalid_ids.append(search_id) if invalid_ids: preview = ", ".join(invalid_ids[:3]) raise _AssistantSelectionOutputError( f"Assistant selected IDs outside the candidate shortlist: {preview}" ) - return selected_ids + return normalized_ids def _assistant_selection_max_tokens(configured_max_tokens: int | None) -> int: @@ -751,8 +798,8 @@ def _assistant_selection_prompt( target = _compact_for_assistant_selection(snapshot.search_text(), 2400) return ( f"{prefix}\n" - 'Required schema: {"selected_search_ids":[""],"reasoning":"<=160 chars"}\n' - f"Rules: select at most {_ASSISTANT_FINAL_PACK_LIMIT}; use only exact listed IDs; use [] if no listed proof support is genuinely useful for the target; no markdown.\n\n" + 'Required schema: {"selected_search_ids":[""],"reasoning":"<=160 chars"}\n' + f"Rules: select at most {_ASSISTANT_FINAL_PACK_LIMIT}; copy only exact SELECT_ID values; do not return proof_id/display IDs; use [] if no listed proof support is genuinely useful for the target; no markdown.\n\n" f"TARGET:\n{target}\n\n" f"CANDIDATES:\n{ids}\n" ) @@ -761,7 +808,11 @@ def _assistant_selection_prompt( def _format_assistant_candidate(support: AssistantProofSupport) -> str: label = support.theorem_name or support.theorem_statement or support.proof_id statement = "" if label == support.theorem_statement else support.theorem_statement - parts = [f"- id: {support.search_id}", f" label: {_compact_for_assistant_selection(label, 180)}"] + parts = [ + f"- SELECT_ID: {support.search_id}", + f" proof_id: {support.proof_id}", + f" label: {_compact_for_assistant_selection(label, 180)}", + ] if statement: parts.append(f" statement: {_compact_for_assistant_selection(statement, 220)}") return "\n".join(parts) diff --git a/backend/shared/runtime_settings.py b/backend/shared/runtime_settings.py index 432f5c0..bd2979e 100644 --- a/backend/shared/runtime_settings.py +++ b/backend/shared/runtime_settings.py @@ -37,6 +37,8 @@ class RuntimeSettingsError(RuntimeError): "smt_timeout": (1, 600), } +_LEGACY_DEFAULT_LEAN4_PROOF_TIMEOUT = 600 + _CONNECTIVITY_BOOL_FIELDS = { "syntheticlib4_enabled", "agent_conversation_memory_enabled", @@ -190,12 +192,19 @@ def apply_persisted_runtime_settings() -> None: ) for field, (minimum, maximum) in _PROOF_INT_FIELDS.items(): if field in proof_settings: + default = int(getattr(system_config, field)) + if ( + field == "lean4_proof_timeout" + and default != _LEGACY_DEFAULT_LEAN4_PROOF_TIMEOUT + and str(proof_settings[field]).strip() == str(_LEGACY_DEFAULT_LEAN4_PROOF_TIMEOUT) + ): + proof_settings[field] = default setattr( system_config, field, _coerce_int( proof_settings[field], - int(getattr(system_config, field)), + default, minimum, maximum, ), diff --git a/frontend/package-lock.json b/frontend/package-lock.json index 0a91f77..6f893ce 100644 --- a/frontend/package-lock.json +++ b/frontend/package-lock.json @@ -1,12 +1,12 @@ { "name": "asi-aggregator-frontend", - "version": "1.1.01", + "version": "1.1.02", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "asi-aggregator-frontend", - "version": "1.1.01", + "version": "1.1.02", "license": "MIT", "dependencies": { "dompurify": "^3.2.4", diff --git a/frontend/package.json b/frontend/package.json index d3a8a8f..aa028fa 100644 --- a/frontend/package.json +++ b/frontend/package.json @@ -1,6 +1,6 @@ { "name": "asi-aggregator-frontend", - "version": "1.1.01", + "version": "1.1.02", "description": "Frontend UI for MOTO S.T.E.M. Mathematics Variant - Autonomous ASI Research System for Novel S.T.E.M. Mathematical Paper Generation", "author": "Intrafere LLC", "license": "MIT", diff --git a/frontend/src/App.jsx b/frontend/src/App.jsx index 7c23ab3..7805462 100644 --- a/frontend/src/App.jsx +++ b/frontend/src/App.jsx @@ -68,6 +68,7 @@ import { CLOUD_ACCESS_PROVIDERS, isCloudAccessProvider } from './utils/oauthProv import { formatContextOverflowActivityMessage, formatAssistantProofPackEventMessage, + buildAutonomousProofProviderPauseActivity, buildRejectionFeedbackNoticeActivity, hasRecentAssistantProofPackDuplicate, shouldAddRejectionFeedbackNotice, @@ -653,6 +654,7 @@ function App() { const [hasOpenRouterKey, setHasOpenRouterKey] = useState(null); const [hasCloudAccess, setHasCloudAccess] = useState(null); const [capabilities, setCapabilities] = useState(DEFAULT_CAPABILITIES); + const [credentialStatusRefreshToken, setCredentialStatusRefreshToken] = useState(0); // Track if any workflow is running (for WorkflowPanel visibility) const [anyWorkflowRunning, setAnyWorkflowRunning] = useState(false); @@ -1514,9 +1516,18 @@ function App() { return `Proof round ${round}/${maxRounds}`; }; const proofLeanResponse = (data = {}) => { - if (data.lean_response) return data.lean_response; + if (data.lean_response) { + let response = data.lean_response; + if (/timed out after/i.test(response) && !/Advanced Settings/.test(response)) { + response = `${response} You can change this timeout in Advanced Settings.`; + } + return response; + } if (data.proof_verified === true) return 'Lean 4 response: proof verified.'; - const error = formatReason(data.error_summary || data.error_output || data.reason || '', 960); + let error = formatReason(data.error_summary || data.error_output || data.reason || '', 960); + if (/timed out after/i.test(error) && !/Advanced Settings/.test(error)) { + error = `${error} You can change this timeout in Advanced Settings.`; + } return error ? `Lean 4 response: ${error} - proof not verified.` : 'Lean 4 response: proof not verified.'; }; const formatProofNoveltyTier = (tier) => { @@ -1865,7 +1876,7 @@ function App() { const handleAutonomousAssistantEvent = (eventName, data) => { const workflowMode = String(data.workflow_mode || ''); - if (!['autonomous', 'aggregator', 'compiler'].includes(workflowMode)) { + if (workflowMode !== 'autonomous') { return; } if (!autonomousRunningRef.current) { @@ -1881,6 +1892,9 @@ function App() { unsubscribers.push(websocket.on('assistant_proof_pack_updated', (data) => { handleAutonomousAssistantEvent('assistant_proof_pack_updated', data); })); + unsubscribers.push(websocket.on('assistant_proof_pack_failed', (data) => { + handleAutonomousAssistantEvent('assistant_proof_pack_failed', data); + })); unsubscribers.push(websocket.on('proof_check_started', (data) => { setProofRefreshToken((prev) => prev + 1); @@ -2485,13 +2499,17 @@ function App() { })); unsubscribers.push(websocket.on('autonomous_proof_provider_paused', (data) => { - console.warn('Autonomous proof verification paused for provider credits:', data); + const { isCreditPause, message } = buildAutonomousProofProviderPauseActivity(data); + console.warn('Autonomous proof verification paused for provider retry:', data); addActivity({ event: 'autonomous_proof_provider_paused', timestamp: getTimestamp(data), - message: `Autonomous proof verification paused until OpenRouter credits are reset: ${data.message || data.source_id || 'provider credits exhausted'}`, + message, ...data }); + if (!isCreditPause) { + return; + } setCreditExhaustionNotifications(prev => { const roleId = `Autonomous Proof (${data.source_id || data.source_type || 'checkpoint'})`; if (prev.some(n => n.role_id === roleId && n.reason === 'provider_paused')) return prev; @@ -2738,12 +2756,21 @@ function App() { }; const leanOJLeanResponse = (data = {}) => { const attempt = data.attempt || {}; - if (data.lean_response) return data.lean_response; + if (data.lean_response) { + let response = data.lean_response; + if (/timed out after/i.test(response) && !/Advanced Settings/.test(response)) { + response = `${response} You can change this timeout in Advanced Settings.`; + } + return response; + } if (data.proof_verified === true || attempt.success === true) return 'Lean 4 response: proof verified.'; - const error = summarizeLeanOJText( + let error = summarizeLeanOJText( attempt.error_output || data.error_summary || data.error_output || data.reason || data.message || '', 960 ); + if (/timed out after/i.test(error) && !/Advanced Settings/.test(error)) { + error = `${error} You can change this timeout in Advanced Settings.`; + } return error ? `Lean 4 response: ${error} - proof not verified.` : 'Lean 4 response: proof not verified.'; }; const formatLeanOJNoveltyTier = (tier) => { @@ -2804,6 +2831,10 @@ function App() { if (data.workflow_mode !== 'leanoj') return; addLeanOJActivity('assistant_proof_pack_updated', data, formatAssistantProofPackEventMessage('assistant_proof_pack_updated', data)); }], + ['assistant_proof_pack_failed', (data) => { + if (data.workflow_mode !== 'leanoj') return; + addLeanOJActivity('assistant_proof_pack_failed', data, formatAssistantProofPackEventMessage('assistant_proof_pack_failed', data)); + }], ['leanoj_stopped', (data) => { setLeanojRunning(false); setAnyWorkflowRunning(false); @@ -3537,6 +3568,9 @@ function App() { }; const handleCloudAccessChanged = async (configured, provider = 'cloud', options = {}) => { + setCredentialStatusRefreshToken((token) => token + 1); + refreshConnectivityStatus(); + if (isCloudAccessProvider(provider) && options.modelsReady === false) { setHasCloudAccess(Boolean(hasOpenRouterKey)); return; @@ -3574,7 +3608,21 @@ function App() { setHasOpenRouterKey(true); setHasCloudAccess(true); console.log('OpenRouter API key set successfully'); + setCredentialStatusRefreshToken((token) => token + 1); + refreshConnectivityStatus(); + }; + + const handleOpenRouterKeyCleared = async () => { + setHasOpenRouterKey(false); + setCredentialStatusRefreshToken((token) => token + 1); refreshConnectivityStatus(); + + try { + const cloudStatus = await cloudAccessAPI.getStatus(); + setHasCloudAccess(hasConfiguredCloudAccessProvider(cloudStatus)); + } catch { + setHasCloudAccess(false); + } }; const handleConnectivityToggle = async (toggles) => { @@ -4083,6 +4131,7 @@ function App() { models={models} capabilities={capabilities} connectivityStatus={connectivityStatus} + credentialStatusRefreshToken={credentialStatusRefreshToken} isRunning={autonomousRunning} developerModeEnabled={developerModeEnabled} /> @@ -4094,6 +4143,7 @@ function App() { onSettingsChange={setLeanojSettings} capabilities={capabilities} connectivityStatus={connectivityStatus} + credentialStatusRefreshToken={credentialStatusRefreshToken} isRunning={leanojRunning} developerModeEnabled={developerModeEnabled} /> @@ -4105,6 +4155,7 @@ function App() { setConfig={setConfig} capabilities={capabilities} connectivityStatus={connectivityStatus} + credentialStatusRefreshToken={credentialStatusRefreshToken} developerModeEnabled={developerModeEnabled} /> )} @@ -4113,6 +4164,7 @@ function App() { )} @@ -4213,6 +4265,7 @@ function App() { isOpen={showOpenRouterKeyModal} onClose={handleCloseOpenRouterKeyModal} onKeySet={handleOpenRouterKeySet} + onKeyCleared={handleOpenRouterKeyCleared} onCloudAccessChanged={handleCloudAccessChanged} reason={openRouterKeyReason} capabilities={capabilities} diff --git a/frontend/src/components/OpenRouterApiKeyModal.jsx b/frontend/src/components/OpenRouterApiKeyModal.jsx index 0539163..a0e0a1f 100644 --- a/frontend/src/components/OpenRouterApiKeyModal.jsx +++ b/frontend/src/components/OpenRouterApiKeyModal.jsx @@ -22,6 +22,7 @@ export default function OpenRouterApiKeyModal({ isOpen, onClose, onKeySet, + onKeyCleared, onCloudAccessChanged, reason = 'setup', capabilities, @@ -482,6 +483,9 @@ export default function OpenRouterApiKeyModal({ setTestResult(null); setError(''); setHasStoredKey(false); + if (onKeyCleared) { + await onKeyCleared(); + } } catch (err) { setError(err.message || 'Failed to clear API key'); } diff --git a/frontend/src/components/WorkflowPanel.css b/frontend/src/components/WorkflowPanel.css index fc3cb5f..dc3de03 100644 --- a/frontend/src/components/WorkflowPanel.css +++ b/frontend/src/components/WorkflowPanel.css @@ -3,7 +3,7 @@ right: 0; top: 0; height: 100vh; - width: 320px; + width: min(320px, 85vw); background: var(--surface-1); border-left: 1px solid var(--border-subtle); display: flex; @@ -17,6 +17,16 @@ width: 50px; } +@media (max-width: 480px) { + .workflow-panel { + width: min(300px, 88vw); + } + + .workflow-panel.collapsed { + width: 44px; + } +} + .workflow-header { display: flex; justify-content: space-between; diff --git a/frontend/src/components/aggregator/AggregatorLogs.jsx b/frontend/src/components/aggregator/AggregatorLogs.jsx index 0c6c010..808f37d 100644 --- a/frontend/src/components/aggregator/AggregatorLogs.jsx +++ b/frontend/src/components/aggregator/AggregatorLogs.jsx @@ -34,6 +34,7 @@ const MANUAL_PROOF_EVENTS = [ ]; const ASSISTANT_MEMORY_EVENTS = [ 'assistant_proof_pack_updated', + 'assistant_proof_pack_failed', ]; const HIDDEN_AGGREGATOR_ACTIVITY_EVENTS = new Set(['new_submission']); @@ -111,12 +112,19 @@ const proofTargetLabel = (data = {}, fallback = 'candidate') => ( const leanProofResponse = (data = {}) => { if (data.lean_response) { - return compactProofText(data.lean_response); + let response = compactProofText(data.lean_response); + if (/timed out after/i.test(response) && !/Advanced Settings/.test(response)) { + response = `${response} You can change this timeout in Advanced Settings.`; + } + return response; } if (data.proof_verified === true) { return 'Lean 4 response: proof verified.'; } - const error = compactProofText(data.error_summary || data.error_output || data.reason, 960); + let error = compactProofText(data.error_summary || data.error_output || data.reason, 960); + if (/timed out after/i.test(error) && !/Advanced Settings/.test(error)) { + error = `${error} You can change this timeout in Advanced Settings.`; + } return error ? `Lean 4 response: ${error} - proof not verified.` : ''; }; @@ -191,6 +199,7 @@ export default function AggregatorLogs() { websocket.on('context_overflow_error', handleContextOverflow), websocket.on('hung_connection_alert', handleHungConnectionAlert), websocket.on('assistant_proof_pack_updated', (data) => handleAssistantProofPackEvent('assistant_proof_pack_updated', data)), + websocket.on('assistant_proof_pack_failed', (data) => handleAssistantProofPackEvent('assistant_proof_pack_failed', data)), ...MANUAL_PROOF_EVENTS.map((eventName) => ( websocket.on(eventName, (data) => handleManualProofEvent(eventName, data)) )), diff --git a/frontend/src/components/aggregator/AggregatorSettings.jsx b/frontend/src/components/aggregator/AggregatorSettings.jsx index a118713..868de65 100644 --- a/frontend/src/components/aggregator/AggregatorSettings.jsx +++ b/frontend/src/components/aggregator/AggregatorSettings.jsx @@ -19,6 +19,7 @@ import { OPENROUTER_REASONING_EFFORT_OPTIONS, SAKANA_FUGU_REASONING_EFFORT_OPTIONS, } from '../../utils/openRouterSelection'; +import { refreshCredentialProviderState } from '../../utils/credentialProviderRefresh'; import { chooseCloudAccessProvider, getConfiguredCloudAccessProviders, @@ -251,6 +252,7 @@ export default function AggregatorSettings({ setConfig, capabilities, connectivityStatus, + credentialStatusRefreshToken = 0, developerModeEnabled = false, }) { const [lmStudioModels, setLmStudioModels] = useState([]); @@ -423,6 +425,37 @@ export default function AggregatorSettings({ checkOpenRouterKey(); }, [lmStudioEnabled]); + useEffect(() => { + if (credentialStatusRefreshToken === 0) { + return; + } + + let isCurrent = true; + refreshCredentialProviderState({ + freeOnly, + openAICodexOauthAvailable, + xaiGrokOauthAvailable, + sakanaFuguAvailable, + setHasOpenRouterKey, + setOpenRouterModels, + setLoadingOpenRouter, + setHasOpenAICodexLogin, + setOpenAICodexModels, + setOpenAICodexModelError, + setHasXAIGrokLogin, + setXaiGrokModels, + setXaiGrokModelError, + setHasSakanaFuguKey, + setSakanaFuguModels, + setSakanaFuguModelError, + shouldApply: () => isCurrent, + logContext: 'Aggregator settings', + }); + return () => { + isCurrent = false; + }; + }, [credentialStatusRefreshToken]); + useEffect(() => { if (lmStudioEnabled) { return; @@ -512,7 +545,6 @@ export default function AggregatorSettings({ } } catch (err) { console.error('Failed to check OpenAI Codex login status:', err); - setHasOpenAICodexLogin(false); setOpenAICodexModelError(`OpenAI Codex OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -532,7 +564,6 @@ export default function AggregatorSettings({ } } catch (err) { console.error('Failed to check xAI Grok login status:', err); - setHasXAIGrokLogin(false); setXaiGrokModelError(`xAI Grok OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -552,7 +583,6 @@ export default function AggregatorSettings({ } } catch (err) { console.error('Failed to check Sakana Fugu API key status:', err); - setHasSakanaFuguKey(false); setSakanaFuguModelError(`Sakana Fugu status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -585,7 +615,7 @@ export default function AggregatorSettings({ const result = await cloudAccessAPI.getOpenAICodexModels(); const models = result.models || []; setOpenAICodexModels(models); - setHasOpenAICodexLogin(models.length > 0); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(models.length > 0 ? '' : 'OpenAI Codex OAuth is connected, but no Codex models were returned. Reconnect OAuth or check account access.' @@ -593,7 +623,7 @@ export default function AggregatorSettings({ } catch (err) { console.error('Failed to fetch OpenAI Codex models:', err); setOpenAICodexModels([]); - setHasOpenAICodexLogin(false); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(`OpenAI Codex OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -609,7 +639,7 @@ export default function AggregatorSettings({ const result = await cloudAccessAPI.getXAIGrokModels(); const models = result.models || []; setXaiGrokModels(models); - setHasXAIGrokLogin(models.length > 0); + setHasXAIGrokLogin(true); setXaiGrokModelError(models.length > 0 ? '' : 'xAI Grok OAuth is connected, but no Grok models were returned. Reconnect OAuth or check account access.' @@ -617,7 +647,7 @@ export default function AggregatorSettings({ } catch (err) { console.error('Failed to fetch xAI Grok models:', err); setXaiGrokModels([]); - setHasXAIGrokLogin(false); + setHasXAIGrokLogin(true); setXaiGrokModelError(`xAI Grok OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -633,7 +663,7 @@ export default function AggregatorSettings({ const result = await cloudAccessAPI.getSakanaFuguModels(); const models = result.models || []; setSakanaFuguModels(models); - setHasSakanaFuguKey(models.length > 0); + setHasSakanaFuguKey(true); setSakanaFuguModelError(models.length > 0 ? '' : 'Sakana Fugu API key is saved, but no Fugu models were returned. Check your Sakana subscription access.' @@ -641,7 +671,7 @@ export default function AggregatorSettings({ } catch (err) { console.error('Failed to fetch Sakana Fugu models:', err); setSakanaFuguModels([]); - setHasSakanaFuguKey(false); + setHasSakanaFuguKey(true); setSakanaFuguModelError(`Sakana Fugu API key is saved, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; diff --git a/frontend/src/components/autonomous/AutonomousResearchInterface.jsx b/frontend/src/components/autonomous/AutonomousResearchInterface.jsx index 923405d..8c20e3e 100644 --- a/frontend/src/components/autonomous/AutonomousResearchInterface.jsx +++ b/frontend/src/components/autonomous/AutonomousResearchInterface.jsx @@ -207,7 +207,7 @@ const AutonomousResearchInterface = ({ const status = await api.getProofStatus(); const updatedStatus = await api.updateProofSettings({ enabled, - timeout: status.lean4_proof_timeout ?? 600, + timeout: status.lean4_proof_timeout ?? 900, lean4_lsp_enabled: Boolean(status.lean4_lsp_enabled), lean4_lsp_idle_timeout: status.lean4_lsp_idle_timeout ?? 600, max_parallel_candidates: status.proof_max_parallel_candidates ?? 6, @@ -532,7 +532,7 @@ const AutonomousResearchInterface = ({ Skip AI Autonomy - We recommend at minimum 5 ACCEPTED submissions. A very low acceptance rate is normal because the validator is seeking novel solutions. Higher parameter models may improve acceptance, though optimizing for both speed and knowledge can also work well. Validator feedback on rejections helps avoid rejection loops. Harder problems may require hundreds or more rejections before a single acceptance, and the first acceptance often takes the longest. View brainstorms in the brainstorm tab. + We recommend at minimum 7 ACCEPTED submissions. A very low acceptance rate is normal because the validator is seeking novel solutions. Higher parameter models may improve acceptance, though optimizing for both speed and knowledge can also work well. Validator feedback on rejections helps avoid rejection loops. Harder problems may require hundreds or more rejections before a single acceptance, and the first acceptance often takes the longest. View brainstorms in the brainstorm tab. )} diff --git a/frontend/src/components/autonomous/AutonomousResearchLogs.jsx b/frontend/src/components/autonomous/AutonomousResearchLogs.jsx index d69ec6f..fef769b 100644 --- a/frontend/src/components/autonomous/AutonomousResearchLogs.jsx +++ b/frontend/src/components/autonomous/AutonomousResearchLogs.jsx @@ -89,9 +89,18 @@ const AutonomousResearchLogs = ({ stats, events }) => { return `Proof round ${round}/${maxRounds}`; }; const proofLeanResponse = () => { - if (data.lean_response) return data.lean_response; + if (data.lean_response) { + let response = data.lean_response; + if (/timed out after/i.test(response) && !/Advanced Settings/.test(response)) { + response = `${response} You can change this timeout in Advanced Settings.`; + } + return response; + } if (data.proof_verified === true) return 'Lean 4 response: proof verified.'; - const error = data.error_summary || data.error_output || data.reason || ''; + let error = data.error_summary || data.error_output || data.reason || ''; + if (/timed out after/i.test(error) && !/Advanced Settings/.test(error)) { + error = `${error} You can change this timeout in Advanced Settings.`; + } return error ? `Lean 4 response: ${error} - proof not verified.` : 'Lean 4 response: proof not verified.'; }; const formatProofNoveltyTier = (tier) => { diff --git a/frontend/src/components/autonomous/AutonomousResearchSettings.jsx b/frontend/src/components/autonomous/AutonomousResearchSettings.jsx index 6bbef73..803baa5 100644 --- a/frontend/src/components/autonomous/AutonomousResearchSettings.jsx +++ b/frontend/src/components/autonomous/AutonomousResearchSettings.jsx @@ -25,6 +25,7 @@ import { OPENROUTER_REASONING_EFFORT_OPTIONS, SAKANA_FUGU_REASONING_EFFORT_OPTIONS, } from '../../utils/openRouterSelection'; +import { refreshCredentialProviderState } from '../../utils/credentialProviderRefresh'; import { chooseCloudAccessProvider, getConfiguredCloudAccessProviders, @@ -421,6 +422,7 @@ const AutonomousResearchSettings = ({ models, capabilities, connectivityStatus, + credentialStatusRefreshToken = 0, isRunning, developerModeEnabled = false, }) => { @@ -458,7 +460,7 @@ const AutonomousResearchSettings = ({ const [proofStatus, setProofStatus] = useState(null); const [proofSettingsEnabled, setProofSettingsEnabled] = useState(false); - const [proofSettingsTimeout, setProofSettingsTimeout] = useState('600'); + const [proofSettingsTimeout, setProofSettingsTimeout] = useState('900'); const [proofSettingsLspEnabled, setProofSettingsLspEnabled] = useState(false); const [proofSettingsLspIdleTimeout, setProofSettingsLspIdleTimeout] = useState('600'); const [proofSettingsMaxParallelCandidates, setProofSettingsMaxParallelCandidates] = useState('6'); @@ -684,7 +686,6 @@ const AutonomousResearchSettings = ({ } } catch (err) { console.error('Failed to check OpenAI Codex login:', err); - setHasOpenAICodexLogin(false); setOpenAICodexModelError(`OpenAI Codex OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -704,7 +705,6 @@ const AutonomousResearchSettings = ({ } } catch (err) { console.error('Failed to check xAI Grok login:', err); - setHasXAIGrokLogin(false); setXaiGrokModelError(`xAI Grok OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -724,7 +724,6 @@ const AutonomousResearchSettings = ({ } } catch (err) { console.error('Failed to check Sakana Fugu API key:', err); - setHasSakanaFuguKey(false); setSakanaFuguModelError(`Sakana Fugu status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -761,7 +760,7 @@ const AutonomousResearchSettings = ({ const status = await autonomousAPI.getProofStatus(); setProofStatus(status); setProofSettingsEnabled(Boolean(status.lean4_enabled)); - setProofSettingsTimeout(String(status.lean4_proof_timeout ?? 600)); + setProofSettingsTimeout(String(status.lean4_proof_timeout ?? 900)); setProofSettingsLspEnabled(Boolean(status.lean4_lsp_enabled)); setProofSettingsLspIdleTimeout(String(status.lean4_lsp_idle_timeout ?? 600)); setProofSettingsMaxParallelCandidates(String(status.proof_max_parallel_candidates ?? 6)); @@ -964,7 +963,7 @@ const AutonomousResearchSettings = ({ const result = await cloudAccessAPI.getOpenAICodexModels(); const models = result.models || []; setOpenAICodexModels(models); - setHasOpenAICodexLogin(models.length > 0); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(models.length > 0 ? '' : 'OpenAI Codex OAuth is connected, but no Codex models were returned. Reconnect OAuth or check account access.' @@ -972,7 +971,7 @@ const AutonomousResearchSettings = ({ } catch (err) { console.error('Failed to fetch OpenAI Codex models:', err); setOpenAICodexModels([]); - setHasOpenAICodexLogin(false); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(`OpenAI Codex OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -988,7 +987,7 @@ const AutonomousResearchSettings = ({ const result = await cloudAccessAPI.getXAIGrokModels(); const models = result.models || []; setXaiGrokModels(models); - setHasXAIGrokLogin(models.length > 0); + setHasXAIGrokLogin(true); setXaiGrokModelError(models.length > 0 ? '' : 'xAI Grok OAuth is connected, but no Grok models were returned. Reconnect OAuth or check account access.' @@ -996,7 +995,7 @@ const AutonomousResearchSettings = ({ } catch (err) { console.error('Failed to fetch xAI Grok models:', err); setXaiGrokModels([]); - setHasXAIGrokLogin(false); + setHasXAIGrokLogin(true); setXaiGrokModelError(`xAI Grok OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -1012,7 +1011,7 @@ const AutonomousResearchSettings = ({ const result = await cloudAccessAPI.getSakanaFuguModels(); const models = result.models || []; setSakanaFuguModels(models); - setHasSakanaFuguKey(models.length > 0); + setHasSakanaFuguKey(true); setSakanaFuguModelError(models.length > 0 ? '' : 'Sakana Fugu API key is saved, but no Fugu models were returned. Check your Sakana subscription access.' @@ -1020,11 +1019,42 @@ const AutonomousResearchSettings = ({ } catch (err) { console.error('Failed to fetch Sakana Fugu models:', err); setSakanaFuguModels([]); - setHasSakanaFuguKey(false); + setHasSakanaFuguKey(true); setSakanaFuguModelError(`Sakana Fugu API key is saved, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; + useEffect(() => { + if (credentialStatusRefreshToken === 0) { + return; + } + + let isCurrent = true; + refreshCredentialProviderState({ + freeOnly, + openAICodexOauthAvailable, + xaiGrokOauthAvailable, + sakanaFuguAvailable, + setHasOpenRouterKey, + setOpenRouterModels, + setLoadingOpenRouter, + setHasOpenAICodexLogin, + setOpenAICodexModels, + setOpenAICodexModelError, + setHasXAIGrokLogin, + setXaiGrokModels, + setXaiGrokModelError, + setHasSakanaFuguKey, + setSakanaFuguModels, + setSakanaFuguModelError, + shouldApply: () => isCurrent, + logContext: 'Autonomous settings', + }); + return () => { + isCurrent = false; + }; + }, [credentialStatusRefreshToken]); + // Refetch models when free-only toggle changes useEffect(() => { if (hasOpenRouterKey && isLoadedFromStorage) { @@ -1488,7 +1518,7 @@ Be honest and constructive. Identify both strengths and weaknesses.`; const handleSaveProofSettings = async () => { const parsedTimeout = parseInt(proofSettingsTimeout, 10); - const timeout = Number.isFinite(parsedTimeout) ? parsedTimeout : 600; + const timeout = Number.isFinite(parsedTimeout) ? parsedTimeout : 900; const parsedLspIdleTimeout = parseInt(proofSettingsLspIdleTimeout, 10); const lspIdleTimeout = Number.isFinite(parsedLspIdleTimeout) ? parsedLspIdleTimeout : 600; const parsedMaxParallelCandidates = parseInt(proofSettingsMaxParallelCandidates, 10); diff --git a/frontend/src/components/autonomous/AutonomousResearchSettings.test.jsx b/frontend/src/components/autonomous/AutonomousResearchSettings.test.jsx index 21cbaa3..888826f 100644 --- a/frontend/src/components/autonomous/AutonomousResearchSettings.test.jsx +++ b/frontend/src/components/autonomous/AutonomousResearchSettings.test.jsx @@ -99,7 +99,7 @@ beforeEach(() => { autonomousAPI.getProofStatus.mockResolvedValue({ lean4_enabled: false, lean4_path: '', - lean4_proof_timeout: 600, + lean4_proof_timeout: 900, lean4_lsp_enabled: false, proof_max_parallel_candidates: 6, smt_enabled: false, diff --git a/frontend/src/components/compiler/CompilerInterface.jsx b/frontend/src/components/compiler/CompilerInterface.jsx index b0c8ea0..004166f 100644 --- a/frontend/src/components/compiler/CompilerInterface.jsx +++ b/frontend/src/components/compiler/CompilerInterface.jsx @@ -383,7 +383,7 @@ function CompilerInterface({ const status = await autonomousAPI.getProofStatus(); const updatedStatus = await autonomousAPI.updateProofSettings({ enabled, - timeout: status.lean4_proof_timeout ?? 600, + timeout: status.lean4_proof_timeout ?? 900, lean4_lsp_enabled: Boolean(status.lean4_lsp_enabled), lean4_lsp_idle_timeout: status.lean4_lsp_idle_timeout ?? 600, max_parallel_candidates: status.proof_max_parallel_candidates ?? 6, diff --git a/frontend/src/components/compiler/CompilerLogs.jsx b/frontend/src/components/compiler/CompilerLogs.jsx index 77b5688..7f50967 100644 --- a/frontend/src/components/compiler/CompilerLogs.jsx +++ b/frontend/src/components/compiler/CompilerLogs.jsx @@ -46,12 +46,19 @@ const proofTargetLabel = (data = {}, fallback = 'candidate') => ( const leanProofResponse = (data = {}) => { if (data.lean_response) { - return compactProofText(data.lean_response); + let response = compactProofText(data.lean_response); + if (/timed out after/i.test(response) && !/Advanced Settings/.test(response)) { + response = `${response} You can change this timeout in Advanced Settings.`; + } + return response; } if (data.proof_verified === true) { return 'Lean 4 response: proof verified.'; } - const error = compactProofText(data.error_summary || data.error_output || data.reason, 1800); + let error = compactProofText(data.error_summary || data.error_output || data.reason, 1800); + if (/timed out after/i.test(error) && !/Advanced Settings/.test(error)) { + error = `${error} You can change this timeout in Advanced Settings.`; + } return error ? `Lean 4 response: ${error} - proof not verified.` : ''; }; @@ -179,6 +186,7 @@ function CompilerLogs() { addEvent({ type: eventName, data }); }; const handleAssistantProofPackUpdated = (data) => handleAssistantProofPackEvent('assistant_proof_pack_updated', data); + const handleAssistantProofPackFailed = (data) => handleAssistantProofPackEvent('assistant_proof_pack_failed', data); // Handler for critique progress to update stats display const handleCritiqueProgress = (data) => { @@ -218,6 +226,7 @@ function CompilerLogs() { websocket.on('model_recovery_failed', handleRecoveryFailed); websocket.on('hung_connection_alert', handleHungConnectionAlert); websocket.on('assistant_proof_pack_updated', handleAssistantProofPackUpdated); + websocket.on('assistant_proof_pack_failed', handleAssistantProofPackFailed); // Critique phase events websocket.on('critique_phase_started', handleCritiquePhaseStarted); @@ -259,6 +268,7 @@ function CompilerLogs() { websocket.off('model_recovery_failed', handleRecoveryFailed); websocket.off('hung_connection_alert', handleHungConnectionAlert); websocket.off('assistant_proof_pack_updated', handleAssistantProofPackUpdated); + websocket.off('assistant_proof_pack_failed', handleAssistantProofPackFailed); // Critique phase events cleanup websocket.off('critique_phase_started', handleCritiquePhaseStarted); @@ -400,7 +410,7 @@ function CompilerLogs() { if (type === 'self_review_appended') { return `AI self-review appended (${data.critique_count || 0} accepted critique${data.critique_count === 1 ? '' : 's'})`; } - if (type === 'assistant_proof_pack_updated') { + if (type === 'assistant_proof_pack_updated' || type === 'assistant_proof_pack_failed') { return formatAssistantProofPackEventMessage(type, data); } diff --git a/frontend/src/components/compiler/CompilerSettings.jsx b/frontend/src/components/compiler/CompilerSettings.jsx index 90a010a..0c98e9c 100644 --- a/frontend/src/components/compiler/CompilerSettings.jsx +++ b/frontend/src/components/compiler/CompilerSettings.jsx @@ -19,6 +19,7 @@ import { OPENROUTER_REASONING_EFFORT_OPTIONS, SAKANA_FUGU_REASONING_EFFORT_OPTIONS, } from '../../utils/openRouterSelection'; +import { refreshCredentialProviderState } from '../../utils/credentialProviderRefresh'; import { chooseCloudAccessProvider, getConfiguredCloudAccessProviders, @@ -55,7 +56,12 @@ const readWriterSetting = (settings, suffix) => { return settings[`${LEGACY_WRITER_CAMEL_PREFIX}${suffix}`]; }; -function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabled = false }) { +function CompilerSettings({ + capabilities, + connectivityStatus, + credentialStatusRefreshToken = 0, + developerModeEnabled = false, +}) { // LM Studio and OpenRouter models const [lmStudioModels, setLmStudioModels] = useState([]); const [openRouterModels, setOpenRouterModels] = useState([]); @@ -193,7 +199,6 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } } catch (err) { console.error('Failed to check OpenAI Codex login:', err); - setHasOpenAICodexLogin(false); setOpenAICodexModelError(`OpenAI Codex OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -213,7 +218,6 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } } catch (err) { console.error('Failed to check xAI Grok login:', err); - setHasXAIGrokLogin(false); setXaiGrokModelError(`xAI Grok OAuth status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -233,7 +237,6 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } } catch (err) { console.error('Failed to check Sakana Fugu API key:', err); - setHasSakanaFuguKey(false); setSakanaFuguModelError(`Sakana Fugu status could not be checked: ${err.message || 'unknown error'}.`); } } else { @@ -544,7 +547,7 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl const result = await cloudAccessAPI.getOpenAICodexModels(); const models = result.models || []; setOpenAICodexModels(models); - setHasOpenAICodexLogin(models.length > 0); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(models.length > 0 ? '' : 'OpenAI Codex OAuth is connected, but no Codex models were returned. Reconnect OAuth or check account access.' @@ -552,7 +555,7 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } catch (err) { console.error('Failed to fetch OpenAI Codex models:', err); setOpenAICodexModels([]); - setHasOpenAICodexLogin(false); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(`OpenAI Codex OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -568,7 +571,7 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl const result = await cloudAccessAPI.getXAIGrokModels(); const models = result.models || []; setXaiGrokModels(models); - setHasXAIGrokLogin(models.length > 0); + setHasXAIGrokLogin(true); setXaiGrokModelError(models.length > 0 ? '' : 'xAI Grok OAuth is connected, but no Grok models were returned. Reconnect OAuth or check account access.' @@ -576,7 +579,7 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } catch (err) { console.error('Failed to fetch xAI Grok models:', err); setXaiGrokModels([]); - setHasXAIGrokLogin(false); + setHasXAIGrokLogin(true); setXaiGrokModelError(`xAI Grok OAuth is connected, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; @@ -592,7 +595,7 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl const result = await cloudAccessAPI.getSakanaFuguModels(); const models = result.models || []; setSakanaFuguModels(models); - setHasSakanaFuguKey(models.length > 0); + setHasSakanaFuguKey(true); setSakanaFuguModelError(models.length > 0 ? '' : 'Sakana Fugu API key is saved, but no Fugu models were returned. Check your Sakana subscription access.' @@ -600,11 +603,41 @@ function CompilerSettings({ capabilities, connectivityStatus, developerModeEnabl } catch (err) { console.error('Failed to fetch Sakana Fugu models:', err); setSakanaFuguModels([]); - setHasSakanaFuguKey(false); + setHasSakanaFuguKey(true); setSakanaFuguModelError(`Sakana Fugu API key is saved, but models could not be loaded: ${err.message || 'unknown error'}.`); } }; + useEffect(() => { + if (credentialStatusRefreshToken === 0) { + return; + } + + let isCurrent = true; + refreshCredentialProviderState({ + freeOnly, + openAICodexOauthAvailable, + xaiGrokOauthAvailable, + sakanaFuguAvailable, + setHasOpenRouterKey, + setOpenRouterModels, + setHasOpenAICodexLogin, + setOpenAICodexModels, + setOpenAICodexModelError, + setHasXAIGrokLogin, + setXaiGrokModels, + setXaiGrokModelError, + setHasSakanaFuguKey, + setSakanaFuguModels, + setSakanaFuguModelError, + shouldApply: () => isCurrent, + logContext: 'Compiler settings', + }); + return () => { + isCurrent = false; + }; + }, [credentialStatusRefreshToken]); + // Refetch models when free-only toggle changes useEffect(() => { if (hasOpenRouterKey && isLoaded) { diff --git a/frontend/src/components/leanoj/LeanOJSettings.jsx b/frontend/src/components/leanoj/LeanOJSettings.jsx index 0ae07f2..1f07abd 100644 --- a/frontend/src/components/leanoj/LeanOJSettings.jsx +++ b/frontend/src/components/leanoj/LeanOJSettings.jsx @@ -19,6 +19,7 @@ import { OPENROUTER_REASONING_EFFORT_OPTIONS, SAKANA_FUGU_REASONING_EFFORT_OPTIONS, } from '../../utils/openRouterSelection'; +import { refreshCredentialProviderState } from '../../utils/credentialProviderRefresh'; import { chooseCloudAccessProvider, getConfiguredCloudAccessProviders, @@ -329,6 +330,7 @@ export default function LeanOJSettings({ onSettingsChange, capabilities, connectivityStatus, + credentialStatusRefreshToken = 0, isRunning, developerModeEnabled = false, }) { @@ -391,7 +393,7 @@ export default function LeanOJSettings({ const codexModels = await cloudAccessAPI.getOpenAICodexModels(); const models = codexModels.models || []; setOpenAICodexModels(models); - setHasOpenAICodexLogin(models.length > 0); + setHasOpenAICodexLogin(true); setOpenAICodexModelError(models.length > 0 ? '' : 'OpenAI Codex OAuth is connected, but no Codex models were returned. Reconnect OAuth or check account access.' @@ -401,7 +403,6 @@ export default function LeanOJSettings({ } } catch (error) { console.error('Failed to load OpenAI Codex state for Proof Solver:', error); - setHasOpenAICodexLogin(false); setOpenAICodexModels([]); setOpenAICodexModelError(`OpenAI Codex OAuth models could not be loaded: ${error.message || 'unknown error'}.`); } @@ -420,7 +421,7 @@ export default function LeanOJSettings({ const xaiModels = await cloudAccessAPI.getXAIGrokModels(); const models = xaiModels.models || []; setXaiGrokModels(models); - setHasXAIGrokLogin(models.length > 0); + setHasXAIGrokLogin(true); setXaiGrokModelError(models.length > 0 ? '' : 'xAI Grok OAuth is connected, but no Grok models were returned. Reconnect OAuth or check account access.' @@ -430,7 +431,6 @@ export default function LeanOJSettings({ } } catch (error) { console.error('Failed to load xAI Grok state for Proof Solver:', error); - setHasXAIGrokLogin(false); setXaiGrokModels([]); setXaiGrokModelError(`xAI Grok OAuth models could not be loaded: ${error.message || 'unknown error'}.`); } @@ -449,7 +449,7 @@ export default function LeanOJSettings({ const sakanaModels = await cloudAccessAPI.getSakanaFuguModels(); const models = sakanaModels.models || []; setSakanaFuguModels(models); - setHasSakanaFuguKey(models.length > 0); + setHasSakanaFuguKey(true); setSakanaFuguModelError(models.length > 0 ? '' : 'Sakana Fugu API key is saved, but no Fugu models were returned. Check your Sakana subscription access.' @@ -459,7 +459,6 @@ export default function LeanOJSettings({ } } catch (error) { console.error('Failed to load Sakana Fugu state for Proof Solver:', error); - setHasSakanaFuguKey(false); setSakanaFuguModels([]); setSakanaFuguModelError(`Sakana Fugu models could not be loaded: ${error.message || 'unknown error'}.`); } @@ -487,6 +486,36 @@ export default function LeanOJSettings({ load(); }, [lmStudioEnabled, settings.freeOnly, openAICodexOauthAvailable, xaiGrokOauthAvailable, sakanaFuguAvailable]); + useEffect(() => { + if (credentialStatusRefreshToken === 0) { + return; + } + + let isCurrent = true; + refreshCredentialProviderState({ + freeOnly: settings.freeOnly, + openAICodexOauthAvailable, + xaiGrokOauthAvailable, + sakanaFuguAvailable, + setHasOpenRouterKey, + setOpenRouterModels, + setHasOpenAICodexLogin, + setOpenAICodexModels, + setOpenAICodexModelError, + setHasXAIGrokLogin, + setXaiGrokModels, + setXaiGrokModelError, + setHasSakanaFuguKey, + setSakanaFuguModels, + setSakanaFuguModelError, + shouldApply: () => isCurrent, + logContext: 'Proof Solver settings', + }); + return () => { + isCurrent = false; + }; + }, [credentialStatusRefreshToken]); + useEffect(() => { setSelectedProfile(settings.selectedProfile || ''); }, [settings.selectedProfile]); diff --git a/frontend/src/index.css b/frontend/src/index.css index fa3889a..968e26c 100644 --- a/frontend/src/index.css +++ b/frontend/src/index.css @@ -269,6 +269,7 @@ code { position: fixed; top: 8px; right: 350px; /* Positioned next to expanded panel (320px + 30px margin) */ + max-width: calc(100vw - 40px); z-index: 1001; display: flex; flex-direction: column; @@ -354,7 +355,8 @@ code { } .connectivity-panel { - width: 330px; + width: min(330px, calc(100vw - 40px)); + max-width: 100%; display: flex; flex-direction: column; gap: 8px; @@ -466,6 +468,7 @@ code { .connectivity-row__left { min-width: 0; + flex: 1 1 auto; display: inline-flex; align-items: center; gap: 0.45rem; @@ -473,6 +476,7 @@ code { } .connectivity-label { + min-width: 0; color: rgba(255, 255, 255, 0.92); font-size: 0.8rem; font-weight: 650; @@ -489,16 +493,16 @@ code { display: inline-grid; place-content: center; box-sizing: border-box; - border: 1px solid rgba(30, 255, 28, 0.52); + border: 1px solid rgba(76, 175, 80, 0.62); border-radius: 3px; background: rgba(4, 12, 6, 0.84); - accent-color: #1eff1c; + accent-color: var(--accent-green); cursor: pointer; } .connectivity-checkbox:checked { - background: #1eff1c; - border-color: #1eff1c; + background: var(--accent-green); + border-color: var(--accent-green); } .connectivity-checkbox:checked::after { @@ -1236,9 +1240,25 @@ button.danger:hover { .mode-switch-control { min-width: 220px; } + + .connectivity-panel .mode-switch-control--compact { + min-width: 0; + } .app-header { - right: 20px; + top: 12px; + right: 12px; + max-width: calc(100vw - 24px); + } + + .app-header.panel-collapsed { + right: 12px; + } + + .connectivity-panel { + width: min(300px, calc(100vw - 24px)); + max-height: calc(100vh - 24px); + overflow-y: auto; } } diff --git a/frontend/src/utils/activityStyles.js b/frontend/src/utils/activityStyles.js index 97c7e4e..089915c 100644 --- a/frontend/src/utils/activityStyles.js +++ b/frontend/src/utils/activityStyles.js @@ -35,6 +35,8 @@ export const getActivityIcon = (event = '') => { switch (event) { case 'assistant_proof_pack_updated': return 'A'; + case 'assistant_proof_pack_failed': + return '!'; case 'brainstorm_submission_accepted': case 'submission_accepted': case 'compiler_acceptance': @@ -317,6 +319,7 @@ export const getActivityClass = (event = '', item = {}) => { event === 'tier3_rejection' || event === 'proof_attempt_failed' || event === 'proof_attempts_exhausted' || + event === 'assistant_proof_pack_failed' || event === 'proof_integrity_rejected' || event === 'smt_check_error' || event === 'context_overflow_error' || @@ -431,6 +434,7 @@ export const formatAssistantProofPackMessage = (data = {}) => { export const ASSISTANT_PROOF_PACK_EVENTS = new Set([ 'assistant_proof_pack_updated', + 'assistant_proof_pack_failed', ]); export const ASSISTANT_PROOF_PACK_DUPLICATE_WINDOW_MS = 15000; @@ -462,6 +466,7 @@ export const getAssistantProofPackDuplicateKey = (event = '', data = {}) => { data.batch_attempts ?? '', data.batch_size ?? '', data.reason || '', + data.error_message || '', Array.isArray(data.warnings) ? data.warnings.join('|') : '', ].join('::'); }; @@ -532,8 +537,23 @@ export const formatAssistantProofPackEventMessage = (event = '', data = {}) => { const warnings = Array.isArray(data.warnings) ? data.warnings.filter(Boolean).join('; ') : ''; return `Assistant memory refresh warning for ${target}${phaseText}: ${warnings || 'proof-search support could not be refreshed'}`; } + if (event === 'assistant_proof_pack_failed') { + const detail = String(data.error_message || data.reason || '').trim(); + const failureText = detail ? `: ${detail}` : ''; + return `Assistant memory model call failed for ${target}${phaseText}${modelText}${candidateText}${failureText}`; + } if (event === 'assistant_proof_pack_stopped') { return `Assistant memory stopped (${data.reason || 'parent stopped'})`; } return formatAssistantProofPackMessage(data); }; + +export const buildAutonomousProofProviderPauseActivity = (data = {}) => { + const isCreditPause = data.reason === 'openrouter_credit_exhaustion'; + return { + isCreditPause, + message: isCreditPause + ? `Autonomous proof verification paused until OpenRouter credits are reset: ${data.message || data.source_id || 'provider credits exhausted'}` + : `Autonomous proof verification paused for a transient provider error and will retry automatically: ${data.message || data.source_id || 'provider retry pending'}`, + }; +}; diff --git a/frontend/src/utils/activityStyles.test.js b/frontend/src/utils/activityStyles.test.js index 92e2b9d..917529b 100644 --- a/frontend/src/utils/activityStyles.test.js +++ b/frontend/src/utils/activityStyles.test.js @@ -1,9 +1,11 @@ import { ASSISTANT_PROOF_PACK_EVENTS, REJECTION_FEEDBACK_NOTICE, + buildAutonomousProofProviderPauseActivity, buildRejectionFeedbackNoticeActivity, formatAssistantProofPackEventMessage, formatAssistantProofPackMessage, + getActivityClass, getAssistantProofPackDuplicateKey, shouldAddRejectionFeedbackNotice, } from './activityStyles'; @@ -45,6 +47,24 @@ test('keeps Assistant warning count when backend reports a real warning', () => expect(message).toContain('(1 warning)'); }); +test('formats Assistant model-output failure as an error activity', () => { + const data = { + candidate_count: 64, + shortlist_count: 20, + target_kind: 'brainstorm_context', + workflow_phase: 'brainstorm', + assistant_role_id: 'autonomous_assistant', + assistant_model_id: 'google/gemma-4-26b-a4b', + reason: 'assistant_llm_selection_failed', + error_message: 'No JSON found in response', + }; + + expect(formatAssistantProofPackEventMessage('assistant_proof_pack_failed', data)).toBe( + 'Assistant memory model call failed for brainstorm context during brainstorm via Assistant (google/gemma-4-26b-a4b) from 64 candidates (20 shortlisted): No JSON found in response' + ); + expect(getActivityClass('assistant_proof_pack_failed')).toBe('activity-reject'); +}); + test('adds rejection feedback notice on first and tenth consecutive rejection only', () => { expect(shouldAddRejectionFeedbackNotice({ total_rejections: 1 })).toBe(true); expect(shouldAddRejectionFeedbackNotice({ total_rejections: 7, consecutive_rejections: 10 })).toBe(true); @@ -68,8 +88,46 @@ test('does not treat Assistant skip or cooldown events as displayable live activ expect(ASSISTANT_PROOF_PACK_EVENTS.has('assistant_proof_memory_unavailable')).toBe(false); expect(ASSISTANT_PROOF_PACK_EVENTS.has('assistant_proof_memory_cooldown')).toBe(false); expect(ASSISTANT_PROOF_PACK_EVENTS.has('assistant_proof_memory_shutdown')).toBe(false); + expect(ASSISTANT_PROOF_PACK_EVENTS.has('assistant_proof_pack_failed')).toBe(true); expect(getAssistantProofPackDuplicateKey('assistant_proof_memory_cooldown', { target_hash: 'target', cooldown_kind: 'zero_useful', })).toBe(''); }); + +test('keeps distinct Assistant failure details out of duplicate suppression', () => { + const base = { + target_hash: 'target-1', + workflow_mode: 'autonomous', + target_kind: 'brainstorm_context', + workflow_phase: 'brainstorm', + source_type: 'brainstorm', + source_id: 'topic_1', + reason: 'assistant_llm_selection_failed', + }; + + expect(getAssistantProofPackDuplicateKey('assistant_proof_pack_failed', { + ...base, + error_message: 'No JSON found in response', + })).not.toBe(getAssistantProofPackDuplicateKey('assistant_proof_pack_failed', { + ...base, + error_message: 'Response exceeded context window', + })); +}); + +test('distinguishes autonomous proof transient provider pauses from credit pauses', () => { + const transient = buildAutonomousProofProviderPauseActivity({ + reason: 'transient_provider_error', + message: 'OpenRouter gateway timeout', + }); + expect(transient.isCreditPause).toBe(false); + expect(transient.message).toContain('will retry automatically'); + expect(transient.message).not.toContain('credits are reset'); + + const credit = buildAutonomousProofProviderPauseActivity({ + reason: 'openrouter_credit_exhaustion', + message: 'credits exhausted', + }); + expect(credit.isCreditPause).toBe(true); + expect(credit.message).toContain('credits are reset'); +}); diff --git a/frontend/src/utils/credentialProviderRefresh.js b/frontend/src/utils/credentialProviderRefresh.js new file mode 100644 index 0000000..a54c0ad --- /dev/null +++ b/frontend/src/utils/credentialProviderRefresh.js @@ -0,0 +1,163 @@ +import { cloudAccessAPI, openRouterAPI } from '../services/api'; + +const noop = () => {}; +const alwaysCurrent = () => true; + +function applyIfCurrent(shouldApply, setter, ...args) { + if (shouldApply()) { + setter(...args); + } +} + +export async function refreshCredentialProviderState({ + freeOnly = false, + openAICodexOauthAvailable = false, + xaiGrokOauthAvailable = false, + sakanaFuguAvailable = false, + setHasOpenRouterKey = noop, + setOpenRouterModels = noop, + setLoadingOpenRouter = noop, + setHasOpenAICodexLogin = noop, + setOpenAICodexModels = noop, + setOpenAICodexModelError = noop, + setHasXAIGrokLogin = noop, + setXaiGrokModels = noop, + setXaiGrokModelError = noop, + setHasSakanaFuguKey = noop, + setSakanaFuguModels = noop, + setSakanaFuguModelError = noop, + shouldApply = alwaysCurrent, + logContext = 'settings', +} = {}) { + try { + const status = await openRouterAPI.getApiKeyStatus(); + if (!shouldApply()) return; + const configured = Boolean(status.has_key); + applyIfCurrent(shouldApply, setHasOpenRouterKey, configured); + if (configured) { + applyIfCurrent(shouldApply, setLoadingOpenRouter, true); + try { + const result = await openRouterAPI.getModels(null, freeOnly); + applyIfCurrent(shouldApply, setOpenRouterModels, result.models || []); + } catch (error) { + if (!shouldApply()) return; + console.error(`Failed to refresh OpenRouter models for ${logContext}:`, error); + } finally { + applyIfCurrent(shouldApply, setLoadingOpenRouter, false); + } + } else { + applyIfCurrent(shouldApply, setOpenRouterModels, []); + } + } catch (error) { + if (!shouldApply()) return; + console.error(`Failed to refresh OpenRouter state for ${logContext}:`, error); + applyIfCurrent(shouldApply, setHasOpenRouterKey, false); + applyIfCurrent(shouldApply, setOpenRouterModels, []); + applyIfCurrent(shouldApply, setLoadingOpenRouter, false); + } + + if (openAICodexOauthAvailable) { + try { + const status = await cloudAccessAPI.getOpenAICodexStatus(); + if (!shouldApply()) return; + const configured = Boolean(status.status?.configured); + applyIfCurrent(shouldApply, setHasOpenAICodexLogin, configured); + if (configured) { + const result = await cloudAccessAPI.getOpenAICodexModels(); + if (!shouldApply()) return; + const models = result.models || []; + applyIfCurrent(shouldApply, setOpenAICodexModels, models); + applyIfCurrent(shouldApply, setOpenAICodexModelError, models.length > 0 + ? '' + : 'OpenAI Codex OAuth is connected, but no Codex models were returned. Reconnect OAuth or check account access.' + ); + } else { + applyIfCurrent(shouldApply, setOpenAICodexModels, []); + applyIfCurrent(shouldApply, setOpenAICodexModelError, ''); + } + } catch (error) { + if (!shouldApply()) return; + console.error(`Failed to refresh OpenAI Codex state for ${logContext}:`, error); + applyIfCurrent(shouldApply, setOpenAICodexModels, []); + applyIfCurrent( + shouldApply, + setOpenAICodexModelError, + `OpenAI Codex OAuth models could not be loaded: ${error.message || 'unknown error'}.` + ); + } + } else { + applyIfCurrent(shouldApply, setHasOpenAICodexLogin, false); + applyIfCurrent(shouldApply, setOpenAICodexModels, []); + applyIfCurrent(shouldApply, setOpenAICodexModelError, ''); + } + + if (xaiGrokOauthAvailable) { + try { + const status = await cloudAccessAPI.getXAIGrokStatus(); + if (!shouldApply()) return; + const configured = Boolean(status.status?.configured); + applyIfCurrent(shouldApply, setHasXAIGrokLogin, configured); + if (configured) { + const result = await cloudAccessAPI.getXAIGrokModels(); + if (!shouldApply()) return; + const models = result.models || []; + applyIfCurrent(shouldApply, setXaiGrokModels, models); + applyIfCurrent(shouldApply, setXaiGrokModelError, models.length > 0 + ? '' + : 'xAI Grok OAuth is connected, but no Grok models were returned. Reconnect OAuth or check account access.' + ); + } else { + applyIfCurrent(shouldApply, setXaiGrokModels, []); + applyIfCurrent(shouldApply, setXaiGrokModelError, ''); + } + } catch (error) { + if (!shouldApply()) return; + console.error(`Failed to refresh xAI Grok state for ${logContext}:`, error); + applyIfCurrent(shouldApply, setXaiGrokModels, []); + applyIfCurrent( + shouldApply, + setXaiGrokModelError, + `xAI Grok OAuth models could not be loaded: ${error.message || 'unknown error'}.` + ); + } + } else { + applyIfCurrent(shouldApply, setHasXAIGrokLogin, false); + applyIfCurrent(shouldApply, setXaiGrokModels, []); + applyIfCurrent(shouldApply, setXaiGrokModelError, ''); + } + + if (sakanaFuguAvailable) { + try { + const status = await cloudAccessAPI.getSakanaFuguStatus(); + if (!shouldApply()) return; + const configured = Boolean(status.status?.configured); + applyIfCurrent(shouldApply, setHasSakanaFuguKey, configured); + if (configured) { + const result = await cloudAccessAPI.getSakanaFuguModels(); + if (!shouldApply()) return; + const models = result.models || []; + applyIfCurrent(shouldApply, setSakanaFuguModels, models); + applyIfCurrent(shouldApply, setSakanaFuguModelError, models.length > 0 + ? '' + : 'Sakana Fugu API key is saved, but no Fugu models were returned. Check your Sakana subscription access.' + ); + } else { + applyIfCurrent(shouldApply, setSakanaFuguModels, []); + applyIfCurrent(shouldApply, setSakanaFuguModelError, ''); + } + } catch (error) { + if (!shouldApply()) return; + console.error(`Failed to refresh Sakana Fugu state for ${logContext}:`, error); + applyIfCurrent(shouldApply, setSakanaFuguModels, []); + applyIfCurrent( + shouldApply, + setSakanaFuguModelError, + `Sakana Fugu models could not be loaded: ${error.message || 'unknown error'}.` + ); + } + } else { + applyIfCurrent(shouldApply, setHasSakanaFuguKey, false); + applyIfCurrent(shouldApply, setSakanaFuguModels, []); + applyIfCurrent(shouldApply, setSakanaFuguModelError, ''); + } +} diff --git a/frontend/src/utils/credentialProviderRefresh.test.js b/frontend/src/utils/credentialProviderRefresh.test.js new file mode 100644 index 0000000..e293312 --- /dev/null +++ b/frontend/src/utils/credentialProviderRefresh.test.js @@ -0,0 +1,113 @@ +import { refreshCredentialProviderState } from './credentialProviderRefresh'; +import { cloudAccessAPI, openRouterAPI } from '../services/api'; + +vi.mock('../services/api', () => ({ + cloudAccessAPI: { + getOpenAICodexStatus: vi.fn(), + getOpenAICodexModels: vi.fn(), + getXAIGrokStatus: vi.fn(), + getXAIGrokModels: vi.fn(), + getSakanaFuguStatus: vi.fn(), + getSakanaFuguModels: vi.fn(), + }, + openRouterAPI: { + getApiKeyStatus: vi.fn(), + getModels: vi.fn(), + }, +})); + +beforeEach(() => { + vi.clearAllMocks(); + vi.spyOn(console, 'error').mockImplementation(() => {}); +}); + +afterEach(() => { + vi.restoreAllMocks(); +}); + +test('keeps OpenRouter enabled when model refresh fails after a valid key check', async () => { + const setHasOpenRouterKey = vi.fn(); + const setOpenRouterModels = vi.fn(); + const setLoadingOpenRouter = vi.fn(); + + openRouterAPI.getApiKeyStatus.mockResolvedValue({ has_key: true }); + openRouterAPI.getModels.mockRejectedValue(new Error('models unavailable')); + + await refreshCredentialProviderState({ + setHasOpenRouterKey, + setOpenRouterModels, + setLoadingOpenRouter, + }); + + expect(setHasOpenRouterKey).toHaveBeenCalledWith(true); + expect(setOpenRouterModels).not.toHaveBeenCalled(); + expect(setLoadingOpenRouter).toHaveBeenNthCalledWith(1, true); + expect(setLoadingOpenRouter).toHaveBeenLastCalledWith(false); +}); + +test('keeps configured OAuth provider enabled when model loading fails', async () => { + const setHasOpenAICodexLogin = vi.fn(); + const setOpenAICodexModels = vi.fn(); + const setOpenAICodexModelError = vi.fn(); + + openRouterAPI.getApiKeyStatus.mockResolvedValue({ has_key: false }); + cloudAccessAPI.getOpenAICodexStatus.mockResolvedValue({ status: { configured: true } }); + cloudAccessAPI.getOpenAICodexModels.mockRejectedValue(new Error('oauth model error')); + + await refreshCredentialProviderState({ + openAICodexOauthAvailable: true, + setHasOpenAICodexLogin, + setOpenAICodexModels, + setOpenAICodexModelError, + }); + + expect(setHasOpenAICodexLogin).toHaveBeenCalledWith(true); + expect(setOpenAICodexModels).toHaveBeenCalledWith([]); + expect(setOpenAICodexModelError).toHaveBeenCalledWith( + expect.stringContaining('OpenAI Codex OAuth models could not be loaded') + ); +}); + +test('keeps configured subscription provider enabled when no models are returned', async () => { + const setHasSakanaFuguKey = vi.fn(); + const setSakanaFuguModels = vi.fn(); + const setSakanaFuguModelError = vi.fn(); + + openRouterAPI.getApiKeyStatus.mockResolvedValue({ has_key: false }); + cloudAccessAPI.getSakanaFuguStatus.mockResolvedValue({ status: { configured: true } }); + cloudAccessAPI.getSakanaFuguModels.mockResolvedValue({ models: [] }); + + await refreshCredentialProviderState({ + sakanaFuguAvailable: true, + setHasSakanaFuguKey, + setSakanaFuguModels, + setSakanaFuguModelError, + }); + + expect(setHasSakanaFuguKey).toHaveBeenCalledWith(true); + expect(setHasSakanaFuguKey).not.toHaveBeenCalledWith(false); + expect(setSakanaFuguModels).toHaveBeenCalledWith([]); + expect(setSakanaFuguModelError).toHaveBeenCalledWith( + expect.stringContaining('no Fugu models were returned') + ); +}); + +test('does not update state after shouldApply returns false', async () => { + const setHasOpenRouterKey = vi.fn(); + const setOpenRouterModels = vi.fn(); + let current = true; + + openRouterAPI.getApiKeyStatus.mockImplementation(async () => { + current = false; + return { has_key: true }; + }); + + await refreshCredentialProviderState({ + setHasOpenRouterKey, + setOpenRouterModels, + shouldApply: () => current, + }); + + expect(setHasOpenRouterKey).not.toHaveBeenCalled(); + expect(setOpenRouterModels).not.toHaveBeenCalled(); +}); diff --git a/moto-update-manifest.json b/moto-update-manifest.json index 7f8c2b0..6ca1b63 100644 --- a/moto-update-manifest.json +++ b/moto-update-manifest.json @@ -1,10 +1,7 @@ { "manifest_version": 1, - "version": "1.1.01", - "build_commit": "7d86e422f615dcea682160126ae88006699aff34", + "version": "1.1.02", + "build_commit": "40be14c63aee7027f02d36479416e1341385b6e3", "update_channel": "main", - "api_contract_version": "build5-v53" + "api_contract_version": "build5-v54" } - - - diff --git a/moto_launcher.py b/moto_launcher.py index d643e6d..023338f 100644 --- a/moto_launcher.py +++ b/moto_launcher.py @@ -872,18 +872,37 @@ def install_windows_nodejs() -> bool: return False cprint("Attempting to install Node.js LTS with winget...", YELLOW) - command = [ + run_visible( + [winget_cmd, "source", "update", "--name", "winget"], + cwd=str(SCRIPT_DIR), + check=False, + ) + + base_command = [ winget_cmd, "install", "--id", - "OpenJS.NodeJS.LTS", + "", "-e", "--source", "winget", "--accept-package-agreements", "--accept-source-agreements", ] - return run_visible(command, cwd=str(SCRIPT_DIR), check=False) == 0 + package_ids = ("OpenJS.NodeJS.LTS", "OpenJS.NodeJS") + scope_args = (["--scope", "user"], []) + + for package_id in package_ids: + for scope_arg in scope_args: + command = list(base_command) + command[3] = package_id + command.extend(scope_arg) + scope_label = "user scope" if scope_arg else "default scope" + cprint(f"Trying winget package {package_id} ({scope_label})...", YELLOW) + if run_visible(command, cwd=str(SCRIPT_DIR), check=False) == 0: + return True + + return False def check_node_installation() -> None: @@ -904,7 +923,7 @@ def check_node_installation() -> None: else: cprint("Please install Node.js 20.19+ or 22.12+ from:", YELLOW) cprint("https://nodejs.org/", YELLOW) - cprint("The Windows launcher tried `winget install OpenJS.NodeJS.LTS`, but it was unavailable or failed.", YELLOW) + cprint("The Windows launcher tried winget packages `OpenJS.NodeJS.LTS` and `OpenJS.NodeJS`, but they were unavailable or failed.", YELLOW) exit_with_pause(1) npm_cmd = get_npm_command() @@ -1311,7 +1330,7 @@ def _set_lean_env_flags( env["MOTO_LEAN4_ENABLED"] = "1" if enabled else "0" env["MOTO_LEAN4_PATH"] = lean_path env["MOTO_LEAN4_WORKSPACE_DIR"] = workspace_dir - env["MOTO_LEAN4_PROOF_TIMEOUT"] = env.get("MOTO_LEAN4_PROOF_TIMEOUT", "").strip() or "600" + env["MOTO_LEAN4_PROOF_TIMEOUT"] = env.get("MOTO_LEAN4_PROOF_TIMEOUT", "").strip() or "900" env["MOTO_LEAN4_LSP_ENABLED"] = ( env.get("MOTO_LEAN4_LSP_ENABLED", "").strip() if enabled and env.get("MOTO_LEAN4_LSP_ENABLED", "").strip() diff --git a/moto_updater.py b/moto_updater.py index 55538d7..0a9fb59 100644 --- a/moto_updater.py +++ b/moto_updater.py @@ -32,7 +32,7 @@ "version": "0.0.0-dev", "build_commit": "dev", "update_channel": "main", - "api_contract_version": "build5-v53", + "api_contract_version": "build5-v54", } _DEFAULT_PRESERVED_ROOTS = { diff --git a/package-lock.json b/package-lock.json index 8d27f8a..986c5e2 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "moto-math-variant", - "version": "1.1.01", + "version": "1.1.02", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "moto-math-variant", - "version": "1.1.01", + "version": "1.1.02", "license": "MIT" } } diff --git a/package.json b/package.json index 4f2c051..8004c13 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "moto-math-variant", - "version": "1.1.01", + "version": "1.1.02", "description": "MOTO S.T.E.M. Mathematics Variant - Autonomous ASI Research System for Novel S.T.E.M. Mathematical Paper Generation", "scripts": { "dev:backend": "python -c \"import os, uvicorn; uvicorn.run('backend.api.main:app', host=os.getenv('MOTO_BACKEND_HOST', os.getenv('HOST', '0.0.0.0')), port=int(os.getenv('MOTO_BACKEND_PORT', os.getenv('PORT', '8000'))), reload=True, access_log=False)\"", @@ -31,4 +31,3 @@ }, "homepage": "https://intrafere.com" } - diff --git a/tests/test_assistant_proof_memory_cooldown.py b/tests/test_assistant_proof_memory_cooldown.py index 9c1dec1..eebb8f8 100644 --- a/tests/test_assistant_proof_memory_cooldown.py +++ b/tests/test_assistant_proof_memory_cooldown.py @@ -387,6 +387,105 @@ async def _capture(event_type: str, payload: dict) -> None: self.assertEqual([event for event, _ in events], ["assistant_proof_pack_warning"]) self.assertIn("search failed", events[0][1]["reason"].lower()) + async def test_assistant_selector_failure_emits_failure_not_empty_pack(self) -> None: + with tempfile.TemporaryDirectory() as temp_dir: + cache = AssistantRankCache(Path(temp_dir) / "assistant_ranker.sqlite") + + async def _failing_selector(*args) -> tuple[list[str], str]: + raise RuntimeError("No JSON found in response") + + snapshot = _snapshot() + coordinator = AssistantProofSearchCoordinator( + service=_NoCandidateProofSearchService(), + cache=cache, + assistant_selector=_failing_selector, + ) + await coordinator._publish_pack( + snapshot, + [_support("manual:prior_good")], + warnings=[], + selection_mode="assistant_llm", + assistant_role_id="autonomous_assistant", + assistant_model_id="good-assistant", + candidate_count=1, + shortlist_count=1, + selection_reasoning="seed good pack", + ) + events: list[tuple[str, dict]] = [] + + async def _capture(event_type: str, payload: dict) -> None: + events.append((event_type, payload)) + + with mock.patch("backend.api.routes.websocket.broadcast_event", new=_capture): + await coordinator.refresh_now(snapshot) + + self.assertEqual( + [event for event, _ in events], + ["assistant_proof_pack_refresh_started", "assistant_proof_pack_failed"], + ) + self.assertNotIn("assistant_proof_pack_updated", [event for event, _ in events]) + self.assertEqual(events[-1][1]["reason"], "assistant_llm_selection_failed") + self.assertIn("No JSON found", events[-1][1]["error_message"]) + latest_pack = coordinator.get_latest_pack() + self.assertIsNotNone(latest_pack) + self.assertEqual([support.search_id for support in latest_pack.results], ["manual:prior_good"]) + state = cache.load_cooldown_state(coordinator._run_key_for_snapshot(snapshot)) + self.assertEqual(state.zero_attempts_in_batch, 0) + self.assertEqual(state.zero_cooldown_stage, 0) + self.assertFalse(state.zero_shutdown_active) + + async def test_assistant_selector_failure_does_not_reuse_unrelated_latest_pack(self) -> None: + with tempfile.TemporaryDirectory() as temp_dir: + cache = AssistantRankCache(Path(temp_dir) / "assistant_ranker.sqlite") + + async def _failing_selector(*args) -> tuple[list[str], str]: + raise RuntimeError("No JSON found in response") + + seed_snapshot = _snapshot() + failed_snapshot = _snapshot().model_copy( + update={ + "source_id": "topic_999", + "target_statement": "theorem unrelated_target : True", + "target_hash": "", + } + ) + failed_target_hash = failed_snapshot.stable_hash() + coordinator = AssistantProofSearchCoordinator( + service=_NoCandidateProofSearchService(), + cache=cache, + assistant_selector=_failing_selector, + ) + await coordinator._publish_pack( + seed_snapshot, + [_support("manual:prior_unrelated")], + warnings=[], + selection_mode="assistant_llm", + assistant_role_id="autonomous_assistant", + assistant_model_id="good-assistant", + candidate_count=1, + shortlist_count=1, + selection_reasoning="seed unrelated pack", + ) + events: list[tuple[str, dict]] = [] + + async def _capture(event_type: str, payload: dict) -> None: + events.append((event_type, payload)) + + with mock.patch("backend.api.routes.websocket.broadcast_event", new=_capture): + pack = await coordinator.refresh_now(failed_snapshot) + + self.assertEqual( + [event for event, _ in events], + ["assistant_proof_pack_refresh_started", "assistant_proof_pack_failed"], + ) + self.assertIsNotNone(pack) + self.assertEqual(pack.target_hash, failed_target_hash) + self.assertEqual(pack.results, []) + latest_pack = coordinator.get_latest_pack() + self.assertIsNotNone(latest_pack) + self.assertEqual(latest_pack.target_hash, failed_target_hash) + self.assertEqual(latest_pack.results, []) + async def test_compiler_zero_useful_batches_accumulate_across_transient_task_ids(self) -> None: with tempfile.TemporaryDirectory() as temp_dir: cache = AssistantRankCache(Path(temp_dir) / "assistant_ranker.sqlite") diff --git a/tests/test_assistant_proof_search.py b/tests/test_assistant_proof_search.py index 68646ad..b64b4de 100644 --- a/tests/test_assistant_proof_search.py +++ b/tests/test_assistant_proof_search.py @@ -444,6 +444,64 @@ async def test_assistant_selector_retries_ids_outside_shortlist(self) -> None: finally: restore() + async def test_assistant_selector_canonicalizes_unique_bare_proof_ids(self) -> None: + restore = _preserve_role_config("manual_proof_assistant") + try: + api_client_manager.configure_role( + "manual_proof_assistant", + ModelConfig( + provider="openrouter", + model_id="assistant-model", + context_window=4096, + max_output_tokens=2048, + ), + ) + coordinator = AssistantProofSearchCoordinator(service=_FakeProofSearchService([])) + snapshot = AssistantTargetSnapshot( + workflow_mode="manual_proof_check", + target_kind="proof_candidate", + user_prompt="Prove the manual target.", + target_statement="theorem target : True", + ) + shortlist = [ + AssistantProofSupport.from_record( + _record(44, search_id="manual:archived_session:proof_44", corpus="manual") + ), + AssistantProofSupport.from_record( + _record(11, search_id="manual:archived_session:proof_11", corpus="manual") + ), + ] + + with mock.patch.object( + api_client_manager, + "generate_completion", + new=mock.AsyncMock( + return_value=_response_json( + '{"selected_search_ids":["proof_44","proof_11"],"reasoning":"use residue certificates"}' + ) + ), + ) as generate_completion: + selected_ids, reasoning = await coordinator._select_with_assistant( + snapshot, + shortlist, + assistant_role_id="manual_proof_assistant", + assistant_model_id="assistant-model", + task_id="assistant_pack_manual_001", + ) + + self.assertEqual( + selected_ids, + ["manual:archived_session:proof_44", "manual:archived_session:proof_11"], + ) + self.assertEqual(reasoning, "use residue certificates") + self.assertEqual(generate_completion.await_count, 1) + prompt = generate_completion.await_args.kwargs["messages"][0]["content"] + self.assertIn("SELECT_ID: manual:archived_session:proof_44", prompt) + self.assertIn("proof_id: proof_44", prompt) + self.assertIn("do not return proof_id/display IDs", prompt) + finally: + restore() + async def test_assistant_selector_valid_empty_selection_is_not_retried(self) -> None: restore = _preserve_role_config("manual_proof_assistant") try: @@ -503,7 +561,7 @@ async def test_assistant_selector_failure_publishes_unavailable_pack(self) -> No ) coordinator = AssistantProofSearchCoordinator( service=_FakeProofSearchService( - [_record(index, corpus="manual") for index in range(3)] + [_record(index, corpus="manual") for index in range(1, 4)] ) ) snapshot = AssistantTargetSnapshot( @@ -854,7 +912,7 @@ async def failing_selector( raise RuntimeError("LM Studio rejected response_format") first = AssistantProofSearchCoordinator( - service=_FakeProofSearchService([_record(index, corpus="manual") for index in range(3)]), + service=_FakeProofSearchService([_record(index, corpus="manual") for index in range(1, 4)]), assistant_selector=failing_selector, ) failed_pack = await first.refresh_now(snapshot) @@ -862,7 +920,7 @@ async def failing_selector( self.assertEqual(failed_pack.results, []) self.assertGreater(failed_pack.candidate_count, 0) - second_service = _FakeProofSearchService([_record(index, corpus="manual") for index in range(3)]) + second_service = _FakeProofSearchService([_record(index, corpus="manual") for index in range(1, 4)]) second = AssistantProofSearchCoordinator( service=second_service, assistant_selector=_fake_assistant_selector, diff --git a/tests/test_autonomous_proof_rounds.py b/tests/test_autonomous_proof_rounds.py index 67ec51f..48605b6 100644 --- a/tests/test_autonomous_proof_rounds.py +++ b/tests/test_autonomous_proof_rounds.py @@ -2,7 +2,11 @@ from importlib import import_module from types import SimpleNamespace -from backend.autonomous.core.autonomous_coordinator import AutonomousCoordinator +from backend.autonomous.core.autonomous_coordinator import ( + _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF, + _brainstorm_rejection_handoff_allowed, + AutonomousCoordinator, +) from backend.autonomous.core.proof_verification_stage import ProofVerificationStage from backend.autonomous.prompts.proof_prompts import build_proof_identification_prompt from backend.shared.config import system_config @@ -177,6 +181,44 @@ def tearDown(self): coordinator_module.proof_database = self.old_proof_database coordinator_module.brainstorm_memory = self.old_brainstorm_memory + def test_brainstorm_handoff_minimum_is_seven_acceptances(self): + self.assertEqual(_BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF, 7) + + def test_rejection_limit_handoff_waits_for_seven_acceptances(self): + self.assertFalse( + _brainstorm_rejection_handoff_allowed( + consecutive_rejections=10, + acceptance_count=_BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF - 1, + ) + ) + self.assertTrue( + _brainstorm_rejection_handoff_allowed( + consecutive_rejections=10, + acceptance_count=_BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF, + ) + ) + + def test_regular_completion_review_waits_for_handoff_minimum(self): + coordinator = AutonomousCoordinator() + coordinator._acceptance_count = _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF - 1 + coordinator._last_completion_review_at = 0 + + self.assertFalse( + coordinator._acceptance_count >= _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + and coordinator._should_run_completion_review() + ) + + coordinator._acceptance_count = _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + coordinator._last_completion_review_at = ( + _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + - system_config.autonomous_completion_review_interval + ) + + self.assertTrue( + coordinator._acceptance_count >= _BRAINSTORM_MIN_ACCEPTANCES_BEFORE_HANDOFF + and coordinator._should_run_completion_review() + ) + def test_follow_up_prompt_uses_strict_question(self): prompt = build_proof_identification_prompt( user_prompt="Solve the problem.", diff --git a/tests/test_model_error_utils.py b/tests/test_model_error_utils.py index 143e4ae..069eda1 100644 --- a/tests/test_model_error_utils.py +++ b/tests/test_model_error_utils.py @@ -5,6 +5,7 @@ is_retryable_model_output_error, is_transient_model_call_error, ) +from backend.shared.openrouter_client import OpenRouterInvalidResponseError class ModelErrorUtilsTests(unittest.TestCase): @@ -70,15 +71,63 @@ def test_xai_grok_server_error_with_missing_fallback_is_transient(self) -> None: self.assertTrue(is_transient_model_call_error(exc)) self.assertFalse(is_non_retryable_model_error(exc)) - def test_openrouter_missing_fallback_remains_non_retryable(self) -> None: + def test_openrouter_upstream_connect_without_fallback_is_transient(self) -> None: exc = RuntimeError( "OpenRouter error for role 'agg_sub1': upstream connect error " "and no LM Studio fallback configured" ) + self.assertTrue(is_transient_model_call_error(exc)) + self.assertFalse(is_non_retryable_model_error(exc)) + + def test_openrouter_invalid_response_is_transient(self) -> None: + exc = OpenRouterInvalidResponseError( + "OpenRouter returned non-JSON body after 3 attempts", + status_code=200, + content_type="text/html", + body_preview="gateway error", + ) + + self.assertTrue(is_transient_model_call_error(exc)) + self.assertFalse(is_non_retryable_model_error(exc)) + + def test_openrouter_non_json_success_without_transient_body_is_not_transient(self) -> None: + exc = OpenRouterInvalidResponseError( + "OpenRouter returned non-JSON body after 3 attempts", + status_code=200, + content_type="text/html", + body_preview="Sign inLogin required", + ) + + self.assertFalse(is_transient_model_call_error(exc)) + + def test_openrouter_json_labeled_invalid_response_is_not_transient_by_default(self) -> None: + exc = OpenRouterInvalidResponseError( + "OpenRouter returned malformed JSON after 3 attempts", + status_code=200, + content_type="application/json", + body_preview='{"unexpected":"shape"}', + ) + + self.assertFalse(is_transient_model_call_error(exc)) + + def test_openrouter_auth_without_fallback_remains_non_retryable(self) -> None: + exc = RuntimeError( + "OpenRouter error for role 'agg_sub1': HTTP 401 unauthorized " + "and no LM Studio fallback configured" + ) + self.assertFalse(is_transient_model_call_error(exc)) self.assertTrue(is_non_retryable_model_error(exc)) + def test_openrouter_rate_limit_is_not_generic_transient(self) -> None: + exc = RuntimeError( + "OpenRouter error for role 'agg_sub1': OpenRouter rate limit: retry later " + "and no LM Studio fallback configured" + ) + + self.assertFalse(is_transient_model_call_error(exc)) + if __name__ == "__main__": unittest.main() diff --git a/tests/test_moto_launcher.py b/tests/test_moto_launcher.py index eeba1fd..ccc9c59 100644 --- a/tests/test_moto_launcher.py +++ b/tests/test_moto_launcher.py @@ -341,6 +341,80 @@ def test_check_node_installation_uses_winget_when_missing_on_windows(self) -> No installer.assert_called_once() + def test_install_windows_nodejs_tries_user_scope_lts_after_source_refresh(self) -> None: + with mock.patch.object(moto_launcher.sys, "platform", "win32"): + with mock.patch.object(moto_launcher, "resolve_command", return_value="winget"): + with mock.patch.object(moto_launcher, "run_visible", side_effect=[0, 0]) as run_visible: + self.assertTrue(moto_launcher.install_windows_nodejs()) + + self.assertEqual(run_visible.call_args_list[0].args[0], ["winget", "source", "update", "--name", "winget"]) + self.assertEqual( + run_visible.call_args_list[1].args[0], + [ + "winget", + "install", + "--id", + "OpenJS.NodeJS.LTS", + "-e", + "--source", + "winget", + "--accept-package-agreements", + "--accept-source-agreements", + "--scope", + "user", + ], + ) + + def test_install_windows_nodejs_falls_back_to_lts_default_then_non_lts_user_scope(self) -> None: + with mock.patch.object(moto_launcher.sys, "platform", "win32"): + with mock.patch.object(moto_launcher, "resolve_command", return_value="winget"): + with mock.patch.object(moto_launcher, "run_visible", side_effect=[0, 1, 1, 0]) as run_visible: + self.assertTrue(moto_launcher.install_windows_nodejs()) + + self.assertEqual( + [call.args[0] for call in run_visible.call_args_list], + [ + ["winget", "source", "update", "--name", "winget"], + [ + "winget", + "install", + "--id", + "OpenJS.NodeJS.LTS", + "-e", + "--source", + "winget", + "--accept-package-agreements", + "--accept-source-agreements", + "--scope", + "user", + ], + [ + "winget", + "install", + "--id", + "OpenJS.NodeJS.LTS", + "-e", + "--source", + "winget", + "--accept-package-agreements", + "--accept-source-agreements", + ], + [ + "winget", + "install", + "--id", + "OpenJS.NodeJS", + "-e", + "--source", + "winget", + "--accept-package-agreements", + "--accept-source-agreements", + "--scope", + "user", + ], + ], + ) + def test_check_node_installation_prepends_detected_node_dir_for_npm_scripts(self) -> None: with tempfile.TemporaryDirectory() as temp_dir: node_dir = Path(temp_dir) / "nodejs" diff --git a/tests/test_oauth_provider_cooldown.py b/tests/test_oauth_provider_cooldown.py index 934049f..179b969 100644 --- a/tests/test_oauth_provider_cooldown.py +++ b/tests/test_oauth_provider_cooldown.py @@ -2,8 +2,13 @@ import time from unittest import IsolatedAsyncioTestCase, mock -from backend.shared.api_client_manager import APIClientManager, OAuthProviderCooldownError +from backend.shared.api_client_manager import ( + APIClientManager, + OAuthProviderCooldownError, + RetryableProviderError, +) from backend.shared.config import system_config +from backend.shared.model_error_utils import is_transient_model_call_error from backend.shared.models import ModelConfig from backend.shared.openai_codex_client import OAuthUsageLimitError, OpenAICodexClient from backend.shared.provider_notification_store import record_provider_notification @@ -129,16 +134,106 @@ async def test_wait_for_oauth_provider_cooldown_sleeps_until_expired(self) -> No resets_at=int(time.time()) + 300, resets_in_seconds=1, ) - async def expire_after_sleep(_seconds: int) -> None: + async def expire_after_sleep(_seconds: int, _should_stop=None) -> None: self.manager._oauth_provider_cooldowns["openai_codex_oauth"]["cooldown_until"] = int(time.time()) - 1 - with mock.patch( - "backend.shared.api_client_manager.asyncio.sleep", + with mock.patch.object( + self.manager, + "_sleep_with_optional_stop", new=mock.AsyncMock(side_effect=expire_after_sleep), ) as sleep_mock: await self.manager.wait_for_oauth_provider_cooldown(error, role_id="agg_sub1") sleep_mock.assert_awaited() + async def test_retryable_provider_error_uses_shared_exponential_backoff(self) -> None: + error = RetryableProviderError( + provider="openai_codex_oauth", + provider_label="OpenAI Codex", + role_id="autonomous_proof_formalization_brainstorm", + model="gpt-5.5", + reason="transient_provider_error", + message="OpenAI Codex transient transport failure", + ) + + with mock.patch.object( + self.manager, + "_sleep_with_optional_stop", + new=mock.AsyncMock(), + ) as sleep_mock: + await self.manager.wait_for_retryable_provider_error(error) + await self.manager.wait_for_retryable_provider_error(error) + + sleep_mock.assert_has_awaits([ + mock.call(60, None), + mock.call(120, None), + ]) + + async def test_retryable_provider_backoff_clears_after_success_with_display_role_override(self) -> None: + error = RetryableProviderError( + provider="openrouter", + provider_label="OpenRouter", + role_id="agg_val", + model="openrouter/model", + reason="transient_provider_error", + message="OpenRouter transient provider failure", + ) + + with mock.patch.object( + self.manager, + "_sleep_with_optional_stop", + new=mock.AsyncMock(), + ) as sleep_mock: + await self.manager.wait_for_retryable_provider_error( + error, + role_id="aggregator_validator", + ) + self.manager._clear_retryable_provider_backoff( + "openrouter", + "agg_val", + "openrouter/model", + ) + await self.manager.wait_for_retryable_provider_error( + error, + role_id="aggregator_validator", + ) + + sleep_mock.assert_has_awaits([ + mock.call(60, None), + mock.call(60, None), + ]) + + async def test_retryable_provider_backoff_stop_returns_without_cancellation(self) -> None: + error = RetryableProviderError( + provider="openrouter", + provider_label="OpenRouter", + role_id="agg_val", + model="openrouter/model", + reason="transient_provider_error", + message="OpenRouter transient provider failure", + ) + + await self.manager.wait_for_retryable_provider_error( + error, + should_stop=lambda: True, + ) + + self.assertEqual( + self.manager._retryable_provider_backoff_state[ + "openrouter|agg_val|openrouter/model|transient_provider_error" + ], + 1, + ) + + def test_transient_classifier_does_not_retry_sakana_auth_failure(self) -> None: + error = RuntimeError("Sakana Fugu request failed: HTTP 401: invalid api key") + + self.assertFalse(is_transient_model_call_error(error)) + + def test_transient_classifier_retries_sakana_server_failure(self) -> None: + error = RuntimeError("Sakana Fugu request failed: HTTP 503: service unavailable") + + self.assertTrue(is_transient_model_call_error(error)) + def test_provider_notification_preserves_cooldown_metadata(self) -> None: old_data_dir = system_config.data_dir with tempfile.TemporaryDirectory() as temp_dir: diff --git a/tests/test_proof_context_regressions.py b/tests/test_proof_context_regressions.py index 1f1cb8c..c866044 100644 --- a/tests/test_proof_context_regressions.py +++ b/tests/test_proof_context_regressions.py @@ -29,6 +29,7 @@ save_manual_compiler_prompt, ) from backend.shared.config import system_config +from backend.shared.api_client_manager import RetryableProviderError from backend.shared.models import ( ProofCandidate, ProofCheckRequest, @@ -1418,33 +1419,32 @@ async def record_failed_candidate(self, *_args, **_kwargs): stage._prepare_candidate = fake_prepare_candidate stage._run_smt_check = fake_smt_check try: - result = await stage.run( - content="brainstorm source", - source_type="brainstorm", - source_id="topic_001", - user_prompt="prove things", - submitter_model="model", - submitter_context=4000, - submitter_max_tokens=1000, - validator_model="validator", - validator_context=4000, - validator_max_tokens=1000, - broadcast_fn=broadcast, - novel_proofs_db=FakeProofDb(), - theorem_candidates=[candidate], - append_to_source=False, - checkpoint_callback=checkpoint, - ) + with self.assertRaises(RetryableProviderError) as exc: + await stage.run( + content="brainstorm source", + source_type="brainstorm", + source_id="topic_001", + user_prompt="prove things", + submitter_model="model", + submitter_context=4000, + submitter_max_tokens=1000, + validator_model="validator", + validator_context=4000, + validator_max_tokens=1000, + broadcast_fn=broadcast, + novel_proofs_db=FakeProofDb(), + theorem_candidates=[candidate], + append_to_source=False, + checkpoint_callback=checkpoint, + ) finally: proof_formalization_module.api_client_manager.generate_completion = old_generate_completion system_config.lean4_enabled = old_lean4_enabled - self.assertTrue(result.had_error) - self.assertIn("TRANSIENT PROVIDER ERROR", result.error_message) - self.assertEqual(result.total_candidates, 1) - self.assertIn("error", checkpoint_statuses) - self.assertIn("proof_check_complete", events) + self.assertIn("TRANSIENT PROVIDER ERROR", str(exc.exception)) + self.assertIn("provider_paused", checkpoint_statuses) self.assertNotIn("proof_attempts_exhausted", events) + self.assertNotIn("proof_check_complete", events) async def test_codex_transient_identification_error_does_not_mark_no_candidates(self): old_lean4_enabled = system_config.lean4_enabled @@ -1473,30 +1473,30 @@ class FakeProofDb: old_generate_completion = proof_identification_module.api_client_manager.generate_completion proof_identification_module.api_client_manager.generate_completion = raise_codex_gateway_timeout try: - result = await stage.run( - content="brainstorm source", - source_type="brainstorm", - source_id="topic_identification_timeout", - user_prompt="prove things", - submitter_model="model", - submitter_context=4000, - submitter_max_tokens=1000, - validator_model="validator", - validator_context=4000, - validator_max_tokens=1000, - broadcast_fn=broadcast, - novel_proofs_db=FakeProofDb(), - append_to_source=False, - checkpoint_callback=checkpoint, - ) + with self.assertRaises(RetryableProviderError) as exc: + await stage.run( + content="brainstorm source", + source_type="brainstorm", + source_id="topic_identification_timeout", + user_prompt="prove things", + submitter_model="model", + submitter_context=4000, + submitter_max_tokens=1000, + validator_model="validator", + validator_context=4000, + validator_max_tokens=1000, + broadcast_fn=broadcast, + novel_proofs_db=FakeProofDb(), + append_to_source=False, + checkpoint_callback=checkpoint, + ) finally: proof_identification_module.api_client_manager.generate_completion = old_generate_completion system_config.lean4_enabled = old_lean4_enabled - self.assertTrue(result.had_error) - self.assertIn("OpenAI Codex failed", result.error_message) - self.assertIn("error", checkpoint_statuses) - self.assertIn("proof_check_complete", events) + self.assertIn("OpenAI Codex failed", str(exc.exception)) + self.assertEqual(checkpoint_statuses, []) + self.assertNotIn("proof_check_complete", events) self.assertNotIn("proof_check_no_candidates", events) async def test_malformed_identification_output_does_not_mark_no_candidates(self): diff --git a/tests/test_response_extraction.py b/tests/test_response_extraction.py index f9f3ec7..8852e2c 100644 --- a/tests/test_response_extraction.py +++ b/tests/test_response_extraction.py @@ -62,6 +62,20 @@ def test_extracts_text_from_content_parts(self): self.assertEqual(text, "part one part two") + def test_parses_lm_studio_legacy_channel_json_after_private_thought(self): + text = ( + '<|channel>thought\n' + 'The model considered proof_044 and proof_011 first, with many ' + 'private notes containing non-json braces like {not valid json}.\n' + '{"selected_search_ids":["proof_044","proof_011"],' + '"reasoning":"Relevant modular certificate proofs."}' + ) + + parsed = parse_json(text) + + self.assertEqual(parsed["selected_search_ids"], ["proof_044", "proof_011"]) + self.assertEqual(parsed["reasoning"], "Relevant modular certificate proofs.") + if __name__ == "__main__": unittest.main()