From 396c10c2ae27a3d1aaa76c4509337cd2587fb976 Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Mon, 30 Mar 2026 18:17:09 +0000 Subject: [PATCH 1/6] Add friendlier onboarding and /chat mode --- README.md | 13 ++ agent/prompt_builder.py | 14 +- cli.py | 92 ++++++++++-- gauss_cli/banner.py | 9 +- gauss_cli/commands.py | 3 +- gauss_cli/default_soul.py | 2 +- gauss_cli/skin_engine.py | 6 +- scripts/install-internal.sh | 142 +++++++++++++++--- tests/gauss_cli/test_banner_responsive.py | 2 + tests/gauss_cli/test_commands.py | 2 + .../run-in-container.sh | 6 + tests/test_cli_handoff_command.py | 28 ++++ tests/test_run_agent.py | 3 +- website/docs/getting-started/installation.md | 4 + website/docs/getting-started/quickstart.md | 9 ++ website/docs/getting-started/start-here.md | 108 +++++++++++++ website/docs/index.md | 3 + website/docs/reference/slash-commands.md | 1 + website/docs/user-guide/cli.md | 5 + website/sidebars.ts | 1 + 20 files changed, 404 insertions(+), 49 deletions(-) create mode 100644 website/docs/getting-started/start-here.md diff --git a/README.md b/README.md index a19c474..f6dd0db 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,13 @@ Open Gauss is a project-scoped Lean workflow orchestrator from Math, Inc. It gives `gauss` a multi-agent frontend for the `lean4-skills` `prove`, `draft`, `review`, `checkpoint`, `refactor`, `golf`, `autoprove`, `formalize`, and `autoformalize` workflows, while staging the Lean tooling, MCP/LSP wiring, and backend session state those workflows need. +> New to OpenGauss, Lean tooling, or AI-agent workflows? +> 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 `/chat`. +> - Local: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/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. Each lifted slash command spawns a managed backend child agent in the active project and forwards the same argument tail into the corresponding `lean4-skills` workflow command: @@ -26,6 +33,8 @@ Each lifted slash command spawns a managed backend child agent in the active pro 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 are not already comfortable with OpenGauss, read the [Start Here guide](website/docs/getting-started/start-here.md) before picking a workflow. + ### macOS and Linux ```bash @@ -108,8 +117,11 @@ gauss update ## Quick start +If you want the plain-language version first, read the [Start Here guide](website/docs/getting-started/start-here.md). + ``` gauss # Launch the CLI +/chat # Ask a plain-language question first /project create ~/my-project --template-source /prove 1+1=2 # Spawn a proving agent /swarm # See running agents @@ -120,6 +132,7 @@ If you already have a Lean project: ``` cd ~/my-lean-project gauss +/chat # Optional: ask questions before choosing a workflow /project init # Register it as a Gauss project /prove # Start proving ``` diff --git a/agent/prompt_builder.py b/agent/prompt_builder.py index c1ff35a..69f6a3b 100644 --- a/agent/prompt_builder.py +++ b/agent/prompt_builder.py @@ -67,12 +67,14 @@ 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, explain that they should first create or activate a Gauss project " - "with /project, then run /prove, /autoprove, /formalize, or " - "/autoformalize followed by a natural-language instruction, for 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. " + "start, give them the lowest-friction path first: point them to /chat if " + "they want orientation or plain-language help, 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 " + "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. " "Be clear, admit uncertainty when appropriate, and prioritize being " "genuinely useful over being verbose unless otherwise directed below. " "Be targeted and efficient in your exploration and investigations." diff --git a/cli.py b/cli.py index b5d4cad..158bc27 100755 --- a/cli.py +++ b/cli.py @@ -1280,6 +1280,7 @@ def __init__( self._background_tasks: Dict[str, threading.Thread] = {} self._background_task_counter = 0 self._project_override_root: Optional[Path] = None + self._chat_mode_enabled = False def _invalidate(self, min_interval: float = 0.25) -> None: """Throttled UI repaint — prevents terminal blinking on slow/SSH connections.""" @@ -2355,8 +2356,8 @@ def show_help(self): _cprint(f"\n {_DIM}Active project: {project_summary}{_RST}") else: _cprint( - f"\n {_DIM}No active project — use /project init, /project convert, " - f"/project create , or /project use .{_RST}" + f"\n {_DIM}No active project — use /chat for plain-language help, or /project init, " + f"/project convert, /project create , or /project use .{_RST}" ) for category, commands in COMMANDS_BY_CATEGORY.items(): @@ -2372,8 +2373,8 @@ def show_help(self): ) _cprint( - f"\n {_DIM}Tip: Use /project first, then launch /prove, /review, /checkpoint, " - f"/refactor, /golf, /draft, /autoprove, /formalize, or /autoformalize.{_RST}" + f"\n {_DIM}Tip: Start with /chat if you want orientation first. 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}") _cprint(f" {_DIM}Paste image: Alt+V (or /paste){_RST}\n") @@ -3307,6 +3308,7 @@ def _project_lock_allows_command(self, command: str) -> bool: """Return whether *command* remains available before project selection.""" cmd_lower = command.lower().strip() allowed_prefixes = ( + "/chat", "/project", "/help", "/quit", @@ -3340,11 +3342,28 @@ def _print_project_lock_notice(self, *, command_label: str) -> None: "or `/project use ` first.[/]", 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 `/chat` and ask a plain-language question.[/]", + "If you only want orientation first, run /chat and ask a plain-language question.", + ) self._print_surface_notice( f"[dim]{detail}[/]", detail, ) + def _chat_mode_active(self) -> bool: + """Return whether plain-text chat is allowed before project selection.""" + return bool(getattr(self, "_chat_mode_enabled", False)) + + def _plain_input_requires_project(self) -> bool: + """Return True when a non-command message should be blocked by project lock.""" + if not self._project_lock_enabled(): + return False + if self._chat_mode_active(): + return False + project, _source, _error = self._project_state() + return project is None + def _enforce_project_lock(self, command: str) -> bool: """Return True when the command should be blocked by the interactive project lock.""" if not self._project_lock_enabled(): @@ -3358,6 +3377,57 @@ def _enforce_project_lock(self, command: str) -> bool: self._print_project_lock_notice(command_label=command_label) return True + def _handle_chat_command(self, cmd: str): + """Handle `/chat` onboarding mode before project selection.""" + parts = cmd.strip().split(maxsplit=1) + payload = parts[1].strip() if len(parts) > 1 else "" + lowered = payload.lower() + + if not payload or lowered in {"on", "enable", "start"}: + 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. " + "Use `/chat off` to go back to project-first mode.[/]", + "`/chat` is on. Plain text now goes to the main interactive provider even without an active Gauss project. Use /chat off to go back to project-first mode.", + ) + return + + if lowered in {"off", "disable", "stop"}: + self._chat_mode_enabled = False + self._print_surface_notice( + "[bold yellow]`/chat` is off.[/] " + "[dim]Plain text without an active project will again prompt you to use `/project` first.[/]", + "`/chat` is off. Plain text without an active project will again prompt you to use /project first.", + ) + return + + if lowered == "status": + if self._chat_mode_active(): + self._print_surface_notice( + "[bold green]`/chat` is currently on.[/]", + "`/chat` is currently on.", + ) + else: + self._print_surface_notice( + "[bold yellow]`/chat` is currently off.[/]", + "`/chat` is currently off.", + ) + return + + self._chat_mode_enabled = True + self._print_surface_notice( + "[dim]`/chat` is on — sending your message to the main interactive provider.[/]", + "`/chat` is on - 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 _setup_swarm_completion_callback(self): """Wire up a one-time callback so finished swarm tasks notify the TUI.""" swarm = SwarmManager() @@ -3866,6 +3936,8 @@ def process_command(self, command: str) -> bool: if cmd_lower in ("/quit", "/exit", "/q"): return False + elif cmd_lower == "/chat" or cmd_lower.startswith("/chat "): + self._handle_chat_command(cmd_original) elif cmd_lower == "/help": self.show_help() elif cmd_lower == "/project" or cmd_lower.startswith("/project "): @@ -6172,10 +6244,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 your message or /help for commands.") + _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /chat for orientation or /help for commands.") _welcome_color = _welcome_skin.get_color("banner_text", "#FFF8DC") except Exception: - _welcome_text = "Welcome to Gauss! Type your message or /help for commands." + _welcome_text = "Welcome to Gauss! Type /chat for orientation or /help for commands." _welcome_color = "#FFF8DC" self.console.print(f"[{_welcome_color}]{_welcome_text}[/]") self.console.print() @@ -7179,11 +7251,9 @@ def process_loop(): app.exit() continue - if self._project_lock_enabled(): - project, _source, _error = self._project_state() - if project is None: - self._print_project_lock_notice(command_label="/chat") - continue + if self._plain_input_requires_project(): + self._print_project_lock_notice(command_label="/chat") + continue # Expand paste references back to full content import re as _re diff --git a/gauss_cli/banner.py b/gauss_cli/banner.py index 1c4ee86..f6b29af 100644 --- a/gauss_cli/banner.py +++ b/gauss_cli/banner.py @@ -434,7 +434,8 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines = [] if simplified: - right_lines.append(f"[bold {accent}]Workflow[/]") + right_lines.append(f"[bold {accent}]Start Here[/]") + right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]ask a plain-language question first[/]") 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[/]") @@ -445,7 +446,8 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines.append(f"[{text}]`/swarm`[/] [dim {dim}]track, attach, or cancel workflow agents[/]") right_lines.append(f"[{text}]`/help`[/] [dim {dim}]commands and diagnostics[/]") else: - right_lines.append(f"[bold {accent}]Primary Workflow[/]") + right_lines.append(f"[bold {accent}]Start Here[/]") + right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} ask a plain-language question before choosing a project[/]") 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[/]") @@ -455,7 +457,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines.append(f"[{text}]`/autoformalize`[/] [dim {dim}]{long_dash} spawn an autonomous managed formalization agent[/]") right_lines.append(f"[{text}]`/swarm`[/] [dim {dim}]{long_dash} track, attach, or cancel workflow agents[/]") right_lines.append(f"[{text}]`/help`[/] [dim {dim}]{long_dash} session and diagnostics commands[/]") - right_lines.append(f"[dim {dim}]Bundled skills and user-managed MCP are off by default.[/]") + right_lines.append(f"[dim {dim}]You can ignore MCP and plugin internals at first; Open Gauss stages the default Lean workflow setup for you.[/]") try: from swarm_manager import SwarmManager @@ -467,6 +469,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str, right_lines.append("") summary_parts = [ + "/chat", "/project", "/prove", "/review", diff --git a/gauss_cli/commands.py b/gauss_cli/commands.py index 696bb70..88db72b 100644 --- a/gauss_cli/commands.py +++ b/gauss_cli/commands.py @@ -17,7 +17,8 @@ # Commands organized by category for better help display COMMANDS_BY_CATEGORY = { - "Project": { + "Start Here": { + "/chat": "Ask a plain-language question before choosing a Gauss project", "/project": "Create, convert, inspect, or switch the active Gauss project", }, "Workflow": { diff --git a/gauss_cli/default_soul.py b/gauss_cli/default_soul.py index 5c42960..e93a2c5 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, point them to `/project` first 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 want to ask a question in plain language, 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. 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 f9e71c0..6065e99 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 your message or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for orientation 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 your message or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for orientation 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 your message or /help for commands.", + "welcome": "Welcome to Gauss! Type /chat for orientation or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index 3394750..ca9cd1c 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -863,10 +863,11 @@ ensure_workspace() { This Lean workspace is prewarmed and already registered as the active Gauss project. Quickstart: -1. Run `gauss-open-session` for the batteries-included launcher. -2. Or launch `gauss` directly inside this workspace. -3. Use `/prove`, `/draft`, `/autoprove`, `/formalize`, `/autoformalize`, or `/swarm`. -4. Keep paper notes, extracted statements, and scratch proofs in this project. +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 orientation 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. TXT log_success "Created $WORKSPACE_DIR/PAPER.md" else @@ -969,6 +970,7 @@ helper_dir.mkdir(parents=True, exist_ok=True) guide_dir.mkdir(parents=True, exist_ok=True) readme = (repo_root / "README.md").read_text(encoding="utf-8") +start_here_doc = repo_root / "website/docs/getting-started/start-here.md" repo_head = subprocess.check_output( ["git", "-C", str(repo_root), "rev-parse", "--short=12", "HEAD"], text=True, @@ -1017,7 +1019,7 @@ guide_html = f""" border-radius: 18px; background: var(--panel); }} - .hero p, .grid p {{ margin: 0; line-height: 1.6; }} + .hero p, .grid p, .grid li, main li {{ margin: 0; line-height: 1.6; }} .grid {{ display: grid; gap: 12px; @@ -1039,6 +1041,13 @@ guide_html = f""" padding: 2px 6px; border-radius: 6px; }} + .callout {{ + margin: 0 20px 14px; + padding: 14px 18px; + border-left: 4px solid var(--accent); + border-radius: 14px; + background: rgba(72, 93, 66, 0.08); + }} main {{ margin: 0 20px 20px; padding: 18px; @@ -1047,12 +1056,41 @@ guide_html = f""" background: var(--surface); overflow: auto; }} - pre {{ - margin: 0; + h2, h3 {{ + margin: 0 0 10px; + color: var(--accent); + }} + h2 {{ margin-top: 20px; }} + h2:first-child {{ margin-top: 0; }} + ul, ol {{ + margin: 10px 0 0 22px; + padding: 0; + }} + li + li {{ margin-top: 8px; }} + .code-block, pre {{ + margin: 12px 0 0; white-space: pre-wrap; word-break: break-word; font: 13px/1.45 "IBM Plex Mono", "SFMono-Regular", monospace; color: var(--ink); + background: var(--code-bg); + border-radius: 12px; + padding: 12px 14px; + }} + details {{ + margin-top: 20px; + padding: 12px 14px; + border: 1px solid var(--border); + border-radius: 14px; + background: rgba(240, 229, 217, 0.55); + }} + summary {{ + cursor: pointer; + font-weight: 700; + color: var(--accent); + }} + pre {{ + margin-top: 12px; }} @@ -1062,27 +1100,70 @@ guide_html = f""" Open repo
-

This local installer uses the checked-out math-inc/OpenGauss repository at {escape(str(repo_root))} and currently resolves to {repo_head}. It preloads Lean 4, Claude Code, OpenAI Codex, the Math Inc skin, and a ready project at {escape(str(workspace_dir))}. Run gauss-open-session for the batteries-included launcher or gauss directly if you prefer to skip the session wrapper.

+

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 /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 /chat.
  • +
  • Local install: run gauss-open-guide or gauss, then start with /chat or /project init.
  • +
  • Lean work starts after project selection: use /prove, /review, /draft, or /autoprove once a project is active.
  • +
- Ready Paths -

{escape(str(repo_root))}
{escape(str(workspace_dir))}
{escape(str(gauss_home / ".env"))}

+ Use These First +

gauss-open-guide
gauss
/chat
/project init

- Backend Helpers -

gauss-use-claude-backend
gauss-use-codex-backend
gauss-use-auto-auth
gauss-use-claude-login
gauss-use-codex-login

+ If You Opened This In Morph +

Claim or save the session early if Morph offers that action. The exact button name can change, but a claimed or saved session is less disposable than a temporary one.

- Main Provider Helpers -

gauss-use-openrouter-key
gauss-use-anthropic-key
gauss-use-openai-key
gauss-configure-main-provider
gauss-open-session

+ Bring Your Existing Project +

The safest path is still git: push the project somewhere, then clone it here. For small files, Morph upload or drag-and-drop is fine if your current view supports it.

- Optional Staged Keys -

OPENROUTER_API_KEY
OPENAI_API_KEY
ANTHROPIC_API_KEY

+ Keep Your Work +

Commit important changes, push to a remote, and use any save or snapshot feature Morph exposes before closing the tab. Avoid leaving important work only in temp directories.

+
+
+ Ready Paths +

{escape(str(repo_root))}
{escape(str(workspace_dir))}
{escape(str(gauss_home / ".env"))}
{escape(str(start_here_doc))}

+
+
+ Backend Helpers +

gauss-use-claude-backend
gauss-use-codex-backend
gauss-use-auto-auth
gauss-use-claude-login
gauss-use-codex-login

-
{escape(readme)}
+
+

Start Here

+
    +
  1. Run gauss.
  2. +
  3. If you want a normal conversation first, type /chat.
  4. +
  5. If you already have a Lean repo, type /project init inside it.
  6. +
  7. If you need a new Lean repo, type /project create <path> --template-source <template-or-git-url>.
  8. +
  9. After that, use /prove, /review, /draft, or /autoprove.
  10. +
+ +

Useful First Questions

+
/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.
+ +

What This Install Prepared

+
    +
  • Repository checkout: {escape(str(repo_root))} at commit {repo_head}
  • +
  • Lean workspace: {escape(str(workspace_dir))}
  • +
  • Gauss home: {escape(str(gauss_home))}
  • +
  • Guide source doc: {escape(str(start_here_doc))}
  • +
+ +
+ Advanced repo README +
{escape(readme)}
+
+
""" @@ -1379,8 +1460,17 @@ Default auth mode: auto Main interactive provider: ${interactive_provider} Staged keys: ${staged_keys} -Quickstart: +Start here: + gauss-open-guide + gauss + /chat + /project init + /project use + /project create --template-source + +Lean workflows: /prove + /review Main.lean /draft "Theorem 3.2" /autoprove /formalize --source ./paper.pdf "Theorem 3.2" @@ -1400,6 +1490,7 @@ Backend helpers: Interactive provider notes: Auto-selection priority: OpenRouter, then Anthropic, then OpenAI-compatible. OpenRouter affects the main chat UI only; managed workflow backends stay separate. + /chat uses the main interactive provider, not the managed Lean backend. PROMPT_TOOLKIT_NO_CPR=1 is enabled to avoid CPR warnings inside tmux. The local guide is written to __GUIDE_PATH__. @@ -1585,20 +1676,24 @@ print_summary() { echo " Guide: $GUIDE_DIR/index.html" echo printf '%b%s%b\n' "${CYAN}${BOLD}" "Next Steps:" "${NC}" - echo " 1. Start immediately: $GAUSS_BIN" - echo " 2. Verify the CLI: $GAUSS_BIN --version" - echo " 3. Reload for \`gauss\`: $SHELL_RELOAD_HINT # current shell ($ACTIVE_SHELL_NAME)" + echo " 1. Open the guide: gauss-open-guide" + echo " 2. Start immediately: $GAUSS_BIN" + echo " 3. Verify the CLI: $GAUSS_BIN --version" + echo " 4. Reload for \`gauss\`: $SHELL_RELOAD_HINT # current shell ($ACTIVE_SHELL_NAME)" if [ -n "$SECONDARY_SHELL_RELOAD_HINT" ]; then echo " $SECONDARY_SHELL_RELOAD_HINT # if you switch to $SECONDARY_SHELL_NAME" fi - echo " 4. Review settings: gauss setup" + echo " 5. Review settings: gauss setup" echo printf '%b%s%b\n' "${CYAN}${BOLD}" "Start Options:" "${NC}" + echo " /chat # ask a plain-language question before choosing a project" + 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" echo " gauss-open-session # batteries-included launcher (tmux when interactive)" echo " gauss-open-guide # open the local guide in a browser, or print its path" echo - echo " Inside Gauss, use /project create to create a Lean project." + echo " Inside Gauss, use /prove, /review, /draft, /autoprove, /formalize, or /autoformalize once a project is active." echo printf '%b%s%b\n' "${CYAN}${BOLD}" "Helper Commands:" "${NC}" echo " gauss-configure-main-provider [auto|openrouter|anthropic|openai]" @@ -1620,6 +1715,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 /chat and ask a normal question." 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/tests/gauss_cli/test_banner_responsive.py b/tests/gauss_cli/test_banner_responsive.py index 850156d..903d5ee 100644 --- a/tests/gauss_cli/test_banner_responsive.py +++ b/tests/gauss_cli/test_banner_responsive.py @@ -205,6 +205,8 @@ def test_build_welcome_banner_mentions_swarm_in_primary_workflow(monkeypatch): ) exported = console.export_text() + assert "/chat" in exported + assert "ask a plain-language question before choosing a project" 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 d08e494..c8a8c02 100644 --- a/tests/gauss_cli/test_commands.py +++ b/tests/gauss_cli/test_commands.py @@ -8,6 +8,7 @@ # All commands that must be present in the shared COMMANDS dict. EXPECTED_COMMANDS = { + "/chat", "/project", "/prove", "/draft", @@ -56,6 +57,7 @@ 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["/chat"] == "Ask a plain-language question before choosing a Gauss project" 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" 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 7fb8044..4ebe203 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 @@ -81,6 +81,9 @@ assert_exists "$GAUSS_HOME/.env" 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 "/chat" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to mention /chat" +grep -F "If You Opened This In Morph" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to include Morph guidance" assert_exists "$GAUSS_HOME/autoformalize/assets/lean4-skills/.gauss-managed-revision" assert_exists "$GAUSS_HOME/skins/mathinc.yaml" assert_exists "$WORKSPACE_DIR/PAPER.md" @@ -168,6 +171,8 @@ SUMMARY_OUTPUT="$(gauss-launch-session --print-summary)" printf '%s\n' "$SUMMARY_OUTPUT" [[ "$SUMMARY_OUTPUT" == *"OpenAI-compatible main provider configured"* ]] || die "expected OpenAI provider summary" [[ "$SUMMARY_OUTPUT" == *"$WORKSPACE_DIR"* ]] || die "expected workspace path in launcher summary" +[[ "$SUMMARY_OUTPUT" == *"/chat"* ]] || die "expected launcher summary to mention /chat" +[[ "$SUMMARY_OUTPUT" == *"gauss-open-guide"* ]] || die "expected launcher summary to mention gauss-open-guide" echo "==> Verifying no-provider launcher fallback state" cp "$GAUSS_HOME/.env" "$GAUSS_HOME/.env.backup" @@ -194,6 +199,7 @@ PY NO_PROVIDER_SUMMARY="$(gauss-launch-session --print-summary)" printf '%s\n' "$NO_PROVIDER_SUMMARY" [[ "$NO_PROVIDER_SUMMARY" == *"No staged OpenRouter, Anthropic, or OpenAI key found for the main interactive provider."* ]] || die "expected missing-provider summary" +[[ "$NO_PROVIDER_SUMMARY" == *"/chat uses the main interactive provider"* ]] || die "expected provider notes to mention /chat" if grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null; then die "expected launcher to stop forcing gauss setup" fi diff --git a/tests/test_cli_handoff_command.py b/tests/test_cli_handoff_command.py index c063464..1a31107 100644 --- a/tests/test_cli_handoff_command.py +++ b/tests/test_cli_handoff_command.py @@ -347,6 +347,34 @@ 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 "/chat" in rendered + + +def test_chat_command_enables_chat_mode_before_project_selection(): + 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._plain_input_requires_project() is True + assert cli_obj.process_command("/chat") is True + + assert cli_obj._chat_mode_enabled is True + assert cli_obj._plain_input_requires_project() is False + rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) + assert "`/chat` is on." in rendered + + +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("/chat Explain what /project init does") is True + + assert cli_obj._chat_mode_enabled is True + cli_obj._pending_input.put.assert_called_once_with("Explain what /project init does") def test_handoff_alias_rewrites_to_autoformalize(): diff --git a/tests/test_run_agent.py b/tests/test_run_agent.py index 71585c0..051296a 100644 --- a/tests/test_run_agent.py +++ b/tests/test_run_agent.py @@ -549,7 +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 "create or activate a Gauss project with /project" in prompt + assert "point them to /chat" 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/installation.md b/website/docs/getting-started/installation.md index e572ae0..e068fbf 100644 --- a/website/docs/getting-started/installation.md +++ b/website/docs/getting-started/installation.md @@ -6,6 +6,8 @@ description: "Install Gauss from a Linux repository checkout." # Installation +> If you want the mathematician-friendly version first, start with [Start Here](/docs/getting-started/start-here). + ## Recommended ```bash @@ -24,12 +26,14 @@ This repository-local installer targets Linux checkouts, with Ubuntu, Debian, an ## After Install ```bash +gauss-open-guide gauss ``` Inside the CLI, start by selecting a project: ```text +/chat /project init ``` diff --git a/website/docs/getting-started/quickstart.md b/website/docs/getting-started/quickstart.md index 5cd6a2b..21bae50 100644 --- a/website/docs/getting-started/quickstart.md +++ b/website/docs/getting-started/quickstart.md @@ -6,6 +6,9 @@ description: "Install Gauss, select a project, and launch the managed Lean prove # Quickstart +> New to OpenGauss or not comfortable with AI tooling yet? +> Read [Start Here](/docs/getting-started/start-here) first. + ## 1. Install ```bash @@ -21,6 +24,12 @@ The installer targets Linux checkouts, defaults runtime state to `~/.gauss/`, ex gauss ``` +If you want plain-language help before choosing a project: + +```text +/chat +``` + ## 3. Select the active project ```text diff --git a/website/docs/getting-started/start-here.md b/website/docs/getting-started/start-here.md new file mode 100644 index 0000000..3a84da9 --- /dev/null +++ b/website/docs/getting-started/start-here.md @@ -0,0 +1,108 @@ +--- +sidebar_position: 1 +title: "Start Here" +description: "A plain-language OpenGauss quick start for mathematicians using either Morph or a local install." +--- + +# Start Here + +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 to ask questions first, use `/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 `/chat` or `/project init`. +- **Local install**: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/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? + +- `/chat` asks a plain-language question in the main OpenGauss chat 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. +- `/prove`, `/review`, `/draft`, `/autoprove`, `/formalize`, and `/autoformalize` are the Lean workflow commands you use **after** you have selected a project. + +## Morph Path + +### First 10 Minutes + +1. Open the OpenGauss Morph template. +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 `/chat`. +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 + +- The safest persistence is still **git**: commit locally and push to a remote. +- If Morph offers **save**, **snapshot**, or **persistent devbox** controls, use them before closing the tab. +- Keep important work in your home directory or in checked-out repositories, not in throwaway temp directories. + +### Bringing In An Existing Project + +- Best path: push the project to Git and `git clone` it inside Morph. +- Fine for small files: use Morph upload or drag-and-drop if your current view supports it, then move the files into a repository directory. +- For larger projects, an archive plus unpacking in the terminal is usually better than lots of one-off file uploads. + +After the project is on the box: + +```text +/project init +/prove +``` + +or + +```text +/project use /path/to/project +/review Main.lean +``` + +## Local Install Path + +From a checkout of `math-inc/OpenGauss`: + +```bash +./scripts/install.sh +gauss-open-guide +gauss +``` + +Then: + +- use `/chat` if you want a plain-language conversation 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 +/chat I have a Lean theorem but I am not sure how to start proving it. +/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" +``` + +## What OpenGauss Is Actually Doing + +- OpenGauss manages the terminal session and project context for you. +- The Lean proving and formalization workflows come from the staged `lean4-skills` environment. +- You do not need to manually install or wire MCP in order to use the default proving flows. + +## If The Interface Feels Like Too Much + +Start with this sequence: + +1. `/chat` +2. Ask one plain question in English. +3. Let OpenGauss explain the next command. +4. Only after that, run `/project ...` + +That path is intentionally slower, but it is the least intimidating way in. diff --git a/website/docs/index.md b/website/docs/index.md index 9bbb86c..e4660cb 100644 --- a/website/docs/index.md +++ b/website/docs/index.md @@ -13,6 +13,8 @@ Gauss is a narrow product on purpose. It is not trying to be a general agent pla 3. enter the managed Lean session for that workflow 4. return to the same Gauss session when that child exits +If you are opening OpenGauss for the first time and just want a plain-language explanation of what to do next, start with [Start Here](/docs/getting-started/start-here). + ## Core Ideas - **Lean workflow menu**: guided proving, drafting, autonomous proving, interactive formalization, and autonomous formalization @@ -22,6 +24,7 @@ Gauss is a narrow product on purpose. It is not trying to be a general agent pla ## Start Here +- [Start Here](/docs/getting-started/start-here) - [Quickstart](/docs/getting-started/quickstart) - [Installation](/docs/getting-started/installation) - [Migration to Gauss](/docs/getting-started/migration-to-gauss) diff --git a/website/docs/reference/slash-commands.md b/website/docs/reference/slash-commands.md index 8f4d8fd..7bfdf40 100644 --- a/website/docs/reference/slash-commands.md +++ b/website/docs/reference/slash-commands.md @@ -12,6 +12,7 @@ Gauss intentionally ships a small default surface. | Command | Description | |---|---| +| `/chat [question]` | Temporarily drop into plain-language chat before selecting a project. | | `/prove [scope or flags]` | Launch the guided managed Lean prove workflow. | | `/draft [topic or flags]` | Launch the managed Lean draft workflow for declaration skeletons. | | `/review [scope or flags]` | Launch the read-only managed Lean review workflow. | diff --git a/website/docs/user-guide/cli.md b/website/docs/user-guide/cli.md index 8de84b9..679c7ee 100644 --- a/website/docs/user-guide/cli.md +++ b/website/docs/user-guide/cli.md @@ -8,6 +8,8 @@ description: "Use the Gauss terminal interface and launch the managed Lean workf Gauss is a terminal-first product. The public surface is intentionally small. +If you are still orienting yourself, read [Start Here](/docs/getting-started/start-here) first and use `/chat` before choosing a project. + ## Start the CLI ```bash @@ -16,6 +18,8 @@ gauss --resume gauss chat -q "hello" ``` +Inside the interactive CLI, `/chat` is the simplest on-ramp when you want to ask a question before selecting a Lean project. + ## Primary Workflow Run this inside the interactive CLI: @@ -36,6 +40,7 @@ Gauss stages the managed Lean runtime, yields the terminal to the configured bac ## Default Slash Commands +- `/chat` - `/prove` - `/draft` - `/review` diff --git a/website/sidebars.ts b/website/sidebars.ts index 11087b0..a89afdb 100644 --- a/website/sidebars.ts +++ b/website/sidebars.ts @@ -7,6 +7,7 @@ const sidebars: SidebarsConfig = { label: 'Getting Started', collapsed: false, items: [ + 'getting-started/start-here', 'getting-started/quickstart', 'getting-started/installation', 'getting-started/updating', From a146764787f6e12ead895fdb5f1cc916e9c3a927 Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Mon, 30 Mar 2026 20:56:15 +0000 Subject: [PATCH 2/6] Improve onboarding entry points and preserve explicit GAUSS_HOME --- README.md | 6 +- agent/prompt_builder.py | 2 +- cli.py | 67 ++++++++++++--- gauss_cli/banner.py | 3 + gauss_cli/commands.py | 82 +++++++++++++++++++ gauss_cli/default_soul.py | 2 +- gauss_cli/skin_engine.py | 6 +- scripts/install-internal.sh | 25 +++--- tests/gauss_cli/test_banner_responsive.py | 2 + tests/gauss_cli/test_commands.py | 21 ++++- .../run-in-container.sh | 3 + tests/test_cli_handoff_command.py | 37 +++++++++ tests/test_run_agent.py | 2 +- website/docs/getting-started/installation.md | 3 +- website/docs/getting-started/quickstart.md | 1 + website/docs/getting-started/start-here.md | 13 ++- website/docs/reference/slash-commands.md | 1 + website/docs/user-guide/cli.md | 5 +- 18 files changed, 245 insertions(+), 36 deletions(-) diff --git a/README.md b/README.md index f6dd0db..b3e8df7 100644 --- a/README.md +++ b/README.md @@ -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 `/chat`. -> - Local: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/chat` or `/project init`. +> - 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`. 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. @@ -121,6 +121,7 @@ If you want the plain-language version first, read the [Start Here guide](websit ``` gauss # Launch the CLI +/start # Show the first steps and turn on plain-language chat /chat # Ask a plain-language question first /project create ~/my-project --template-source /prove 1+1=2 # Spawn a proving agent @@ -132,6 +133,7 @@ If you already have a Lean project: ``` cd ~/my-lean-project gauss +/start # Optional: turn on onboarding mode first /chat # Optional: ask questions before choosing a workflow /project init # Register it as a Gauss project /prove # Start proving diff --git a/agent/prompt_builder.py b/agent/prompt_builder.py index 69f6a3b..090d92b 100644 --- a/agent/prompt_builder.py +++ b/agent/prompt_builder.py @@ -67,7 +67,7 @@ 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 /chat if " + "start, give them the lowest-friction path first: point them to /start or /chat if " "they want orientation or plain-language help, 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 " diff --git a/cli.py b/cli.py index 158bc27..a8c45e5 100755 --- a/cli.py +++ b/cli.py @@ -68,6 +68,12 @@ supported_autoformalize_backends, ) from gauss_cli.banner import _format_context_length +from gauss_cli.commands import ( + COMMANDS, + SlashCommandCompleter, + rewrite_friendly_entry_command, + rewrite_friendly_slash_command, +) from gauss_cli.handoff import HandoffError, HandoffUsageError, execute_handoff, resolve_handoff_request from gauss_cli.config import get_gauss_home from gauss_cli.project import ( @@ -504,7 +510,6 @@ def load_cli_config() -> Dict[str, Any]: build_welcome_banner, ) from gauss_cli.colors import render_terminal_text, spinner_frames, supports_ansi, supports_unicode -from gauss_cli.commands import COMMANDS, SlashCommandCompleter from gauss_cli import callbacks as _callbacks from toolsets import get_all_toolsets, get_toolset_info, resolve_toolset, validate_toolset @@ -2356,7 +2361,7 @@ def show_help(self): _cprint(f"\n {_DIM}Active project: {project_summary}{_RST}") else: _cprint( - f"\n {_DIM}No active project — use /chat for plain-language help, or /project init, " + f"\n {_DIM}No active project — use /start or /chat for orientation, or /project init, " f"/project convert, /project create , or /project use .{_RST}" ) @@ -2373,7 +2378,7 @@ def show_help(self): ) _cprint( - f"\n {_DIM}Tip: Start with /chat if you want orientation first. Use /project when you're ready to work in a Lean repo, " + f"\n {_DIM}Tip: Start with /start or /chat if you want orientation first. 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}") @@ -3308,6 +3313,7 @@ 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", "/project", "/help", @@ -3343,8 +3349,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 `/chat` and ask a plain-language question.[/]", - "If you only want orientation first, run /chat and ask a plain-language question.", + "[dim]If you only want orientation first, run `/start` or `/chat` and ask a plain-language question.[/]", + "If you only want orientation first, run /start or /chat and ask a plain-language question.", ) self._print_surface_notice( f"[dim]{detail}[/]", @@ -3428,6 +3434,39 @@ def _handle_chat_command(self, cmd: str): "Chat queue is not available in this mode.", ) + 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` for plain-language questions, `/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 for plain-language questions, /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.", + ) + def _setup_swarm_completion_callback(self): """Wire up a one-time callback so finished swarm tasks notify the TUI.""" swarm = SwarmManager() @@ -3928,14 +3967,20 @@ def process_command(self, command: str) -> bool: bool: True to continue, False to exit """ # Lowercase only for dispatch matching; preserve original case for arguments - cmd_lower = command.lower().strip() cmd_original = command.strip() + corrected = rewrite_friendly_slash_command(cmd_original) + if corrected and corrected != cmd_original: + _cprint(f" {_DIM}Assuming {corrected.split()[0]} from your input.{_RST}") + cmd_original = corrected + cmd_lower = cmd_original.lower().strip() if self._enforce_project_lock(cmd_original): return True 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 == "/help": @@ -4307,7 +4352,6 @@ def process_command(self, command: str) -> bool: # Prefix matching: if input uniquely identifies one command, execute it. # Matches against both built-in COMMANDS and installed skill commands so # that execution-time resolution agrees with tab-completion. - from gauss_cli.commands import COMMANDS typed_base = cmd_lower.split()[0] all_known = set(COMMANDS) | set(_skill_commands) matches = [c for c in all_known if c.startswith(typed_base)] @@ -6244,10 +6288,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 /chat for orientation or /help for commands.") + _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.") _welcome_color = _welcome_skin.get_color("banner_text", "#FFF8DC") except Exception: - _welcome_text = "Welcome to Gauss! Type /chat for orientation or /help for commands." + _welcome_text = "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands." _welcome_color = "#FFF8DC" self.console.print(f"[{_welcome_color}]{_welcome_text}[/]") self.console.print() @@ -7240,7 +7284,10 @@ def process_loop(): dispatched_command = ( user_input if user_input.startswith("/") - else rewrite_forgiving_managed_command(user_input) + else ( + rewrite_friendly_entry_command(user_input) + or rewrite_forgiving_managed_command(user_input) + ) ) if dispatched_command is not None: _cprint(f"\n⚙️ {dispatched_command}") diff --git a/gauss_cli/banner.py b/gauss_cli/banner.py index f6b29af..1bd7e02 100644 --- a/gauss_cli/banner.py +++ b/gauss_cli/banner.py @@ -435,6 +435,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}]ask a plain-language question first[/]") 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[/]") @@ -447,6 +448,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} ask a plain-language question before choosing a project[/]") 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[/]") @@ -469,6 +471,7 @@ 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 88db72b..593214b 100644 --- a/gauss_cli/commands.py +++ b/gauss_cli/commands.py @@ -7,7 +7,9 @@ from __future__ import annotations +import difflib import os +import re from collections.abc import Callable, Mapping from pathlib import Path from typing import Any @@ -18,6 +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": "Ask a plain-language question before choosing a Gauss project", "/project": "Create, convert, inspect, or switch the active Gauss project", }, @@ -70,6 +73,85 @@ COMMANDS.update(category_commands) +_FRIENDLY_ENTRY_ALIASES = { + "chat": "/chat", + "start": "/start", + "begin": "/start", + "project": "/project", + "help": "/help", +} + +_FRIENDLY_ENTRY_PHRASES = ( + "get started", + "getting started", + "how do i start", + "how do i get started", + "what do i do first", + "what should i do first", + "where do i start", +) + +_FRIENDLY_FUZZY_TARGETS = { + "chat": "/chat", + "start": "/start", + "project": "/project", + "help": "/help", +} + + +def _normalize_entry_token(token: str) -> str: + return re.sub(r"[^a-z]", "", token.lower()) + + +def rewrite_friendly_entry_command(command: str) -> str | None: + """Rewrite low-friction onboarding inputs into slash commands.""" + if not isinstance(command, str): + return None + text = command.strip() + if not text or text.startswith("/"): + return None + + lowered = " ".join(text.lower().split()) + if lowered in _FRIENDLY_ENTRY_PHRASES: + return "/start" + + parts = text.split(maxsplit=1) + token = _normalize_entry_token(parts[0]) + remainder = parts[1].strip() if len(parts) > 1 else "" + + direct = _FRIENDLY_ENTRY_ALIASES.get(token) + if direct: + return direct if not remainder else f"{direct} {remainder}" + + matches = difflib.get_close_matches(token, _FRIENDLY_FUZZY_TARGETS.keys(), n=1, cutoff=0.75) + if not matches: + return None + corrected = _FRIENDLY_FUZZY_TARGETS[matches[0]] + return corrected if not remainder else f"{corrected} {remainder}" + + +def rewrite_friendly_slash_command(command: str) -> str | None: + """Rewrite obvious misspelled onboarding slash commands.""" + if not isinstance(command, str): + return None + text = command.strip() + if not text.startswith("/"): + return None + + parts = text.split(maxsplit=1) + token = parts[0].strip().lower() + remainder = parts[1].strip() if len(parts) > 1 else "" + if token in COMMANDS: + return None + + normalized = _normalize_entry_token(token.lstrip("/")) + matches = difflib.get_close_matches(normalized, _FRIENDLY_FUZZY_TARGETS.keys(), n=1, cutoff=0.75) + if not matches: + return None + corrected = _FRIENDLY_FUZZY_TARGETS[matches[0]] + return corrected if not remainder else f"{corrected} {remainder}" + + class SlashCommandCompleter(Completer): """Autocomplete for built-in slash commands and optional skill commands.""" diff --git a/gauss_cli/default_soul.py b/gauss_cli/default_soul.py index e93a2c5..b5fd9bf 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 want to ask a question in plain language, 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 want to ask a question in plain language, point them to `/start` or `/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 6065e99..4632fde 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 /chat for orientation or /help for commands.", + "welcome": "Welcome to Gauss! Type /start or /chat for orientation, 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 /chat for orientation or /help for commands.", + "welcome": "Welcome to Gauss! Type /start or /chat for orientation, 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 /chat for orientation or /help for commands.", + "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index ca9cd1c..71a92eb 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -914,11 +914,11 @@ repo_root = sys.argv[2] shell_configs = [Path(arg).expanduser() for arg in sys.argv[3:]] block = f"""# >>> gauss workflow installer env >>> -export GAUSS_HOME="{gauss_home}" -export GAUSS_INSTALL_ROOT="{repo_root}" -if [ -f "{gauss_home}/.env" ]; then +export GAUSS_HOME="${{GAUSS_HOME:-{gauss_home}}}" +export GAUSS_INSTALL_ROOT="${{GAUSS_INSTALL_ROOT:-{repo_root}}}" +if [ -f "$GAUSS_HOME/.env" ]; then set -a - . "{gauss_home}/.env" + . "$GAUSS_HOME/.env" set +a fi export PATH="$HOME/.local/bin:{repo_root}/venv/bin:$HOME/.elan/bin:$PATH" @@ -1100,20 +1100,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 /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 first, start the CLI and type /start or /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 /chat.
  • -
  • Local install: run gauss-open-guide or gauss, then start with /chat or /project init.
  • +
  • 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.
  • Lean work starts after project selection: use /prove, /review, /draft, or /autoprove once a project is active.
Use These First -

gauss-open-guide
gauss
/chat
/project init

+

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

If You Opened This In Morph @@ -1140,6 +1140,7 @@ guide_html = f"""

Start Here

  1. Run gauss.
  2. +
  3. If you want a guided first step, type /start.
  4. If you want a normal conversation first, type /chat.
  5. If you already have a Lean repo, type /project init inside it.
  6. If you need a new Lean repo, type /project create <path> --template-source <template-or-git-url>.
  7. @@ -1147,7 +1148,8 @@ guide_html = f"""

Useful First Questions

-
/chat I am a mathematician new to Open Gauss. What should I do first? +
/start +/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.
@@ -1463,6 +1465,7 @@ Staged keys: ${staged_keys} Start here: gauss-open-guide gauss + /start /chat /project init /project use @@ -1490,6 +1493,7 @@ Backend helpers: Interactive provider notes: Auto-selection priority: OpenRouter, then Anthropic, then OpenAI-compatible. OpenRouter affects the main chat UI only; managed workflow backends stay separate. + /start and /chat use the main interactive provider, not the managed Lean backend. /chat uses the main interactive provider, not the managed Lean backend. PROMPT_TOOLKIT_NO_CPR=1 is enabled to avoid CPR warnings inside tmux. @@ -1686,6 +1690,7 @@ 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 # ask a plain-language question before choosing a project" echo " /project init # register the current Lean repo as the active project" echo " /project create ... # create a new Lean project from a template" @@ -1715,7 +1720,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 /chat and ask a normal question." + echo " - If Open Gauss feels intimidating, start with /start or /chat and ask a normal question." 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/tests/gauss_cli/test_banner_responsive.py b/tests/gauss_cli/test_banner_responsive.py index 903d5ee..95de1a4 100644 --- a/tests/gauss_cli/test_banner_responsive.py +++ b/tests/gauss_cli/test_banner_responsive.py @@ -205,6 +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 "ask a plain-language question before choosing a project" in exported assert "/swarm" in exported diff --git a/tests/gauss_cli/test_commands.py b/tests/gauss_cli/test_commands.py index c8a8c02..9f94841 100644 --- a/tests/gauss_cli/test_commands.py +++ b/tests/gauss_cli/test_commands.py @@ -3,11 +3,17 @@ from prompt_toolkit.completion import CompleteEvent from prompt_toolkit.document import Document -from gauss_cli.commands import COMMANDS, SlashCommandCompleter +from gauss_cli.commands import ( + COMMANDS, + SlashCommandCompleter, + rewrite_friendly_entry_command, + rewrite_friendly_slash_command, +) # All commands that must be present in the shared COMMANDS dict. EXPECTED_COMMANDS = { + "/start", "/chat", "/project", "/prove", @@ -57,6 +63,7 @@ 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"] == "Ask a plain-language question before choosing a Gauss project" 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" @@ -116,6 +123,18 @@ def test_no_completions_for_non_slash_input(self): def test_no_completions_for_empty_input(self): assert _completions(SlashCommandCompleter(), "") == [] + 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("caht hello") == "/chat hello" + assert rewrite_friendly_entry_command("get started") == "/start" + + def test_friendly_slash_rewriter_handles_obvious_typos(self): + assert rewrite_friendly_slash_command("/strat") == "/start" + assert rewrite_friendly_slash_command("/caht hello") == "/chat hello" + assert rewrite_friendly_slash_command("/project use .") is None + # -- skill commands via provider ------------------------------------ def test_skill_commands_are_completed_from_provider(self): 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 4ebe203..f2b9206 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,6 +53,7 @@ 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 "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" @@ -70,6 +71,7 @@ fi export PATH="$HOME/.local/bin:$REPO_ROOT/venv/bin:$HOME/.elan/bin:$PATH" export GAUSS_HOME +grep -F 'export GAUSS_HOME="${GAUSS_HOME:-' "$HOME/.bashrc" >/dev/null || die "expected shell block to preserve an explicitly set GAUSS_HOME" echo "==> Verifying core commands" for cmd in gauss uv node npm claude codex elan lake rg tmux ffmpeg; do @@ -82,6 +84,7 @@ 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 "If You Opened This In Morph" "$GAUSS_HOME/guide/index.html" >/dev/null || die "expected generated guide to include Morph guidance" assert_exists "$GAUSS_HOME/autoformalize/assets/lean4-skills/.gauss-managed-revision" diff --git a/tests/test_cli_handoff_command.py b/tests/test_cli_handoff_command.py index 1a31107..224afcb 100644 --- a/tests/test_cli_handoff_command.py +++ b/tests/test_cli_handoff_command.py @@ -347,6 +347,7 @@ 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 @@ -377,6 +378,42 @@ def test_chat_command_with_payload_queues_plain_message(): cli_obj._pending_input.put.assert_called_once_with("Explain what /project init does") +def test_start_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._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 "/project use " in rendered + assert "/prove" in rendered + + +def test_start_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._chat_mode_enabled is True + cli_obj._pending_input.put.assert_called_once_with("I have a theorem but no project yet") + + +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: + assert cli_obj.process_command("/strat") is True + + mock_start.assert_called_once_with("/start") + + def test_handoff_alias_rewrites_to_autoformalize(): cli_obj = _make_cli() diff --git a/tests/test_run_agent.py b/tests/test_run_agent.py index 051296a..c23ebf5 100644 --- a/tests/test_run_agent.py +++ b/tests/test_run_agent.py @@ -549,7 +549,7 @@ 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 /chat" in prompt + assert "point them to /start or /chat" 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/installation.md b/website/docs/getting-started/installation.md index e068fbf..e278b71 100644 --- a/website/docs/getting-started/installation.md +++ b/website/docs/getting-started/installation.md @@ -30,9 +30,10 @@ gauss-open-guide gauss ``` -Inside the CLI, start by selecting a project: +Inside the CLI, the lowest-friction start is: ```text +/start /chat /project init ``` diff --git a/website/docs/getting-started/quickstart.md b/website/docs/getting-started/quickstart.md index 21bae50..8ec8f8c 100644 --- a/website/docs/getting-started/quickstart.md +++ b/website/docs/getting-started/quickstart.md @@ -27,6 +27,7 @@ gauss If you want plain-language help before choosing a project: ```text +/start /chat ``` diff --git a/website/docs/getting-started/start-here.md b/website/docs/getting-started/start-here.md index 3a84da9..5c10ce7 100644 --- a/website/docs/getting-started/start-here.md +++ b/website/docs/getting-started/start-here.md @@ -8,19 +8,22 @@ 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 to ask questions first, use `/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 `/chat` or `/project init`. -- **Local install**: run `./scripts/install.sh`, then `gauss-open-guide` or `gauss`, then start with `/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 `/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`. - **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` asks a plain-language question in the main OpenGauss chat 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. @@ -35,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 `/chat`. +4. If you want orientation first, type `/start` or `/chat`. 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 @@ -76,6 +79,7 @@ gauss Then: +- use `/start` if you want a short first-step guide and plain-language chat mode - use `/chat` if you want a plain-language conversation first - use `/project init` if you are already inside a Lean repository - use `/project create --template-source ` if you need a new project @@ -83,6 +87,7 @@ Then: ## First Useful Examples ```text +/start /chat I have a Lean theorem but I am not sure how to start proving it. /chat What does `/project init` do? /prove Show me how to prove that 1 + 1 = 2 in Lean. @@ -100,7 +105,7 @@ Then: Start with this sequence: -1. `/chat` +1. `/start` 2. Ask one plain question in English. 3. Let OpenGauss explain the next command. 4. Only after that, run `/project ...` diff --git a/website/docs/reference/slash-commands.md b/website/docs/reference/slash-commands.md index 7bfdf40..e13e76b 100644 --- a/website/docs/reference/slash-commands.md +++ b/website/docs/reference/slash-commands.md @@ -12,6 +12,7 @@ Gauss intentionally ships a small default surface. | Command | Description | |---|---| +| `/start [question]` | Show the first-step guide, enable onboarding chat mode, and optionally send a first question. | | `/chat [question]` | Temporarily drop into plain-language chat before selecting a project. | | `/prove [scope or flags]` | Launch the guided managed Lean prove workflow. | | `/draft [topic or flags]` | Launch the managed Lean draft workflow for declaration skeletons. | diff --git a/website/docs/user-guide/cli.md b/website/docs/user-guide/cli.md index 679c7ee..cc20736 100644 --- a/website/docs/user-guide/cli.md +++ b/website/docs/user-guide/cli.md @@ -8,7 +8,7 @@ description: "Use the Gauss terminal interface and launch the managed Lean workf Gauss is a terminal-first product. The public surface is intentionally small. -If you are still orienting yourself, read [Start Here](/docs/getting-started/start-here) first and use `/chat` before choosing a project. +If you are still orienting yourself, read [Start Here](/docs/getting-started/start-here) first and use `/start` or `/chat` before choosing a project. ## Start the CLI @@ -18,7 +18,7 @@ gauss --resume gauss chat -q "hello" ``` -Inside the interactive CLI, `/chat` is the simplest on-ramp when you want to ask a question before selecting a Lean project. +Inside the interactive CLI, `/start` and `/chat` are the simplest on-ramps when you want orientation before selecting a Lean project. ## Primary Workflow @@ -40,6 +40,7 @@ Gauss stages the managed Lean runtime, yields the terminal to the configured bac ## Default Slash Commands +- `/start` - `/chat` - `/prove` - `/draft` From a13bad166dd0f543bc8627c56449bddf5bf54e4d Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Tue, 31 Mar 2026 12:49:06 +0000 Subject: [PATCH 3/6] Harden template installer env handling --- scripts/install-internal.sh | 41 ++++++++++++++++++++++++++++++++++- scripts/install.sh | 6 +++-- tests/test_install_wrapper.py | 2 ++ 3 files changed, 46 insertions(+), 3 deletions(-) diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index 71a92eb..f45dcc9 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -107,6 +107,9 @@ Behavior: Exported non-empty provider keys are written to ~/.gauss/.env. Unset provider keys leave existing ~/.gauss/.env values untouched. Export a provider key as an empty string to clear the staged value. + Template-driven installs ignore ambient provider keys by default; run + `gauss setup` later if you want to stage keys explicitly, or set + OPEN_GAUSS_TRUST_AMBIENT_PROVIDER_ENV=1 to opt back in. TXT } @@ -247,6 +250,31 @@ refresh_paths() { INSTALL_ROOT_FILE="$GAUSS_HOME/install-root" } +ignore_ambient_provider_keys_if_needed() { + if [ -z "${OPEN_GAUSS_REPO_ROOT:-}" ] || [ "${OPEN_GAUSS_TRUST_AMBIENT_PROVIDER_ENV:-0}" = "1" ]; then + return + fi + + local provider_keys=( + OPENROUTER_API_KEY + OPENAI_API_KEY + ANTHROPIC_API_KEY + ) + + local ignored=() + local key + for key in "${provider_keys[@]}"; do + if [ "${!key+x}" = "x" ] && [ -n "${!key}" ]; then + ignored+=("$key") + unset "$key" + fi + done + + if [ "${#ignored[@]}" -gt 0 ]; then + log_info "Ignoring ambient provider keys in template install (${ignored[*]}). Run 'gauss setup' later if you want to stage keys explicitly." + fi +} + set_boolean_from_env() { local env_name="$1" local target_name="$2" @@ -916,11 +944,21 @@ shell_configs = [Path(arg).expanduser() for arg in sys.argv[3:]] block = f"""# >>> gauss workflow installer env >>> export GAUSS_HOME="${{GAUSS_HOME:-{gauss_home}}}" export GAUSS_INSTALL_ROOT="${{GAUSS_INSTALL_ROOT:-{repo_root}}}" -if [ -f "$GAUSS_HOME/.env" ]; then +_gauss_shell_autoenv=1 +case "${{BASH_EXECUTION_STRING:-}}" in + *".opengauss-template/runtime.env"*) + _gauss_shell_autoenv=0 + ;; +esac +if [ "${{OPEN_GAUSS_SKIP_SHELL_AUTOENV:-0}}" = "1" ]; then + _gauss_shell_autoenv=0 +fi +if [ "$_gauss_shell_autoenv" = "1" ] && [ -f "$GAUSS_HOME/.env" ]; then set -a . "$GAUSS_HOME/.env" set +a fi +unset _gauss_shell_autoenv export PATH="$HOME/.local/bin:{repo_root}/venv/bin:$HOME/.elan/bin:$PATH" export PROMPT_TOOLKIT_NO_CPR=1 # <<< gauss workflow installer env <<< @@ -1747,6 +1785,7 @@ main() { install_repo_dependencies link_repo_binaries prepare_gauss_home + ignore_ambient_provider_keys_if_needed sync_optional_provider_keys ensure_workspace initialize_gauss_workspace || true diff --git a/scripts/install.sh b/scripts/install.sh index 1681833..70a1300 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -186,10 +186,12 @@ ensure_runner_venv() { run_local_template() { if [ "${#MORPH_ARGS[@]}" -gt 0 ]; then - "$RUNNER_VENV/bin/morphcloud" devbox template run "$INSTALL_TARGET" --experimental-run-locally "${MORPH_ARGS[@]}" + OPEN_GAUSS_SKIP_SHELL_AUTOENV=1 \ + "$RUNNER_VENV/bin/morphcloud" devbox template run "$INSTALL_TARGET" --experimental-run-locally "${MORPH_ARGS[@]}" return fi - "$RUNNER_VENV/bin/morphcloud" devbox template run "$INSTALL_TARGET" --experimental-run-locally + OPEN_GAUSS_SKIP_SHELL_AUTOENV=1 \ + "$RUNNER_VENV/bin/morphcloud" devbox template run "$INSTALL_TARGET" --experimental-run-locally } parse_args "$@" diff --git a/tests/test_install_wrapper.py b/tests/test_install_wrapper.py index 7ca4227..fb7859f 100644 --- a/tests/test_install_wrapper.py +++ b/tests/test_install_wrapper.py @@ -47,6 +47,7 @@ def test_install_wrapper_translates_installer_flags_for_local_template_run(tmp_p "GAUSS_CREATE_WORKSPACE", "GAUSS_SETUP_MODE", "GAUSS_RECREATE_VENV", + "OPEN_GAUSS_SKIP_SHELL_AUTOENV", ] Path("{env_log}").write_text( "".join(f"{{key}}={{os.environ.get(key, '')}}\\n" for key in keys), @@ -128,6 +129,7 @@ def test_install_wrapper_translates_installer_flags_for_local_template_run(tmp_p "GAUSS_CREATE_WORKSPACE": "1", "GAUSS_SETUP_MODE": "skip", "GAUSS_RECREATE_VENV": "1", + "OPEN_GAUSS_SKIP_SHELL_AUTOENV": "1", } From 2af97f03891be7f3cbb1e94c10b3ae4bb244db61 Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Thu, 2 Apr 2026 01:50:01 +0000 Subject: [PATCH 4/6] Fix macOS installer wrapper bootstrap --- scripts/install.sh | 14 ++++- tests/test_install_wrapper.py | 107 ++++++++++++++++++++++++++++++++-- 2 files changed, 115 insertions(+), 6 deletions(-) diff --git a/scripts/install.sh b/scripts/install.sh index 70a1300..26fc87f 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -181,7 +181,16 @@ ensure_runner_venv() { if [ -e "$RUNNER_VENV" ] || [ -L "$RUNNER_VENV" ]; then recreate_runner_venv fi - uv venv --python "$runner_python" "$RUNNER_VENV" + uv venv --seed --python "$runner_python" "$RUNNER_VENV" +} + +ensure_runner_pip() { + if "$RUNNER_VENV/bin/python" -m pip --version >/dev/null 2>&1; then + return + fi + + "$RUNNER_VENV/bin/python" -m ensurepip --upgrade >/dev/null 2>&1 \ + || die "Failed to bootstrap pip inside $RUNNER_VENV." } run_local_template() { @@ -208,7 +217,8 @@ if ! command -v uv >/dev/null 2>&1; then fi ensure_runner_venv -uv pip install --python "$RUNNER_VENV/bin/python" morphcloud --upgrade +ensure_runner_pip +"$RUNNER_VENV/bin/python" -m pip install --upgrade morphcloud printf 'Running Open Gauss installer flow locally from target: %s\n' "$INSTALL_TARGET" run_local_template diff --git a/tests/test_install_wrapper.py b/tests/test_install_wrapper.py index fb7859f..5b329fe 100644 --- a/tests/test_install_wrapper.py +++ b/tests/test_install_wrapper.py @@ -243,7 +243,7 @@ def test_install_wrapper_prefers_supported_runner_python_when_python3_is_too_new set -euo pipefail printf '%s\\n' "$@" >> "{uv_log}" if [ "$1" = "venv" ]; then - runner_dir="$4/bin" + runner_dir="${{@: -1}}/bin" mkdir -p "$runner_dir" cat > "$runner_dir/python" <<'EOF' #!/usr/bin/env bash @@ -291,8 +291,9 @@ def test_install_wrapper_prefers_supported_runner_python_when_python3_is_too_new assert result.returncode == 0, result.stderr + result.stdout uv_calls = uv_log.read_text(encoding="utf-8").splitlines() - assert uv_calls[:4] == [ + assert uv_calls[:5] == [ "venv", + "--seed", "--python", "3.13", str(repo / ".opengauss-installer-venv"), @@ -348,7 +349,7 @@ def test_install_wrapper_recreates_unsupported_runner_venv(tmp_path): set -euo pipefail printf '%s\\n' "$@" >> "{uv_log}" if [ "$1" = "venv" ]; then - runner_dir="$4/bin" + runner_dir="${{@: -1}}/bin" mkdir -p "$runner_dir" cat > "$runner_dir/python" <<'EOF' #!/usr/bin/env bash @@ -397,8 +398,9 @@ def test_install_wrapper_recreates_unsupported_runner_venv(tmp_path): assert result.returncode == 0, result.stderr + result.stdout uv_calls = uv_log.read_text(encoding="utf-8").splitlines() - assert uv_calls[:4] == [ + assert uv_calls[:5] == [ "venv", + "--seed", "--python", "3.13", str(repo / ".opengauss-installer-venv"), @@ -410,3 +412,100 @@ def test_install_wrapper_recreates_unsupported_runner_venv(tmp_path): "opengauss", "--experimental-run-locally", ] + + +def test_install_wrapper_installs_morphcloud_with_runner_venv_pip(tmp_path): + repo = tmp_path / "repo" + scripts_dir = repo / "scripts" + scripts_dir.mkdir(parents=True) + shutil.copy2(REPO_ROOT / "scripts" / "install.sh", scripts_dir / "install.sh") + + runner_bin = repo / ".opengauss-installer-venv" / "bin" + runner_bin.mkdir(parents=True) + + pip_log = tmp_path / "runner-pip-log.txt" + args_log = tmp_path / "morph-args.txt" + _write_executable( + runner_bin / "python", + f"""#!/usr/bin/env bash + set -euo pipefail + printf '%s\\n' "$@" >> "{pip_log}" + if [ "${{1:-}}" = "-" ]; then + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ]; then + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "ensurepip" ]; then + exit 0 + fi + exit 1 + """, + ) + _write_executable( + runner_bin / "morphcloud", + f"""#!/usr/bin/env bash + set -euo pipefail + printf '%s\\n' "$@" > "{args_log}" + """, + ) + + uv_log = tmp_path / "uv-log.txt" + fake_bin = tmp_path / "bin" + fake_bin.mkdir() + _write_executable( + fake_bin / "uv", + f"""#!/usr/bin/env bash + set -euo pipefail + printf '%s\\n' "$@" >> "{uv_log}" + if [ "$1" = "pip" ]; then + printf '%s\\n' 'uv pip should not be used for the runner venv' >&2 + exit 1 + fi + exit 0 + """, + ) + _write_executable( + fake_bin / "tmux", + """#!/usr/bin/env bash + set -euo pipefail + exit 1 + """, + ) + + env = os.environ.copy() + env["PATH"] = f"{fake_bin}:{env['PATH']}" + env["OPEN_GAUSS_AUTO_ATTACH"] = "0" + + result = subprocess.run( + [ + "bash", + "scripts/install.sh", + "--skip-setup", + ], + cwd=repo, + env=env, + text=True, + capture_output=True, + ) + assert result.returncode == 0, result.stderr + result.stdout + + assert pip_log.read_text(encoding="utf-8").splitlines() == [ + "-", + "-m", + "pip", + "--version", + "-m", + "pip", + "install", + "--upgrade", + "morphcloud", + ] + assert not uv_log.exists() + assert args_log.read_text(encoding="utf-8").splitlines() == [ + "devbox", + "template", + "run", + "opengauss", + "--experimental-run-locally", + ] From 16fc8ecf8970ff95854f2650d1682c22cc3f04fa Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Thu, 2 Apr 2026 01:55:51 +0000 Subject: [PATCH 5/6] Harden installer runner pip bootstrap --- scripts/install.sh | 45 ++++++++- tests/test_install_wrapper.py | 169 ++++++++++++++++++++++++++++++++-- 2 files changed, 202 insertions(+), 12 deletions(-) diff --git a/scripts/install.sh b/scripts/install.sh index 26fc87f..3da71c9 100755 --- a/scripts/install.sh +++ b/scripts/install.sh @@ -185,12 +185,49 @@ ensure_runner_venv() { } ensure_runner_pip() { - if "$RUNNER_VENV/bin/python" -m pip --version >/dev/null 2>&1; then - return + local pip_version_output="" + pip_version_output="$("$RUNNER_VENV/bin/python" -m pip --version 2>/dev/null || true)" + case "$pip_version_output" in + *"from $RUNNER_VENV/"*) + return + ;; + esac + + "$RUNNER_VENV/bin/python" -m ensurepip --upgrade >/dev/null 2>&1 || true + + pip_version_output="$("$RUNNER_VENV/bin/python" -m pip --version 2>/dev/null || true)" + case "$pip_version_output" in + *"from $RUNNER_VENV/"*) + return + ;; + esac + + local runner_python + runner_python="$(select_runner_python)" + + if [ -e "$RUNNER_VENV" ] || [ -L "$RUNNER_VENV" ]; then + recreate_runner_venv fi - "$RUNNER_VENV/bin/python" -m ensurepip --upgrade >/dev/null 2>&1 \ - || die "Failed to bootstrap pip inside $RUNNER_VENV." + uv venv --seed --python "$runner_python" "$RUNNER_VENV" + + pip_version_output="$("$RUNNER_VENV/bin/python" -m pip --version 2>/dev/null || true)" + case "$pip_version_output" in + *"from $RUNNER_VENV/"*) + return + ;; + esac + + "$RUNNER_VENV/bin/python" -m ensurepip --upgrade >/dev/null 2>&1 || die "Failed to bootstrap pip inside $RUNNER_VENV." + + pip_version_output="$("$RUNNER_VENV/bin/python" -m pip --version 2>/dev/null || true)" + case "$pip_version_output" in + *"from $RUNNER_VENV/"*) + return + ;; + esac + + die "Failed to bootstrap pip inside $RUNNER_VENV." } run_local_template() { diff --git a/tests/test_install_wrapper.py b/tests/test_install_wrapper.py index 5b329fe..9e8304a 100644 --- a/tests/test_install_wrapper.py +++ b/tests/test_install_wrapper.py @@ -14,19 +14,38 @@ def _write_executable(path: Path, body: str) -> None: path.chmod(0o755) +def _fake_runner_python_with_local_pip(venv_root: Path) -> str: + return f"""#!/usr/bin/env bash + set -euo pipefail + if [ "${{1:-}}" = "-" ]; then + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ] && [ "${{3:-}}" = "--version" ]; then + printf '%s\\n' 'pip 24.1.2 from {venv_root}/lib/python3.13/site-packages/pip (python 3.13)' + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ]; then + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "ensurepip" ]; then + exit 0 + fi + exit 1 + """ + + def test_install_wrapper_translates_installer_flags_for_local_template_run(tmp_path): repo = tmp_path / "repo" scripts_dir = repo / "scripts" scripts_dir.mkdir(parents=True) shutil.copy2(REPO_ROOT / "scripts" / "install.sh", scripts_dir / "install.sh") + runner_root = repo / ".opengauss-installer-venv" runner_bin = repo / ".opengauss-installer-venv" / "bin" runner_bin.mkdir(parents=True) _write_executable( runner_bin / "python", - """#!/usr/bin/env bash - exit 0 - """, + _fake_runner_python_with_local_pip(runner_root), ) args_log = tmp_path / "morph-args.txt" @@ -139,13 +158,12 @@ def test_install_wrapper_supports_empty_morph_passthrough_on_bash_nounset(tmp_pa scripts_dir.mkdir(parents=True) shutil.copy2(REPO_ROOT / "scripts" / "install.sh", scripts_dir / "install.sh") + runner_root = repo / ".opengauss-installer-venv" runner_bin = repo / ".opengauss-installer-venv" / "bin" runner_bin.mkdir(parents=True) _write_executable( runner_bin / "python", - """#!/usr/bin/env bash - exit 0 - """, + _fake_runner_python_with_local_pip(runner_root), ) args_log = tmp_path / "morph-noargs.txt" @@ -247,7 +265,22 @@ def test_install_wrapper_prefers_supported_runner_python_when_python3_is_too_new mkdir -p "$runner_dir" cat > "$runner_dir/python" <<'EOF' #!/usr/bin/env bash -exit 0 +set -euo pipefail +runner_root="$(cd "$(dirname "$0")/.." && pwd)" +if [ "${1:-}" = "-" ]; then + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "pip" ] && [ "${3:-}" = "--version" ]; then + printf '%s\n' "pip 24.1.2 from $runner_root/lib/python3.13/site-packages/pip (python 3.13)" + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "pip" ]; then + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "ensurepip" ]; then + exit 0 +fi +exit 1 EOF chmod +x "$runner_dir/python" cat > "$runner_dir/morphcloud" <<'EOF' @@ -353,7 +386,22 @@ def test_install_wrapper_recreates_unsupported_runner_venv(tmp_path): mkdir -p "$runner_dir" cat > "$runner_dir/python" <<'EOF' #!/usr/bin/env bash -exit 0 +set -euo pipefail +runner_root="$(cd "$(dirname "$0")/.." && pwd)" +if [ "${1:-}" = "-" ]; then + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "pip" ] && [ "${3:-}" = "--version" ]; then + printf '%s\n' "pip 24.1.2 from $runner_root/lib/python3.13/site-packages/pip (python 3.13)" + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "pip" ]; then + exit 0 +fi +if [ "${1:-}" = "-m" ] && [ "${2:-}" = "ensurepip" ]; then + exit 0 +fi +exit 1 EOF chmod +x "$runner_dir/python" cat > "$runner_dir/morphcloud" <<'EOF' @@ -420,6 +468,7 @@ def test_install_wrapper_installs_morphcloud_with_runner_venv_pip(tmp_path): scripts_dir.mkdir(parents=True) shutil.copy2(REPO_ROOT / "scripts" / "install.sh", scripts_dir / "install.sh") + runner_root = repo / ".opengauss-installer-venv" runner_bin = repo / ".opengauss-installer-venv" / "bin" runner_bin.mkdir(parents=True) @@ -433,6 +482,10 @@ def test_install_wrapper_installs_morphcloud_with_runner_venv_pip(tmp_path): if [ "${{1:-}}" = "-" ]; then exit 0 fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ] && [ "${{3:-}}" = "--version" ]; then + printf '%s\\n' 'pip 24.1.2 from {runner_root}/lib/python3.13/site-packages/pip (python 3.13)' + exit 0 + fi if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ]; then exit 0 fi @@ -509,3 +562,103 @@ def test_install_wrapper_installs_morphcloud_with_runner_venv_pip(tmp_path): "opengauss", "--experimental-run-locally", ] + + +def test_install_wrapper_reseeds_runner_pip_when_existing_runner_uses_external_pip(tmp_path): + repo = tmp_path / "repo" + scripts_dir = repo / "scripts" + scripts_dir.mkdir(parents=True) + shutil.copy2(REPO_ROOT / "scripts" / "install.sh", scripts_dir / "install.sh") + + runner_root = repo / ".opengauss-installer-venv" + runner_bin = runner_root / "bin" + runner_bin.mkdir(parents=True) + + args_log = tmp_path / "runner-pip-log.txt" + morph_args_log = tmp_path / "morph-args.txt" + ensurepip_state = tmp_path / "ensurepip.state" + _write_executable( + runner_bin / "python", + f"""#!/usr/bin/env bash + set -euo pipefail + if [ "${{1:-}}" = "-" ]; then + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ] && [ "${{3:-}}" = "--version" ]; then + if [ -f "{ensurepip_state}" ]; then + printf '%s\\n' 'pip 24.1.2 from {runner_root}/lib/python3.13/site-packages/pip (python 3.13)' + else + printf '%s\\n' 'pip 24.1.2 from /Users/freer/.local/share/uv/python/cpython-3.13.0-macos-aarch64-none/lib/python3.13/site-packages/pip (python 3.13)' + fi + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "ensurepip" ]; then + touch "{ensurepip_state}" + exit 0 + fi + if [ "${{1:-}}" = "-m" ] && [ "${{2:-}}" = "pip" ]; then + printf '%s\\n' "$@" > "{args_log}" + exit 0 + fi + exit 1 + """, + ) + _write_executable( + runner_bin / "morphcloud", + f"""#!/usr/bin/env bash + set -euo pipefail + printf '%s\\n' "$@" > "{morph_args_log}" + """, + ) + + uv_log = tmp_path / "uv-log.txt" + fake_bin = tmp_path / "bin" + fake_bin.mkdir() + _write_executable( + fake_bin / "uv", + f"""#!/usr/bin/env bash + set -euo pipefail + printf '%s\\n' "$@" >> "{uv_log}" + exit 0 + """, + ) + _write_executable( + fake_bin / "tmux", + """#!/usr/bin/env bash + set -euo pipefail + exit 1 + """, + ) + + env = os.environ.copy() + env["PATH"] = f"{fake_bin}:{env['PATH']}" + env["OPEN_GAUSS_AUTO_ATTACH"] = "0" + + result = subprocess.run( + [ + "bash", + "scripts/install.sh", + "--skip-setup", + ], + cwd=repo, + env=env, + text=True, + capture_output=True, + ) + assert result.returncode == 0, result.stderr + result.stdout + assert ensurepip_state.exists() + assert not uv_log.exists() + assert args_log.read_text(encoding="utf-8").splitlines() == [ + "-m", + "pip", + "install", + "--upgrade", + "morphcloud", + ] + assert morph_args_log.read_text(encoding="utf-8").splitlines() == [ + "devbox", + "template", + "run", + "opengauss", + "--experimental-run-locally", + ] From 39b34c1a30f01b493c92e8ae9c8cc97954c88e30 Mon Sep 17 00:00:00 2001 From: gauss-math-inc Date: Thu, 2 Apr 2026 02:13:10 +0000 Subject: [PATCH 6/6] Fix TUI command output rendering --- cli.py | 44 ++++++++++++++++++++++++++--- tests/test_cli_runtime_console.py | 46 +++++++++++++++++++++++++++++++ 2 files changed, 86 insertions(+), 4 deletions(-) create mode 100644 tests/test_cli_runtime_console.py diff --git a/cli.py b/cli.py index a8c45e5..241b687 100755 --- a/cli.py +++ b/cli.py @@ -886,6 +886,43 @@ def print(self, *args, **kwargs): for line in output.rstrip("\n").split("\n"): _cprint(line) + +class RuntimeConsole: + """Route CLI console output through prompt_toolkit once the TUI is active.""" + + def __init__(self, app_getter): + self._app_getter = app_getter + self._rich = Console() + self._chat = ChatConsole() + + def _active_app(self): + try: + return self._app_getter() + except Exception: + return None + + @property + def width(self) -> int: + if self._active_app() is not None: + return shutil.get_terminal_size((80, 24)).columns + return self._rich.width + + def print(self, *args, **kwargs): + if self._active_app() is not None: + return self._chat.print(*args, **kwargs) + return self._rich.print(*args, **kwargs) + + def clear(self): + app = self._active_app() + if app is not None: + output = getattr(app, "output", None) + if output is not None: + output.erase_screen() + output.cursor_goto(0, 0) + output.flush() + return + self._rich.clear() + # ASCII Art - GAUSS-AGENT logo (full width, single line - requires ~95 char terminal) GAUSS_AGENT_LOGO = """[bold #FFD700]██╗ ██╗███████╗██████╗ ███╗ ███╗███████╗███████╗ █████╗ ██████╗ ███████╗███╗ ██╗████████╗[/] [bold #FFD700]██║ ██║██╔════╝██╔══██╗████╗ ████║██╔════╝██╔════╝ ██╔══██╗██╔════╝ ██╔════╝████╗ ██║╚══██╔══╝[/] @@ -1096,8 +1133,9 @@ def __init__( resume: Session ID to resume (restores conversation history from SQLite) pass_session_id: Include the session ID in the agent's system prompt """ - # Initialize Rich console - self.console = Console() + # Route output through prompt_toolkit-safe rendering once the TUI starts. + self._app = None # prompt_toolkit Application (set in run()) + self.console = RuntimeConsole(lambda: self._app) self.config = CLI_CONFIG self.compact = compact if compact is not None else CLI_CONFIG["display"].get("compact", False) # tool_progress: "off", "new", "all", "verbose" (from config.yaml display section) @@ -1212,7 +1250,6 @@ def __init__( # Agent will be initialized on first use self.agent: Optional[AIAgent] = None - self._app = None # prompt_toolkit Application (set in run()) self._input_area = None # Conversation state @@ -1242,7 +1279,6 @@ def __init__( # History file for persistent input recall across sessions self._history_file = _gauss_home / ".gauss_history" self._last_invalidate: float = 0.0 # throttle UI repaints - self._app = None # State shared by interactive run() and single-query chat mode. # These must exist before any direct chat() call because single-query diff --git a/tests/test_cli_runtime_console.py b/tests/test_cli_runtime_console.py new file mode 100644 index 0000000..00cd8c7 --- /dev/null +++ b/tests/test_cli_runtime_console.py @@ -0,0 +1,46 @@ +from unittest.mock import MagicMock + +from cli import RuntimeConsole + + +def test_runtime_console_uses_rich_console_without_tui(): + console = RuntimeConsole(lambda: None) + console._rich.print = MagicMock() + console._chat.print = MagicMock() + + console.print("[bold]hello[/]") + + console._rich.print.assert_called_once_with("[bold]hello[/]") + console._chat.print.assert_not_called() + + +def test_runtime_console_uses_chat_console_with_tui(): + console = RuntimeConsole(lambda: object()) + console._rich.print = MagicMock() + console._chat.print = MagicMock() + + console.print("[bold]hello[/]") + + console._chat.print.assert_called_once_with("[bold]hello[/]") + console._rich.print.assert_not_called() + + +def test_runtime_console_clear_uses_prompt_toolkit_output_when_tui_active(): + output = MagicMock() + app = MagicMock(output=output) + console = RuntimeConsole(lambda: app) + console._rich.clear = MagicMock() + + console.clear() + + output.erase_screen.assert_called_once_with() + output.cursor_goto.assert_called_once_with(0, 0) + output.flush.assert_called_once_with() + console._rich.clear.assert_not_called() + + +def test_runtime_console_width_uses_terminal_size_when_tui_active(monkeypatch): + console = RuntimeConsole(lambda: object()) + monkeypatch.setattr("cli.shutil.get_terminal_size", lambda fallback=(80, 24): MagicMock(columns=123)) + + assert console.width == 123