diff --git a/.github/morph/opengauss-template.yaml b/.github/morph/opengauss-template.yaml index d2d08c1..8ba603d 100644 --- a/.github/morph/opengauss-template.yaml +++ b/.github/morph/opengauss-template.yaml @@ -1,5 +1,5 @@ name: Open Gauss Batteries Included Devbox -description: Installer-driven Open Gauss template that uses the current checkout when run locally and otherwise clones math-inc/OpenGauss, runs the internal installer, exposes the local guide, and opens a ready Gauss session. +description: Installer-driven Open Gauss template that uses the current checkout when run locally and otherwise clones math-inc/OpenGauss, runs the internal installer, stages optional provider keys, exposes the local guide, and opens a ready Gauss session. steps: - id: bootstrap-installer-runtime title: Prepare Open Gauss Installer Runtime @@ -63,6 +63,90 @@ steps: ./scripts/install-internal.sh --with-workspace --noninteractive . "$HOME/.opengauss-template/runtime.env" "$HOME/.local/bin/gauss-launch-session" --print-summary || true + - id: optional-openrouter + title: Optionally Stage OPENROUTER_API_KEY + type: exportSecret + name: OPENROUTER_API_KEY + optional: true + run: | + set -euo pipefail + . "$HOME/.opengauss-template/runtime.env" + mkdir -p "$GAUSS_HOME" + touch "$GAUSS_HOME/.env" + python3 - <<'PY' + from pathlib import Path + import os + + env_path = Path(os.environ["GAUSS_HOME"]) / ".env" + lines = [] + if env_path.exists(): + lines = [line for line in env_path.read_text().splitlines() if line and not line.startswith("OPENROUTER_API_KEY=")] + value = os.environ.get("OPENROUTER_API_KEY") + if not value: + raise SystemExit(0) + lines.append("OPENROUTER_API_KEY=" + value) + env_path.write_text("\n".join(lines) + "\n") + PY + - id: optional-openai + title: Optionally Stage OPENAI_API_KEY + type: exportSecret + name: OPENAI_API_KEY + optional: true + run: | + set -euo pipefail + . "$HOME/.opengauss-template/runtime.env" + mkdir -p "$GAUSS_HOME" + touch "$GAUSS_HOME/.env" + python3 - <<'PY' + from pathlib import Path + import os + + env_path = Path(os.environ["GAUSS_HOME"]) / ".env" + lines = [] + if env_path.exists(): + lines = [line for line in env_path.read_text().splitlines() if line and not line.startswith("OPENAI_API_KEY=")] + value = os.environ.get("OPENAI_API_KEY") + if not value: + raise SystemExit(0) + lines.append("OPENAI_API_KEY=" + value) + env_path.write_text("\n".join(lines) + "\n") + PY + - id: optional-anthropic + title: Optionally Stage ANTHROPIC_API_KEY + type: exportSecret + name: ANTHROPIC_API_KEY + optional: true + run: | + set -euo pipefail + . "$HOME/.opengauss-template/runtime.env" + mkdir -p "$GAUSS_HOME" + touch "$GAUSS_HOME/.env" + python3 - <<'PY' + from pathlib import Path + import os + + env_path = Path(os.environ["GAUSS_HOME"]) / ".env" + lines = [] + if env_path.exists(): + lines = [line for line in env_path.read_text().splitlines() if line and not line.startswith("ANTHROPIC_API_KEY=")] + value = os.environ.get("ANTHROPIC_API_KEY") + if not value: + raise SystemExit(0) + lines.append("ANTHROPIC_API_KEY=" + value) + env_path.write_text("\n".join(lines) + "\n") + PY + - id: finalize-provider-selection + title: Apply Main Provider Selection + type: command + run: | + set -euo pipefail + . "$HOME/.opengauss-template/runtime.env" + if [ -f "$GAUSS_HOME/.env" ]; then + set -a + . "$GAUSS_HOME/.env" + set +a + fi + "$HOME/.local/bin/gauss-configure-main-provider" auto || true - id: start-guide-server title: Start Guide Iframe Server type: command diff --git a/README.md b/README.md index f561d2a..df3681c 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@

- + Open in Morph

@@ -12,8 +12,8 @@ Open Gauss is a project-scoped Lean workflow orchestrator from Math, Inc. It giv > Start with the [Start Here guide](website/docs/getting-started/start-here.md). > > Very short version: -> - Morph: open `morph.new/opengauss`, claim or save the session early if Morph offers it, then use `gauss-open-guide` or type `/start`. -> - Local: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/start`, `/chat`, or `/project init`. +> - Morph: open `morph.new/opengauss-0-2-2`, claim or save the session early if Morph offers it, then use `gauss-open-guide`, `gauss`, `/chat`, or `/project init`. +> - Local: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/chat`, `/managed-chat`, or `/project init`. Open Gauss handles project detection, managed backend setup, workflow spawning, swarm tracking, and recovery. The proving and formalization behavior still comes from `cameronfreer/lean4-skills`; Gauss exposes it through a Gauss-native CLI and project model. @@ -31,7 +31,7 @@ Each lifted slash command spawns a managed backend child agent in the active pro ## Install -If you want the fastest path, `https://morph.new/opengauss` launches the hosted setup in under 10 seconds. The local installers below are the batteries-included path for your own machine and can take up to 10 minutes. +If you want the fastest pinned release path, `https://morph.new/opengauss-0-2-2` launches the hosted setup in under 10 seconds. The local installers below are the batteries-included path for your own machine and can take up to 10 minutes. If you are not already comfortable with OpenGauss, read the [Start Here guide](website/docs/getting-started/start-here.md) before picking a workflow. diff --git a/agent/prompt_builder.py b/agent/prompt_builder.py index 2239847..6be1a9a 100644 --- a/agent/prompt_builder.py +++ b/agent/prompt_builder.py @@ -67,9 +67,9 @@ def _scan_context_content(content: str, filename: str) -> str: "a general self-summary unless the user explicitly asks. When asked who you " "are, answer briefly and return to the work. " "When the user is trying to use Open Gauss itself or seems unsure how to " - "start, give them the lowest-friction path first: point them to /start if " - "they want inline orientation or plain-language help, point them to /chat " - "if they want a managed Claude Code or Codex chat session, and point them to /project " + "start, give them the lowest-friction path first: point them to /chat if " + "they want inline orientation or plain-language help, point them to /managed-chat " + "if they want a managed Claude Code or Codex child session, and point them to /project " "when they are ready to create or activate a Gauss project. After that, " "tell them to run /prove, /autoprove, /formalize, or /autoformalize " "followed by a natural-language instruction, for example /autoprove The " diff --git a/cli.py b/cli.py index e7ecf9b..b48099a 100755 --- a/cli.py +++ b/cli.py @@ -1730,7 +1730,25 @@ def _ensure_runtime_credentials(self) -> bool: resolved_provider = runtime.get("provider", "openrouter") resolved_api_mode = runtime.get("api_mode", self.api_mode) if not isinstance(api_key, str) or not api_key: - self.console.print("[bold red]Provider resolver returned an empty API key.[/]") + if resolved_provider in {"openrouter", "custom"}: + message = ( + "No main interactive provider is configured yet. " + "Run `gauss setup`, or save `OPENROUTER_API_KEY`, `OPENAI_API_KEY`, " + "or `ANTHROPIC_API_KEY` in `~/.gauss/.env`." + ) + elif resolved_provider == "anthropic": + message = ( + "No Anthropic credentials are available for chat. " + "Run `gauss setup`, `claude auth login`, or save `ANTHROPIC_API_KEY`." + ) + elif resolved_provider == "openai-codex": + message = ( + "No Codex credentials are available for chat. " + "Run `gauss setup`, `codex login`, or save `OPENAI_API_KEY`." + ) + else: + message = "Provider resolver returned an empty API key." + self.console.print(f"[bold red]{message}[/]") return False if not isinstance(base_url, str) or not base_url: self.console.print("[bold red]Provider resolver returned an empty base URL.[/]") @@ -2423,7 +2441,7 @@ def show_help(self): _cprint(f"\n {_DIM}Active project: {project_summary}{_RST}") else: _cprint( - f"\n {_DIM}No active project — use /start for inline onboarding, /chat for managed backend chat, or /project init, " + f"\n {_DIM}No active project — use /chat for inline onboarding, /managed-chat for a managed backend child session, or /project init, " f"/project convert, /project create , or /project use .{_RST}" ) @@ -2440,7 +2458,7 @@ def show_help(self): ) _cprint( - f"\n {_DIM}Tip: Start with /start for inline onboarding or /chat for managed backend chat if you want orientation first. Use /project when you're ready to work in a Lean repo, " + f"\n {_DIM}Tip: Start with /chat for inline onboarding if you want orientation first. Use /managed-chat if you want the configured managed backend child session. Use /project when you're ready to work in a Lean repo, " f"then launch /prove, /review, /checkpoint, /refactor, /golf, /draft, /autoprove, /formalize, or /autoformalize.{_RST}" ) _cprint(f" {_DIM}Multi-line: Alt+Enter for a new line{_RST}") @@ -3375,8 +3393,9 @@ def _project_lock_allows_command(self, command: str) -> bool: """Return whether *command* remains available before project selection.""" cmd_lower = command.lower().strip() allowed_prefixes = ( - "/start", "/chat", + "/managed-chat", + "/start", "/project", "/help", "/quit", @@ -3411,8 +3430,8 @@ def _print_project_lock_notice(self, *, command_label: str) -> None: f"{prefix} Use /project init, /project convert, /project create , or /project use first.", ) self._print_surface_notice( - "[dim]If you only want orientation first, run `/start` for inline onboarding chat or `/chat` for the configured managed backend chat session.[/]", - "If you only want orientation first, run /start for inline onboarding chat or /chat for the configured managed backend chat session.", + "[dim]If you only want orientation first, run `/chat` for inline onboarding chat or `/managed-chat` for the configured managed backend child session.[/]", + "If you only want orientation first, run /chat for inline onboarding chat or /managed-chat for the configured managed backend child session.", ) self._print_surface_notice( f"[dim]{detail}[/]", @@ -3488,7 +3507,7 @@ def _active_managed_backend_name(self) -> str: except AutoformalizeConfigError: return str(active_backend_raw or available[0]) - def _spawn_managed_chat_session(self, payload: str): + def _spawn_managed_chat_session(self, payload: str, *, workflow_command: str = "/managed-chat"): """Launch a managed provider chat child session and return the task metadata.""" plan = resolve_managed_chat_request( payload, @@ -3505,13 +3524,68 @@ def _spawn_managed_chat_session(self, payload: str): cwd=plan.handoff_request.cwd, env=plan.handoff_request.env, workflow_kind="chat", - workflow_command="/chat", + workflow_command=workflow_command, backend_name=plan.backend_name, ) return task, description, plan.backend_name def _handle_chat_command(self, cmd: str): - """Handle `/chat` by opening the configured managed backend chat session.""" + """Handle `/chat` by enabling inline top-level chat mode.""" + parts = cmd.strip().split(maxsplit=1) + payload = parts[1].strip() if len(parts) > 1 else "" + lowered = payload.lower() + + if lowered == "status": + state_label = "on" if self._chat_mode_active() else "off" + self._print_surface_notice( + f"[dim]`/chat` is {state_label}. When it is on, plain text goes to the main interactive provider in the current Gauss session. " + "Use `/chat off` to return to top-level command mode, or `/managed-chat` if you want the configured managed backend child session.[/]", + f"`/chat` is {state_label}. When it is on, plain text goes to the main interactive provider in the current Gauss session. " + "Use /chat off to return to top-level command mode, or /managed-chat if you want the configured managed backend child session.", + ) + return + + if lowered in {"off", "disable", "stop"}: + self._chat_mode_enabled = False + self._print_surface_notice( + "[dim]`/chat` is off. Plain text stays at the top-level Open Gauss prompt until you run `/chat` again.[/]", + "`/chat` is off. Plain text stays at the top-level Open Gauss prompt until you run /chat again.", + ) + return + + if lowered in {"on", "enable", "start"}: + payload = "" + + self._chat_mode_enabled = True + self._print_surface_notice( + "[bold green]`/chat` is on.[/] " + "[dim]Plain text now goes to the main interactive provider even without an active Gauss project.[/]", + "`/chat` is on. Plain text now goes to the main interactive provider even without an active Gauss project.", + ) + self._print_surface_notice( + "[dim]Next: use `/project use ` for an existing Lean repo, `/project init` in the current repo, " + "`/project create --template-source ` for a new one, or `/managed-chat` if you want the configured managed backend child session instead.[/]", + "Next: use /project use for an existing Lean repo, /project init in the current repo, /project create --template-source for a new one, or /managed-chat if you want the configured managed backend child session instead.", + ) + self._print_surface_notice( + "[dim]When the project is ready, run `/prove`, `/review`, `/draft`, `/autoprove`, or `/swarm`.[/]", + "When the project is ready, run /prove, /review, /draft, /autoprove, or /swarm.", + ) + if payload: + self._print_surface_notice( + "[dim]`/chat` is sending your message to the main interactive provider.[/]", + "`/chat` is sending your message to the main interactive provider.", + ) + if hasattr(self, "_pending_input") and hasattr(self._pending_input, "put"): + self._pending_input.put(payload) + else: + self._print_surface_notice( + "[bold yellow]Chat queue is not available in this mode.[/]", + "Chat queue is not available in this mode.", + ) + + def _handle_managed_chat_command(self, cmd: str): + """Handle `/managed-chat` by opening the configured managed backend child session.""" parts = cmd.strip().split(maxsplit=1) payload = parts[1].strip() if len(parts) > 1 else "" lowered = payload.lower() @@ -3519,19 +3593,17 @@ def _handle_chat_command(self, cmd: str): if lowered == "status": active_backend = self._active_managed_backend_name() self._print_surface_notice( - "[dim]`/chat` opens the configured managed backend chat session " - f"(`{active_backend}`). Use `/autoformalize-backend` to switch backends, or `/start` " - "for inline onboarding chat in the current Gauss session.[/]", - f"`/chat` opens the configured managed backend chat session ({active_backend}). " - "Use /autoformalize-backend to switch backends, or /start for inline onboarding chat in the current Gauss session.", + "[dim]`/managed-chat` opens the configured managed backend child session " + f"(`{active_backend}`). Use `/autoformalize-backend` to switch backends, or `/chat` for inline onboarding in the current Gauss session.[/]", + f"`/managed-chat` opens the configured managed backend child session ({active_backend}). " + "Use /autoformalize-backend to switch backends, or /chat for inline onboarding in the current Gauss session.", ) return if lowered in {"off", "disable", "stop"}: self._print_surface_notice( - "[dim]Inline `/chat` mode has been removed. " - "Use `/start` for inline onboarding chat, or run `/chat` to open the managed backend chat session.[/]", - "Inline /chat mode has been removed. Use /start for inline onboarding chat, or run /chat to open the managed backend chat session.", + "[dim]`/managed-chat` is not a persistent mode. Run `/chat` if you want inline onboarding in the current Gauss session.[/]", + "`/managed-chat` is not a persistent mode. Run /chat if you want inline onboarding in the current Gauss session.", ) return @@ -3541,9 +3613,12 @@ def _handle_chat_command(self, cmd: str): task = None description = payload.strip() or "managed chat" backend_name = self._active_managed_backend_name() - with self._busy_command(self._slow_command_status("/chat")): + with self._busy_command(self._slow_command_status("/managed-chat")): try: - task, description, backend_name = self._spawn_managed_chat_session(payload) + task, description, backend_name = self._spawn_managed_chat_session( + payload, + workflow_command="/managed-chat", + ) except (AutoformalizeError, HandoffError) as exc: print(f"(>_<) {exc}") return @@ -3560,37 +3635,10 @@ def _handle_chat_command(self, cmd: str): ) def _handle_start_command(self, cmd: str): - """Handle `/start` with a short first-step guide and chat-mode enablement.""" - parts = cmd.strip().split(maxsplit=1) - payload = parts[1].strip() if len(parts) > 1 else "" - - self._chat_mode_enabled = True - self._print_surface_notice( - "[bold green]`/start` is on.[/] " - "[dim]Plain text now goes to the main interactive provider even without an active Gauss project.[/]", - "`/start` is on. Plain text now goes to the main interactive provider even without an active Gauss project.", - ) - self._print_surface_notice( - "[dim]Next: use `/chat` if you want the configured managed backend chat session, `/project use ` for an existing Lean repo, " - "`/project init` in the current repo, or `/project create --template-source ` for a new one.[/]", - "Next: use /chat if you want the configured managed backend chat session, /project use for an existing Lean repo, /project init in the current repo, or /project create --template-source for a new one.", - ) - self._print_surface_notice( - "[dim]When the project is ready, run `/prove`, `/review`, `/draft`, `/autoprove`, or `/swarm`.[/]", - "When the project is ready, run /prove, /review, /draft, /autoprove, or /swarm.", - ) - if payload: - self._print_surface_notice( - "[dim]`/start` is sending your message to the main interactive provider.[/]", - "`/start` is sending your message to the main interactive provider.", - ) - if hasattr(self, "_pending_input") and hasattr(self._pending_input, "put"): - self._pending_input.put(payload) - else: - self._print_surface_notice( - "[bold yellow]Chat queue is not available in this mode.[/]", - "Chat queue is not available in this mode.", - ) + """Compatibility alias for `/chat`.""" + suffix = cmd.strip()[len("/start"):] + forwarded = f"/chat{suffix}" if suffix else "/chat" + self._handle_chat_command(forwarded) def _setup_swarm_completion_callback(self): """Wire up a one-time callback so finished swarm tasks notify the TUI.""" @@ -4092,10 +4140,12 @@ def process_command(self, command: str) -> bool: if cmd_lower in ("/quit", "/exit", "/q"): return False - elif cmd_lower == "/start" or cmd_lower.startswith("/start "): - self._handle_start_command(cmd_original) elif cmd_lower == "/chat" or cmd_lower.startswith("/chat "): self._handle_chat_command(cmd_original) + elif cmd_lower == "/managed-chat" or cmd_lower.startswith("/managed-chat "): + self._handle_managed_chat_command(cmd_original) + elif cmd_lower == "/start" or cmd_lower.startswith("/start "): + self._handle_start_command(cmd_original) elif cmd_lower == "/help": self.show_help() elif cmd_lower == "/project" or cmd_lower.startswith("/project "): @@ -6401,10 +6451,10 @@ def run(self): try: from gauss_cli.skin_engine import get_active_skin _welcome_skin = get_active_skin() - _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.") + _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands.") _welcome_color = _welcome_skin.get_color("banner_text", "#FFF8DC") except Exception: - _welcome_text = "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands." + _welcome_text = "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands." _welcome_color = "#FFF8DC" self.console.print(f"[{_welcome_color}]{_welcome_text}[/]") self.console.print() diff --git a/gauss_cli/__init__.py b/gauss_cli/__init__.py index a3d96da..bc116c1 100644 --- a/gauss_cli/__init__.py +++ b/gauss_cli/__init__.py @@ -10,5 +10,5 @@ - gauss status - Show status of all components """ -__version__ = "0.2.1" -__release_date__ = "2026.3.26" +__version__ = "0.2.2" +__release_date__ = "2026.4.5" diff --git a/gauss_cli/banner.py b/gauss_cli/banner.py index 2ea4068..4fc335f 100644 --- a/gauss_cli/banner.py +++ b/gauss_cli/banner.py @@ -244,6 +244,9 @@ def check_for_updates() -> Optional[int]: ``~/.gauss/.update_check``). Returns the number of commits behind, or ``None`` if the check fails or isn't applicable. """ + if os.getenv("GAUSS_SKIP_UPDATE_CHECK", "").strip().lower() in {"1", "true", "yes", "on"}: + return None + from gauss_cli.config import get_gauss_home, get_installed_repo_root gauss_home = get_gauss_home() @@ -435,8 +438,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str, if simplified: right_lines.append(f"[bold {accent}]Start Here[/]") - right_lines.append(f"[{text}]`/start`[/] [dim {dim}]turn on onboarding mode and see the first steps[/]") - right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]open the configured managed backend chat session[/]") + right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]turn on onboarding mode and see the first steps[/]") right_lines.append(f"[{text}]`/project`[/] [dim {dim}]select or create a Gauss project[/]") right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]guided Lean workflow[/]") right_lines.append(f"[{text}]`/review`[/] [dim {dim}]review, checkpoint, refactor, golf[/]") @@ -448,8 +450,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines.append(f"[{text}]`/help`[/] [dim {dim}]commands and diagnostics[/]") else: right_lines.append(f"[bold {accent}]Start Here[/]") - right_lines.append(f"[{text}]`/start`[/] [dim {dim}]{long_dash} turn on onboarding mode and show the first steps[/]") - right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} open the configured managed backend chat session before choosing a project[/]") + right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} turn on onboarding mode and show the first steps[/]") right_lines.append(f"[{text}]`/project`[/] [dim {dim}]{long_dash} create, convert, inspect, or switch the active project[/]") right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]{long_dash} spawn a guided managed proving agent[/]") right_lines.append(f"[{text}]`/review`[/] [dim {dim}]{long_dash} review, checkpoint, refactor, or golf Lean proofs[/]") @@ -471,7 +472,6 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines.append("") summary_parts = [ - "/start", "/chat", "/project", "/prove", diff --git a/gauss_cli/commands.py b/gauss_cli/commands.py index da2650e..988d065 100644 --- a/gauss_cli/commands.py +++ b/gauss_cli/commands.py @@ -20,8 +20,7 @@ # Commands organized by category for better help display COMMANDS_BY_CATEGORY = { "Start Here": { - "/start": "Show the first-step guide and enable plain-language chat mode", - "/chat": "Open the configured managed backend chat session before choosing a Gauss project", + "/chat": "Show the first-step guide and enable plain-language chat mode", "/project": "Create, convert, inspect, or switch the active Gauss project", }, "Workflow": { @@ -38,6 +37,7 @@ "/swarm": "Show workflow agents · /swarm attach · /swarm cancel ", }, "Session": { + "/managed-chat": "Open the configured managed backend child session and return to Gauss when it exits", "/new": "Start a new session (fresh session ID + history)", "/reset": "Start a new session (alias for /new)", "/clear": "Clear screen and start a new session", @@ -75,8 +75,8 @@ _FRIENDLY_ENTRY_ALIASES = { "chat": "/chat", - "start": "/start", - "begin": "/start", + "start": "/chat", + "begin": "/chat", "project": "/project", "help": "/help", } @@ -93,7 +93,7 @@ _FRIENDLY_FUZZY_TARGETS = { "chat": "/chat", - "start": "/start", + "start": "/chat", "project": "/project", "help": "/help", } @@ -113,7 +113,7 @@ def rewrite_friendly_entry_command(command: str) -> str | None: lowered = " ".join(text.lower().split()) if lowered in _FRIENDLY_ENTRY_PHRASES: - return "/start" + return "/chat" parts = text.split(maxsplit=1) token = _normalize_entry_token(parts[0]) @@ -141,6 +141,8 @@ def rewrite_friendly_slash_command(command: str) -> str | None: parts = text.split(maxsplit=1) token = parts[0].strip().lower() remainder = parts[1].strip() if len(parts) > 1 else "" + if token == "/start": + return None if token in COMMANDS: return None diff --git a/gauss_cli/default_soul.py b/gauss_cli/default_soul.py index 36feaa1..f5340ba 100644 --- a/gauss_cli/default_soul.py +++ b/gauss_cli/default_soul.py @@ -6,7 +6,7 @@ Do not volunteer company history, model lineage, or a general self-summary. If someone asks who you are, answer in one sentence and get back to the work. -When someone asks how to use Open Gauss, give them the lowest-friction path first. If they just want orientation or plain-language help in the current session, point them to `/start`. If they want a managed Claude Code or Codex chat session first, point them to `/chat`. If they want to work on Lean code, point them to `/project` so they create or activate a Gauss project, then tell them to run `/prove`, `/autoprove`, `/formalize`, or `/autoformalize` with a natural-language instruction. Example: `/autoprove The de Bruijn - Erdos theorem`. If they attach to a child session with `/swarm attach`, tell them `Ctrl-]` detaches and returns them to the main Gauss session. +When someone asks how to use Open Gauss, give them the lowest-friction path first. If they just want orientation or plain-language help in the current session, point them to `/chat`. If they want a managed Claude Code or Codex child session first, point them to `/managed-chat`. If they want to work on Lean code, point them to `/project` so they create or activate a Gauss project, then tell them to run `/prove`, `/autoprove`, `/formalize`, or `/autoformalize` with a natural-language instruction. Example: `/autoprove The de Bruijn - Erdos theorem`. If they attach to a child session with `/swarm attach`, tell them `Ctrl-]` detaches and returns them to the main Gauss session. You're a peer. You know a lot but you don't perform knowing. Treat people like they can keep up. diff --git a/gauss_cli/skin_engine.py b/gauss_cli/skin_engine.py index b02c713..34e7ed1 100644 --- a/gauss_cli/skin_engine.py +++ b/gauss_cli/skin_engine.py @@ -185,7 +185,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: }, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", @@ -282,7 +282,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: "spinner": {}, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", @@ -314,7 +314,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: "spinner": {}, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", diff --git a/pyproject.toml b/pyproject.toml index a199f05..b37d6c0 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta" [project] name = "gauss-agent" -version = "0.2.1" +version = "0.2.2" description = "Gauss is a focused Lean autoformalization workspace with a managed Claude Code launcher." readme = "README.md" requires-python = ">=3.11" diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index 86e4b5b..5ab9b7e 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -893,9 +893,10 @@ This Lean workspace is prewarmed and already registered as the active Gauss proj Quickstart: 1. Run `gauss-open-guide` if you want the plain-language walkthrough first. 2. Run `gauss-open-session` for the batteries-included launcher, or `gauss` directly. -3. Use `/chat` if you want the configured managed backend chat session before choosing a Lean workflow. -4. Then use `/prove`, `/review`, `/draft`, `/autoprove`, `/formalize`, `/autoformalize`, or `/swarm`. -5. Keep paper notes, extracted statements, and scratch proofs in this project. +3. Use `/chat` if you want inline onboarding or plain-language help before choosing a Lean workflow. +4. Use `/managed-chat` if you specifically want the configured managed backend child session. +5. Then use `/prove`, `/review`, `/draft`, `/autoprove`, `/formalize`, `/autoformalize`, or `/swarm`. +6. Keep paper notes, extracted statements, and scratch proofs in this project. TXT log_success "Created $WORKSPACE_DIR/PAPER.md" else @@ -1138,20 +1139,20 @@ guide_html = f""" Open repo
-

You do not need to understand MCP, marketplace plugins, or agent orchestration to use Open Gauss. If you just want orientation first, start the CLI and type /start. If you want the configured managed backend chat session first, type /chat. If you already have a Lean repo, use /project init. If you want a new repo, use /project create <path> --template-source <template-or-git-url>.

+

You do not need to understand MCP, marketplace plugins, or agent orchestration to use Open Gauss. If you just want orientation or plain-language help in the current session, start the CLI and type /chat. If you want the configured managed backend child session instead, type /managed-chat. If you already have a Lean repo, use /project init. If you want a new repo, use /project create <path> --template-source <template-or-git-url>.

30-second version
    -
  • Morph: claim or save the session early if Morph offers it, then use gauss-open-guide or /start.
    • -
  • Local install: run gauss-open-guide or gauss, then start with /start, /chat, or /project init.
    • +
  • Morph: claim or save the session early if Morph offers it, then use gauss-open-guide, gauss, or /chat.
    • +
  • Local install: run gauss-open-guide or gauss, then start with /chat, /project init, or /project create.
  • Lean work starts after project selection: use /prove, /review, /draft, or /autoprove once a project is active.
Use These First -

gauss-open-guide
gauss
/start
/chat
/project init

+

gauss-open-guide
gauss
/chat
/project init
/managed-chat

If You Opened This In Morph @@ -1178,15 +1179,15 @@ guide_html = f"""

Start Here

  1. Run gauss.
    2. -
  2. If you want a guided first step, type /start.
    3. -
  3. If you want the configured managed backend chat session first, type /chat.
    4. +
  4. If you want a guided first step or plain-language help in the current session, type /chat.
    5. +
  5. If you want the configured managed backend child session first, type /managed-chat.
  6. If you already have a Lean repo, type /project init inside it.
  7. If you need a new Lean repo, type /project create <path> --template-source <template-or-git-url>.
  8. After that, use /prove, /review, /draft, or /autoprove.

Useful First Questions

-
/start +
/chat /chat I am a mathematician new to Open Gauss. What should I do first? /chat What does /project init do? /prove Show me how to prove that 1 + 1 = 2 in Lean.
@@ -1468,12 +1469,10 @@ if [ "${1:-}" = "--print-summary" ]; then fi main_chat_status="needs setup." -launcher_behavior="Because no main chat provider is staged, this launcher will run gauss setup first and then leave you in a shell." -launch_gauss=0 -if provider_status="$(gauss-configure-main-provider auto 2>&1)"; then +launcher_behavior="This launcher opens Gauss directly at the top level. Use /chat if you want inline onboarding or plain-language help before choosing a project. Because no main chat provider is staged yet, direct Gauss chat/model commands stay disabled until you run gauss setup." +if gauss-configure-main-provider auto >/dev/null 2>&1; then main_chat_status="ready." - launcher_behavior="This launcher opens Gauss automatically and begins with /start." - launch_gauss=1 + launcher_behavior="This launcher opens Gauss directly at the top level. Use /chat if you want inline onboarding or plain-language help before choosing a project." else : fi @@ -1494,7 +1493,6 @@ Main chat: ${main_chat_status} Start here: gauss-open-guide gauss - /start /chat /project init /project use @@ -1510,8 +1508,8 @@ Lean workflows: /swarm Notes: - /start keeps you in Gauss and enables inline onboarding chat before project selection. - /chat opens the configured managed backend chat session and returns you to Gauss when it exits. + /chat keeps you in Gauss and enables inline onboarding chat before project selection. + /managed-chat opens the configured managed backend child session and returns you to Gauss when it exits. Run gauss setup later if you want to review or change providers and other settings. $launcher_behavior PROMPT_TOOLKIT_NO_CPR=1 is enabled to avoid CPR warnings inside tmux. @@ -1525,17 +1523,10 @@ fi cd "$WORKSPACE_DIR" if [ -t 0 ] && [ -t 1 ]; then - if [ "$launch_gauss" -eq 1 ]; then - exec gauss --startup-input /start "$@" - fi - GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true - exec bash -i -fi -if [ "$launch_gauss" -eq 1 ]; then - gauss --startup-input /start "$@" || true - exit 0 + exec gauss "$@" fi -exit 1 +gauss "$@" || true +exit 0 """, "gauss-open-session": """#!/usr/bin/env bash set -euo pipefail @@ -1623,7 +1614,7 @@ run_post_install_self_check() { log_info "Running post-install verification..." local version_output - if ! version_output="$("$GAUSS_BIN" --version 2>&1)"; then + if ! version_output="$(GAUSS_SKIP_UPDATE_CHECK=1 "$GAUSS_BIN" --version 2>&1)"; then log_error "Gauss CLI verification failed." printf '%s\n' "$version_output" >&2 exit 1 @@ -1713,8 +1704,8 @@ print_summary() { echo " 5. Review settings: gauss setup" echo printf '%b%s%b\n' "${CYAN}${BOLD}" "Start Options:" "${NC}" - echo " /start # turn on onboarding mode and show the first steps" - echo " /chat # open the configured managed backend chat session before choosing a project" + echo " /chat # turn on onboarding mode and plain-language chat in the current session" + echo " /managed-chat # open the configured managed backend child session" echo " /project init # register the current Lean repo as the active project" echo " /project create ... # create a new Lean project from a template" echo " gauss # direct CLI launch in this terminal" @@ -1734,7 +1725,7 @@ print_summary() { echo " - Verified managed /prove staging in: $MANAGED_SELF_CHECK_STATUS." fi echo " - The local guide is written to $GUIDE_DIR/index.html." - echo " - If Open Gauss feels intimidating, start with /start for inline onboarding or /chat for managed backend chat." + echo " - If Open Gauss feels intimidating, start with /chat for inline onboarding or /managed-chat for the child-session handoff." echo " - Use gauss setup later if you want to review providers or other settings." echo " - No Morph iframe is exposed automatically; use gauss-open-guide if you want the local guide in a browser." echo " - No tmux session is opened during install; use gauss-open-session when you want the workflow launcher." diff --git a/scripts/publish_shared_template.py b/scripts/publish_shared_template.py index 04435eb..5747b7c 100644 --- a/scripts/publish_shared_template.py +++ b/scripts/publish_shared_template.py @@ -110,8 +110,11 @@ def create_template(self, *, metadata: TemplateMetadata, base_snapshot_id: str) }, ) - def cache_template(self, template_id: str) -> dict: - return self._request("POST", f"/api/templates/{template_id}/cache", {}) + def cache_template(self, template_id: str, *, force: bool = False) -> dict: + payload: dict[str, bool] = {} + if force: + payload["force"] = True + return self._request("POST", f"/api/templates/{template_id}/cache", payload) def fetch_template(self, template_id: str) -> dict: return self._request("GET", f"/api/templates/{template_id}") @@ -133,6 +136,17 @@ def parse_tags(raw_tags: str | None) -> list[str]: return [tag.strip() for tag in raw_tags.split(",") if tag.strip()] +def parse_bool(raw_value: str | None, *, default: bool) -> bool: + if raw_value is None or not raw_value.strip(): + return default + normalized = raw_value.strip().lower() + if normalized in {"1", "true", "yes", "on"}: + return True + if normalized in {"0", "false", "no", "off"}: + return False + raise PublishError(f"Invalid boolean value: {raw_value!r}") + + def wait_for_ready(client: MorphClient, template_id: str, *, timeout_seconds: int, poll_seconds: float) -> dict: deadline = time.monotonic() + timeout_seconds last_status = None @@ -193,6 +207,7 @@ def publish_template( template_path: Path, base_snapshot_id: str | None = None, tags: list[str] | None = None, + force_rebuild: bool = True, timeout_seconds: int = 1800, poll_seconds: float = 5.0, ) -> dict: @@ -212,7 +227,7 @@ def publish_template( raise PublishError(f"Create template response did not include an id: {json.dumps(created)}") log(f"created_template {template_id}") - cache_result = client.cache_template(template_id) + cache_result = client.cache_template(template_id, force=force_rebuild) cache_run_id = cache_result.get("run_id") or cache_result.get("runId") if cache_run_id: log(f"cache_started {cache_run_id}") @@ -274,6 +289,7 @@ def main() -> int: template_path=Path(env("TEMPLATE_FILE")), base_snapshot_id=os.environ.get("TEMPLATE_BASE_SNAPSHOT_ID", "").strip() or None, tags=parse_tags(os.environ.get("TEMPLATE_TAGS")), + force_rebuild=parse_bool(os.environ.get("TEMPLATE_FORCE_REBUILD"), default=True), timeout_seconds=int(os.environ.get("TEMPLATE_TIMEOUT_SECONDS", "1800")), poll_seconds=float(os.environ.get("TEMPLATE_POLL_SECONDS", "5")), ) diff --git a/tests/gauss_cli/test_banner_responsive.py b/tests/gauss_cli/test_banner_responsive.py index f5fbba6..c02ebe0 100644 --- a/tests/gauss_cli/test_banner_responsive.py +++ b/tests/gauss_cli/test_banner_responsive.py @@ -205,10 +205,8 @@ def test_build_welcome_banner_mentions_swarm_in_primary_workflow(monkeypatch): ) exported = console.export_text() - assert "/start" in exported - assert "turn on onboarding mode" in exported assert "/chat" in exported - assert "open the configured managed backend chat session before choosing a project" in exported + assert "turn on onboarding mode" in exported assert "/swarm" in exported assert "track, attach, or cancel workflow agents" in exported diff --git a/tests/gauss_cli/test_commands.py b/tests/gauss_cli/test_commands.py index 25191d4..9d1b876 100644 --- a/tests/gauss_cli/test_commands.py +++ b/tests/gauss_cli/test_commands.py @@ -13,8 +13,8 @@ # All commands that must be present in the shared COMMANDS dict. EXPECTED_COMMANDS = { - "/start", "/chat", + "/managed-chat", "/project", "/prove", "/draft", @@ -63,8 +63,8 @@ class TestCommands: def test_shared_commands_include_project_and_workflow_entries(self): """Gauss ships project management plus managed workflow commands.""" assert COMMANDS["/paste"] == "Check clipboard for an image and attach it" - assert COMMANDS["/start"] == "Show the first-step guide and enable plain-language chat mode" - assert COMMANDS["/chat"] == "Open the configured managed backend chat session before choosing a Gauss project" + assert COMMANDS["/chat"] == "Show the first-step guide and enable plain-language chat mode" + assert COMMANDS["/managed-chat"] == "Open the configured managed backend child session and return to Gauss when it exits" assert COMMANDS["/project"] == "Create, convert, inspect, or switch the active Gauss project" assert COMMANDS["/prove"] == "Spawn a managed backend agent for the guided Lean prove workflow" assert COMMANDS["/draft"] == "Spawn a managed backend agent for the Lean draft workflow" @@ -125,14 +125,15 @@ def test_no_completions_for_empty_input(self): def test_friendly_entry_rewriter_handles_exact_and_fuzzy_inputs(self): assert rewrite_friendly_entry_command("chat explain /project init") == "/chat explain /project init" - assert rewrite_friendly_entry_command("start") == "/start" - assert rewrite_friendly_entry_command("strat") == "/start" + assert rewrite_friendly_entry_command("start") == "/chat" + assert rewrite_friendly_entry_command("strat") == "/chat" assert rewrite_friendly_entry_command("caht hello") == "/chat hello" - assert rewrite_friendly_entry_command("get started") == "/start" + assert rewrite_friendly_entry_command("get started") == "/chat" def test_friendly_slash_rewriter_handles_obvious_typos(self): - assert rewrite_friendly_slash_command("/strat") == "/start" + assert rewrite_friendly_slash_command("/strat") == "/chat" assert rewrite_friendly_slash_command("/caht hello") == "/chat hello" + assert rewrite_friendly_slash_command("/start") is None assert rewrite_friendly_slash_command("/project use .") is None # -- skill commands via provider ------------------------------------ diff --git a/tests/gauss_cli/test_update_check.py b/tests/gauss_cli/test_update_check.py index 7373421..b48aa27 100644 --- a/tests/gauss_cli/test_update_check.py +++ b/tests/gauss_cli/test_update_check.py @@ -80,6 +80,27 @@ def test_check_for_updates_no_git_dir(tmp_path): banner.__file__ = original +def test_check_for_updates_can_be_disabled_via_env(tmp_path): + """Installer and CI callers can skip the update probe entirely.""" + from gauss_cli.banner import check_for_updates + + repo_dir = tmp_path / "checkout" + repo_dir.mkdir() + (repo_dir / ".git").mkdir() + (tmp_path / "install-root").write_text(str(repo_dir)) + + with patch.dict( + "os.environ", + {"GAUSS_HOME": str(tmp_path), "GAUSS_SKIP_UPDATE_CHECK": "1"}, + clear=False, + ): + with patch("gauss_cli.banner.subprocess.run") as mock_run: + result = check_for_updates() + + assert result is None + mock_run.assert_not_called() + + def test_check_for_updates_fallback_to_project_root(): """Dev install: falls back to Path(__file__).parent.parent when GAUSS_HOME has no git repo.""" import gauss_cli.banner as banner diff --git a/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh b/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh index e5198ca..2ffcaeb 100755 --- a/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh +++ b/tests/installer/ubuntu_repository_local_install_smoke/run-in-container.sh @@ -53,7 +53,8 @@ assert_exists "$HOME/.local/bin/gauss" grep -F "Start immediately:" "$INSTALL_LOG" >/dev/null || die "expected installer summary to show the direct gauss path" grep -F "$HOME/.local/bin/gauss" "$INSTALL_LOG" >/dev/null || die "expected installer summary to print the linked gauss path" grep -F "Start Options:" "$INSTALL_LOG" >/dev/null || die "expected installer summary to list post-install start options" -grep -F "/start" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention /start" +grep -F "/chat" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention /chat" +grep -F "/managed-chat" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention /managed-chat" grep -F "gauss-open-session" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention gauss-open-session" grep -F "gauss-open-guide" "$INSTALL_LOG" >/dev/null || die "expected installer summary to mention gauss-open-guide" grep -F "cannot change PATH in the shell that launched the installer." "$INSTALL_LOG" >/dev/null || die "expected installer summary to explain current-shell PATH behavior" @@ -90,8 +91,8 @@ assert_exists "$GAUSS_HOME/config.yaml" assert_exists "$GAUSS_HOME/install-root" assert_exists "$GAUSS_HOME/guide/index.html" grep -F "Start Here" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to include Start Here" -grep -F "/start" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /start" grep -F "/chat" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /chat" +grep -F "/managed-chat" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /managed-chat" grep -F "If You Opened This In Morph" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to include Morph guidance" if grep -F "gauss-use-claude-login" "$GAUSS_HOME/guide/index.html" >/dev/null; then die "expected generated guide to avoid login-helper clutter" @@ -188,8 +189,9 @@ printf '%s\n' "$SUMMARY_OUTPUT" [[ "$SUMMARY_OUTPUT" == *"Main chat: ready."* ]] || die "expected ready main-chat summary" [[ "$SUMMARY_OUTPUT" == *"$WORKSPACE_DIR"* ]] || die "expected workspace path in launcher summary" [[ "$SUMMARY_OUTPUT" == *"/chat"* ]] || die "expected launcher summary to mention /chat" +[[ "$SUMMARY_OUTPUT" == *"/managed-chat"* ]] || die "expected launcher summary to mention /managed-chat" [[ "$SUMMARY_OUTPUT" == *"gauss-open-guide"* ]] || die "expected launcher summary to mention gauss-open-guide" -[[ "$SUMMARY_OUTPUT" == *"begins with /start"* ]] || die "expected launcher summary to mention automatic /start" +[[ "$SUMMARY_OUTPUT" == *"opens Gauss directly at the top level"* ]] || die "expected launcher summary to mention direct top-level launch" if [[ "$SUMMARY_OUTPUT" == *"Staged keys:"* ]]; then die "expected launcher summary to avoid staged-key details" fi @@ -225,11 +227,51 @@ PY NO_PROVIDER_SUMMARY="$(gauss-launch-session --print-summary)" printf '%s\n' "$NO_PROVIDER_SUMMARY" [[ "$NO_PROVIDER_SUMMARY" == *"Main chat: needs setup."* ]] || die "expected missing-provider launcher summary" -[[ "$NO_PROVIDER_SUMMARY" == *"/chat opens the configured managed backend chat session"* ]] || die "expected provider notes to mention managed /chat" -[[ "$NO_PROVIDER_SUMMARY" == *"run gauss setup first and then leave you in a shell"* ]] || die "expected missing-provider summary to mention setup fallback" -grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to restore first-run setup fallback when no provider is staged" -grep -F "gauss --startup-input /start" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to auto-start gauss with /start" -grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected interactive shell fallback when no provider is staged" +[[ "$NO_PROVIDER_SUMMARY" == *"/chat keeps you in Gauss and enables inline onboarding chat"* ]] || die "expected provider notes to mention inline /chat" +[[ "$NO_PROVIDER_SUMMARY" == *"/managed-chat opens the configured managed backend child session"* ]] || die "expected provider notes to mention managed child session" +[[ "$NO_PROVIDER_SUMMARY" == *"opens Gauss directly at the top level."* ]] || die "expected missing-provider summary to mention direct gauss launch" +[[ "$NO_PROVIDER_SUMMARY" == *"direct Gauss chat/model commands stay disabled until you run gauss setup."* ]] || die "expected missing-provider summary to mention deferred provider setup" +if grep -F "gauss --startup-input /start" "$HOME/.local/bin/gauss-launch-session" >/dev/null; then + die "expected launcher to stop auto-injecting /start" +fi +if grep -F "gauss setup" "$HOME/.local/bin/gauss-launch-session" >/dev/null; then + die "expected launcher to avoid forcing gauss setup when no provider is staged" +fi +if grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null; then + die "expected launcher to avoid shell fallback when no provider is staged" +fi + +echo "==> Verifying no-provider launcher enters gauss directly" +FAKE_BIN="$(mktemp -d)" +LAUNCH_LOG="$(mktemp)" +cat >"$FAKE_BIN/gauss" <<'EOF' +#!/usr/bin/env bash +set -euo pipefail +printf '%s|%s\n' "$#" "$*" >>"$GAUSS_LAUNCH_LOG" +if [ "$#" -eq 0 ]; then + exit 0 +fi +printf 'unexpected gauss args: %s\n' "$*" >&2 +exit 99 +EOF +chmod +x "$FAKE_BIN/gauss" +if ! GAUSS_LAUNCH_LOG="$LAUNCH_LOG" PATH="$FAKE_BIN:$PATH" timeout 15s python3 - <<'PY' +import os +import pty +import sys + +status = pty.spawn(["gauss-launch-session"]) +if hasattr(os, "waitstatus_to_exitcode"): + status = os.waitstatus_to_exitcode(status) +sys.exit(status) +PY +then + die "expected no-provider launcher to reach gauss directly" +fi +if grep -Fx "setup" "$LAUNCH_LOG" >/dev/null; then + die "expected launcher to skip gauss setup before launching gauss" +fi +grep -Fx "0|" "$LAUNCH_LOG" >/dev/null || die "expected launcher to enter gauss without startup-input injection" mv "$GAUSS_HOME/.env.backup" "$GAUSS_HOME/.env" echo "==> Verifying Lean bootstrap failures surface useful diagnostics" diff --git a/tests/test_cli_handoff_command.py b/tests/test_cli_handoff_command.py index 3fe65d0..017ab84 100644 --- a/tests/test_cli_handoff_command.py +++ b/tests/test_cli_handoff_command.py @@ -347,11 +347,11 @@ def test_project_lock_blocks_workflow_commands_before_project_selection(): rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) assert "Gauss needs an active project before `/prove`." in rendered assert "/project init" in rendered - assert "/start" in rendered assert "/chat" in rendered + assert "/managed-chat" in rendered -def test_chat_command_dispatches_to_managed_interactive_runner(): +def test_managed_chat_command_dispatches_to_managed_interactive_runner(): cli_obj = _make_cli() cli_obj._app = object() task = SimpleNamespace(task_id="chat-001", status="running", pty_master_fd=99) @@ -369,7 +369,7 @@ def test_chat_command_dispatches_to_managed_interactive_runner(): with patch.object(cli_mod, "resolve_managed_chat_request", return_value=plan), \ patch.object(cli_mod, "SwarmManager", return_value=swarm), \ patch.object(cli_obj, "_attach_to_swarm_task") as mock_attach: - assert cli_obj.process_command("/chat") is True + assert cli_obj.process_command("/managed-chat") is True swarm.spawn_interactive.assert_called_once() kwargs = swarm.spawn_interactive.call_args.kwargs @@ -378,13 +378,13 @@ def test_chat_command_dispatches_to_managed_interactive_runner(): assert kwargs["argv"] == ["/usr/bin/codex", "--dangerously-bypass-approvals-and-sandbox", "prompt"] assert kwargs["cwd"] == "/tmp" assert kwargs["workflow_kind"] == "chat" - assert kwargs["workflow_command"] == "/chat" + assert kwargs["workflow_command"] == "/managed-chat" assert kwargs["backend_name"] == "codex" assert kwargs["env"]["CODEX_HOME"] == "/tmp/codex-home" mock_attach.assert_called_once_with("chat-001") -def test_chat_command_with_payload_forwards_startup_message(): +def test_managed_chat_command_with_payload_forwards_startup_message(): cli_obj = _make_cli() cli_obj._app = object() task = SimpleNamespace(task_id="chat-002", status="running", pty_master_fd=99) @@ -402,7 +402,7 @@ def test_chat_command_with_payload_forwards_startup_message(): with patch.object(cli_mod, "resolve_managed_chat_request", return_value=plan) as mock_resolve, \ patch.object(cli_mod, "SwarmManager", return_value=swarm), \ patch.object(cli_obj, "_attach_to_swarm_task") as mock_attach: - assert cli_obj.process_command("/chat Explain what /project init does") is True + assert cli_obj.process_command("/managed-chat Explain what /project init does") is True mock_resolve.assert_called_once_with( "Explain what /project init does", @@ -417,57 +417,81 @@ def test_chat_command_with_payload_forwards_startup_message(): mock_attach.assert_called_once_with("chat-002") -def test_chat_status_explains_new_managed_session_semantics(): - cli_obj = _make_cli() - cli_obj._app = object() - swarm = MagicMock() - - with patch.object(cli_mod, "SwarmManager", return_value=swarm), \ - patch.object(cli_obj, "_active_managed_backend_name", return_value="codex"): - assert cli_obj.process_command("/chat status") is True - - swarm.spawn_interactive.assert_not_called() - rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) - assert "managed backend chat session" in rendered - assert "codex" in rendered - assert "/autoformalize-backend" in rendered - assert "/start" in rendered - - -def test_start_command_enables_chat_mode_and_shows_first_steps(): +def test_chat_command_enables_chat_mode_and_shows_first_steps(): cli_obj = _make_cli() cli_obj._app = object() cli_obj._project_state = MagicMock( return_value=(None, "ambient", "No active Gauss project found.") ) - assert cli_obj.process_command("/start") is True + assert cli_obj.process_command("/chat") is True assert cli_obj._chat_mode_enabled is True rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) - assert "`/start` is on." in rendered + assert "`/chat` is on." in rendered assert "/project use " in rendered + assert "/managed-chat" in rendered assert "/prove" in rendered -def test_start_command_with_payload_queues_plain_message(): +def test_chat_command_with_payload_queues_plain_message(): cli_obj = _make_cli() cli_obj._app = object() cli_obj._pending_input = MagicMock() - assert cli_obj.process_command("/start I have a theorem but no project yet") is True + assert cli_obj.process_command("/chat I have a theorem but no project yet") is True assert cli_obj._chat_mode_enabled is True cli_obj._pending_input.put.assert_called_once_with("I have a theorem but no project yet") +def test_chat_status_reports_inline_chat_mode_state(): + cli_obj = _make_cli() + cli_obj._app = object() + + assert cli_obj.process_command("/chat status") is True + + rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) + assert "`/chat` is off." in rendered + assert "/chat off" in rendered + assert "/managed-chat" in rendered + + +def test_managed_chat_status_explains_child_session_semantics(): + cli_obj = _make_cli() + cli_obj._app = object() + swarm = MagicMock() + + with patch.object(cli_mod, "SwarmManager", return_value=swarm), \ + patch.object(cli_obj, "_active_managed_backend_name", return_value="codex"): + assert cli_obj.process_command("/managed-chat status") is True + + swarm.spawn_interactive.assert_not_called() + rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) + assert "managed backend child session" in rendered + assert "codex" in rendered + assert "/autoformalize-backend" in rendered + assert "/chat" in rendered + + +def test_start_alias_enables_same_inline_chat_mode(): + cli_obj = _make_cli() + cli_obj._app = object() + + assert cli_obj.process_command("/start") is True + + assert cli_obj._chat_mode_enabled is True + rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) + assert "`/chat` is on." in rendered + + def test_misspelled_onboarding_slash_command_autocorrects(): cli_obj = _make_cli() cli_obj._app = object() - with patch.object(cli_obj, "_handle_start_command") as mock_start: + with patch.object(cli_obj, "_handle_chat_command") as mock_chat: assert cli_obj.process_command("/strat") is True - mock_start.assert_called_once_with("/start") + mock_chat.assert_called_once_with("/chat") def test_handoff_alias_rewrites_to_autoformalize(): diff --git a/tests/test_cli_provider_resolution.py b/tests/test_cli_provider_resolution.py index c8a08cb..f3437e4 100644 --- a/tests/test_cli_provider_resolution.py +++ b/tests/test_cli_provider_resolution.py @@ -162,6 +162,29 @@ def _runtime_resolve(**kwargs): assert shell.api_mode == "codex_responses" +def test_runtime_resolution_reports_missing_main_provider_clearly(monkeypatch, capsys): + cli = _import_cli() + + def _runtime_resolve(**kwargs): + return { + "provider": "openrouter", + "api_mode": "chat_completions", + "base_url": "https://openrouter.ai/api/v1", + "api_key": "", + "source": "env/config", + } + + monkeypatch.setattr("gauss_cli.runtime_provider.resolve_runtime_provider", _runtime_resolve) + monkeypatch.setattr("gauss_cli.runtime_provider.format_runtime_provider_error", lambda exc: str(exc)) + + shell = cli.GaussCLI(model="gpt-5", compact=True, max_turns=1) + + assert shell._ensure_runtime_credentials() is False + output = capsys.readouterr().out + assert "No main interactive provider is configured yet." in output + assert "gauss setup" in output + + def test_cli_prefers_config_provider_over_stale_env_override(monkeypatch): cli = _import_cli() @@ -374,4 +397,4 @@ def test_model_flow_custom_saves_verified_v1_base_url(monkeypatch, capsys): assert "Saving the working base URL instead" in output assert saved_env["OPENAI_BASE_URL"] == "http://localhost:8000/v1" assert saved_env["OPENAI_API_KEY"] == "local-key" - assert saved_env["MODEL"] == "llm" \ No newline at end of file + assert saved_env["MODEL"] == "llm" diff --git a/tests/test_morph_template.py b/tests/test_morph_template.py new file mode 100644 index 0000000..0c8f34e --- /dev/null +++ b/tests/test_morph_template.py @@ -0,0 +1,39 @@ +from pathlib import Path + +import yaml + + +TEMPLATE_PATH = Path(__file__).resolve().parents[1] / ".github" / "morph" / "opengauss-template.yaml" + + +def _load_template() -> dict: + return yaml.safe_load(TEMPLATE_PATH.read_text(encoding="utf-8")) + + +def test_morph_template_restores_optional_provider_secret_staging(): + template = _load_template() + steps = template["steps"] + step_ids = [step["id"] for step in steps] + by_id = {step["id"]: step for step in steps} + + assert "stages optional provider keys" in template["description"] + + expected_secret_steps = { + "optional-openrouter": "OPENROUTER_API_KEY", + "optional-openai": "OPENAI_API_KEY", + "optional-anthropic": "ANTHROPIC_API_KEY", + } + for step_id, secret_name in expected_secret_steps.items(): + step = by_id[step_id] + assert step["type"] == "exportSecret" + assert step["name"] == secret_name + assert step["optional"] is True + assert f'{secret_name}=' in step["run"] + + finalize = by_id["finalize-provider-selection"] + assert finalize["type"] == "command" + assert "gauss-configure-main-provider" in finalize["run"] + assert step_ids.index("optional-openrouter") < step_ids.index("finalize-provider-selection") + assert step_ids.index("optional-openai") < step_ids.index("finalize-provider-selection") + assert step_ids.index("optional-anthropic") < step_ids.index("finalize-provider-selection") + assert step_ids.index("finalize-provider-selection") < step_ids.index("start-guide-server") diff --git a/tests/test_publish_shared_template.py b/tests/test_publish_shared_template.py index 8f23024..04b59b8 100644 --- a/tests/test_publish_shared_template.py +++ b/tests/test_publish_shared_template.py @@ -97,7 +97,9 @@ def create_template(request): assert "steps:" in body["yaml"] return FakeResponse({"id": "tpl_new", "status": "draft"}) - def cache_template(_request): + def cache_template(request): + body = json.loads(request.data.decode("utf-8")) + assert body == {"force": True} return FakeResponse({"template_id": "tpl_new", "run_id": "run_1"}) template_polls = iter( @@ -186,7 +188,9 @@ def create_template(request): assert body["baseSnapshotId"] == "snap_base" return FakeResponse({"id": "tpl_new", "status": "draft"}) - def cache_template(_request): + def cache_template(request): + body = json.loads(request.data.decode("utf-8")) + assert body == {"force": True} return FakeResponse({"run_id": "run_1"}) template_polls = iter( @@ -222,3 +226,19 @@ def alias_after(_request): assert result["template_id"] == "tpl_new" assert result["alias"] == "demo" + + +def test_parse_bool_defaults_and_accepts_common_values(): + module = load_module() + + assert module.parse_bool(None, default=True) is True + assert module.parse_bool("", default=False) is False + assert module.parse_bool("1", default=False) is True + assert module.parse_bool("true", default=False) is True + assert module.parse_bool("yes", default=False) is True + assert module.parse_bool("0", default=True) is False + assert module.parse_bool("false", default=True) is False + assert module.parse_bool("no", default=True) is False + + with pytest.raises(module.PublishError, match="Invalid boolean value"): + module.parse_bool("maybe", default=True) diff --git a/tests/test_run_agent.py b/tests/test_run_agent.py index 058a6c4..e1abb7b 100644 --- a/tests/test_run_agent.py +++ b/tests/test_run_agent.py @@ -549,8 +549,8 @@ def test_always_has_identity(self, agent): def test_includes_open_gauss_entry_workflow_guidance(self, agent): prompt = agent._build_system_prompt() - assert "point them to /start if they want inline orientation or plain-language help" in prompt - assert "point them to /chat if they want a managed Claude Code or Codex chat session" in prompt + assert "point them to /chat if they want inline orientation or plain-language help" in prompt + assert "point them to /managed-chat if they want a managed Claude Code or Codex child session" in prompt assert "point them to /project" in prompt assert "/autoprove The de Bruijn - Erdos theorem" in prompt assert "Ctrl-] detaches and returns them to the main Gauss session" in prompt diff --git a/website/docs/getting-started/start-here.md b/website/docs/getting-started/start-here.md index 5de0d4d..a52d4e3 100644 --- a/website/docs/getting-started/start-here.md +++ b/website/docs/getting-started/start-here.md @@ -8,23 +8,23 @@ description: "A plain-language OpenGauss quick start for mathematicians using ei OpenGauss is for Lean work, but you do **not** need to understand MCP, plugin internals, or agent orchestration to get started. -If you only want a guided first step, use `/start`. +If you only want a guided first step or plain-language help in the current session, use `/chat`. -If you want a managed Claude Code or Codex chat session first, use `/chat`. +If you want a managed Claude Code or Codex child session first, use `/managed-chat`. If you want OpenGauss to work inside a Lean project, use `/project`. ## 30-Second Version -- **Morph**: open `morph.new/opengauss`, claim or save the session early if Morph offers that option, run `gauss-open-guide` if the guide is not already open, then start with `/start`, `/chat`, or `/project init`. -- **Local install**: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/start`, `/chat`, or `/project init`. +- **Morph**: open `morph.new/opengauss`, claim or save the session early if Morph offers that option, run `gauss-open-guide` if the guide is not already open, then start with `/chat`, `/managed-chat`, or `/project init`. +- **Local install**: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/chat`, `/managed-chat`, or `/project init`. - **Already have a Lean repo**: `cd` into it, run `gauss`, then `/project init`. - **Need a new Lean repo**: run `gauss`, then `/project create --template-source `. ## Which Command Should I Start With? -- `/start` turns on onboarding mode, gives you the first useful commands, and lets plain text go straight to the main chat. -- `/chat` opens the configured managed backend chat session before you choose a project. +- `/chat` turns on onboarding mode, gives you the first useful commands, and lets plain text go straight to the main chat in the current Gauss session. +- `/managed-chat` opens the configured managed backend child session before you choose a project. - `/project init` tells OpenGauss that the current Lean repository is your working project. - `/project use ` points OpenGauss at an already-initialized project somewhere else on disk. - `/project create --template-source ` creates a new Lean project and registers it. @@ -38,7 +38,7 @@ If you want OpenGauss to work inside a Lean project, use `/project`. 2. If Morph shows a **Claim**, **Save**, or similar action for the session, use it early. The exact button text can change, but temporary sessions are easier to lose than claimed ones. 3. Run `gauss-open-guide` if the browser guide is not already visible. -4. If you want orientation first, type `/start`, or use `/chat` for the configured managed backend chat session. +4. If you want orientation first, type `/chat`, or use `/managed-chat` for the configured managed backend child session. 5. If you want to work on a Lean project, clone or open it and then run `/project init` or `/project use`. ### Making It Persistent @@ -79,17 +79,17 @@ gauss Then: -- use `/start` if you want a short first-step guide and plain-language chat mode -- use `/chat` if you want the configured managed backend chat session first +- use `/chat` if you want a short first-step guide and plain-language chat mode +- use `/managed-chat` if you want the configured managed backend child session first - use `/project init` if you are already inside a Lean repository - use `/project create --template-source ` if you need a new project ## First Useful Examples ```text -/start +/chat /chat I have a Lean theorem but I am not sure how to start proving it. -/chat What does `/project init` do? +/managed-chat What does `/project init` do? /prove Show me how to prove that 1 + 1 = 2 in Lean. /review Main.lean /draft "State the intermediate value theorem" @@ -105,7 +105,7 @@ Then: Start with this sequence: -1. `/start` +1. `/chat` 2. Ask one plain question in English. 3. Let OpenGauss explain the next command. 4. Only after that, run `/project ...`