diff --git a/README.md b/README.md index b3e8df7..f561d2a 100644 --- a/README.md +++ b/README.md @@ -122,7 +122,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 +/chat # Open the configured managed backend chat session first /project create ~/my-project --template-source /prove 1+1=2 # Spawn a proving agent /swarm # See running agents @@ -134,7 +134,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 +/chat # Optional: open the configured managed backend chat session 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 090d92b..2239847 100644 --- a/agent/prompt_builder.py +++ b/agent/prompt_builder.py @@ -67,8 +67,9 @@ def _scan_context_content(content: str, filename: str) -> str: "a general self-summary unless the user explicitly asks. When asked who you " "are, answer briefly and return to the work. " "When the user is trying to use Open Gauss itself or seems unsure how to " - "start, give them the lowest-friction path first: point them to /start or /chat if " - "they want orientation or plain-language help, and point them to /project " + "start, give them the lowest-friction path first: point them to /start if " + "they want inline orientation or plain-language help, point them to /chat " + "if they want a managed Claude Code or Codex chat session, and point them to /project " "when they are ready to create or activate a Gauss project. After that, " "tell them to run /prove, /autoprove, /formalize, or /autoformalize " "followed by a natural-language instruction, for example /autoprove The " diff --git a/cli.py b/cli.py index 241b687..e7ecf9b 100755 --- a/cli.py +++ b/cli.py @@ -63,6 +63,7 @@ AutoformalizeConfigError, AutoformalizeError, normalize_autoformalize_backend_name, + resolve_managed_chat_request, rewrite_forgiving_managed_command, resolve_autoformalize_request, supported_autoformalize_backends, @@ -1036,6 +1037,27 @@ def _parse_skills_argument(skills: str | list[str] | tuple[str, ...] | None) -> return parsed +def _parse_startup_inputs_argument( + startup_input: str | list[str] | tuple[str, ...] | None, +) -> list[str]: + """Normalize one or more startup inputs into an ordered list.""" + if startup_input is None: + return [] + if isinstance(startup_input, str): + raw_values = [startup_input] + elif isinstance(startup_input, (list, tuple)): + raw_values = [str(item) for item in startup_input if item is not None] + else: + raw_values = [str(startup_input)] + + parsed: list[str] = [] + for raw in raw_values: + normalized = raw.strip() + if normalized: + parsed.append(normalized) + return parsed + + def save_config_value(key_path: str, value: any) -> bool: """ Save a value to the active config file at the specified key path. @@ -1117,6 +1139,7 @@ def __init__( resume: str = None, checkpoints: bool = False, pass_session_id: bool = False, + startup_inputs: list[str] | None = None, ): """ Initialize the Gauss CLI. @@ -1132,6 +1155,7 @@ def __init__( compact: Use compact display mode resume: Session ID to resume (restores conversation history from SQLite) pass_session_id: Include the session ID in the agent's system prompt + startup_inputs: Commands or messages to enqueue when the interactive UI starts """ # Route output through prompt_toolkit-safe rendering once the TUI starts. self._app = None # prompt_toolkit Application (set in run()) @@ -1305,6 +1329,7 @@ def __init__( self._image_counter = 0 self.preloaded_skills: list[str] = [] self._startup_skills_line_shown = False + self._startup_inputs = list(startup_inputs or []) # Voice mode state (also reinitialized inside run() for interactive TUI). self._voice_lock = threading.Lock() @@ -1619,6 +1644,7 @@ def _slow_command_status(self, command: str) -> str: cmd_lower.startswith("/autoformalize") or cmd_lower.startswith("/auto_formalize") or cmd_lower.startswith("/auto-formalize") + or cmd_lower.startswith("/chat") or cmd_lower.startswith("/draft") or cmd_lower.startswith("/formalize") or cmd_lower.startswith("/prove") @@ -2397,7 +2423,7 @@ def show_help(self): _cprint(f"\n {_DIM}Active project: {project_summary}{_RST}") else: _cprint( - f"\n {_DIM}No active project — use /start or /chat for orientation, or /project init, " + f"\n {_DIM}No active project — use /start for inline onboarding, /chat for managed backend chat, or /project init, " f"/project convert, /project create , or /project use .{_RST}" ) @@ -2414,7 +2440,7 @@ def show_help(self): ) _cprint( - 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"\n {_DIM}Tip: Start with /start for inline onboarding or /chat for managed backend chat if you want orientation first. Use /project when you're ready to work in a Lean repo, " f"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}") @@ -3385,8 +3411,8 @@ def _print_project_lock_notice(self, *, command_label: str) -> None: f"{prefix} Use /project init, /project convert, /project create , or /project use first.", ) self._print_surface_notice( - "[dim]If you only want orientation first, run `/start` or `/chat` and ask a plain-language question.[/]", - "If you only want orientation first, run /start or /chat and ask a plain-language question.", + "[dim]If you only want orientation first, run `/start` for inline onboarding chat or `/chat` for the configured managed backend chat session.[/]", + "If you only want orientation first, run /start for inline onboarding chat or /chat for the configured managed backend chat session.", ) self._print_surface_notice( f"[dim]{detail}[/]", @@ -3419,56 +3445,119 @@ def _enforce_project_lock(self, command: str) -> bool: self._print_project_lock_notice(command_label=command_label) return True + @staticmethod + def _wait_for_interactive_swarm_task(task) -> tuple[int | None, str]: + """Wait briefly for an interactive swarm task PTY to become attachable.""" + task_pty_master_fd = getattr(task, "pty_master_fd", None) + task_status = getattr(task, "status", "running") + for _ in range(20): + if task_pty_master_fd is not None and task_status == "running": + break + time.sleep(0.1) + task_pty_master_fd = getattr(task, "pty_master_fd", None) + task_status = getattr(task, "status", "running") + return task_pty_master_fd, task_status + + def _attach_spawned_interactive_task( + self, + task, + *, + fallback_spawned_message: str, + fallback_attach_message: str, + ) -> None: + """Attach to an interactive swarm task when ready, or print fallback guidance.""" + task_pty_master_fd, task_status = self._wait_for_interactive_swarm_task(task) + if task_pty_master_fd is not None and task_status == "running": + self._attach_to_swarm_task(task.task_id) + return + + cc = ChatConsole() + cc.print(fallback_spawned_message) + cc.print(fallback_attach_message) + + def _active_managed_backend_name(self) -> str: + """Return the normalized backend used for managed chat and Lean workflows.""" + available = supported_autoformalize_backends() + active_backend_raw = ( + os.environ.get("GAUSS_AUTOFORMALIZE_BACKEND") + or self.config.get("gauss", {}).get("autoformalize", {}).get("backend", "") + or available[0] + ) + try: + return normalize_autoformalize_backend_name(active_backend_raw) + except AutoformalizeConfigError: + return str(active_backend_raw or available[0]) + + def _spawn_managed_chat_session(self, payload: str): + """Launch a managed provider chat child session and return the task metadata.""" + plan = resolve_managed_chat_request( + payload, + self.config, + active_cwd=self._active_handoff_cwd(), + ) + + swarm = SwarmManager() + description = payload.strip() or "managed chat" + task = swarm.spawn_interactive( + theorem=payload.strip() or "managed chat", + description=description, + argv=list(plan.handoff_request.argv), + cwd=plan.handoff_request.cwd, + env=plan.handoff_request.env, + workflow_kind="chat", + workflow_command="/chat", + backend_name=plan.backend_name, + ) + return task, description, plan.backend_name + def _handle_chat_command(self, cmd: str): - """Handle `/chat` onboarding mode before project selection.""" + """Handle `/chat` by opening the configured managed backend chat session.""" 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 + if lowered == "status": + active_backend = self._active_managed_backend_name() 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.", + "[dim]`/chat` opens the configured managed backend chat session " + f"(`{active_backend}`). Use `/autoformalize-backend` to switch backends, or `/start` " + "for inline onboarding chat in the current Gauss session.[/]", + f"`/chat` opens the configured managed backend chat session ({active_backend}). " + "Use /autoformalize-backend to switch backends, or /start for inline onboarding chat in the current Gauss session.", ) 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.", + "[dim]Inline `/chat` mode has been removed. " + "Use `/start` for inline onboarding chat, or run `/chat` to open the managed backend chat session.[/]", + "Inline /chat mode has been removed. Use /start for inline onboarding chat, or run /chat to open the managed backend chat session.", ) 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 + if lowered in {"on", "enable", "start"}: + payload = "" - 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.", + task = None + description = payload.strip() or "managed chat" + backend_name = self._active_managed_backend_name() + with self._busy_command(self._slow_command_status("/chat")): + try: + task, description, backend_name = self._spawn_managed_chat_session(payload) + except (AutoformalizeError, HandoffError) as exc: + print(f"(>_<) {exc}") + return + self._attach_spawned_interactive_task( + task, + fallback_spawned_message=( + f"[dim]Spawned managed chat session {task.task_id} " + f"({backend_name}): {description}[/]" + ), + fallback_attach_message=( + f"[dim]Use `/swarm attach {task.task_id}` to connect. " + f"`/swarm` for status. Ctrl-] to detach.[/]" + ), ) - if hasattr(self, "_pending_input") and hasattr(self._pending_input, "put"): - self._pending_input.put(payload) - else: - self._print_surface_notice( - "[bold yellow]Chat queue is not available in this mode.[/]", - "Chat queue is not available in this mode.", - ) def _handle_start_command(self, cmd: str): """Handle `/start` with a short first-step guide and chat-mode enablement.""" @@ -3482,9 +3571,9 @@ def _handle_start_command(self, cmd: str): "`/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, " + "[dim]Next: use `/chat` if you want the configured managed backend chat session, `/project use ` for an existing Lean repo, " "`/project init` in the current repo, or `/project create --template-source ` for a new one.[/]", - "Next: use /chat 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 if you want the configured managed backend chat session, /project use for an existing Lean repo, /project init in the current repo, or /project create --template-source for a new one.", ) self._print_surface_notice( "[dim]When the project is ready, run `/prove`, `/review`, `/draft`, `/autoprove`, or `/swarm`.[/]", @@ -3789,28 +3878,16 @@ def _handle_interactive_workflow_command(self, cmd: str): project_root=str(plan.project.root), backend_name=plan.managed_context.backend_name, ) - - # Wait briefly for the PTY to become available before attaching - task_pty_master_fd = getattr(task, "pty_master_fd", None) - task_status = getattr(task, "status", "running") - for _ in range(20): - if task_pty_master_fd is not None and task_status == "running": - break - time.sleep(0.1) - task_pty_master_fd = getattr(task, "pty_master_fd", None) - task_status = getattr(task, "status", "running") - - if task_pty_master_fd is not None and task_status == "running": - self._attach_to_swarm_task(task.task_id) - else: - cc = ChatConsole() - cc.print( + self._attach_spawned_interactive_task( + task, + fallback_spawned_message=( f"[dim]Spawned {plan.workflow_kind} agent {task.task_id}: {description}[/]" - ) - cc.print( + ), + fallback_attach_message=( f"[dim]Use `/swarm attach {task.task_id}` to connect. " f"`/swarm` for status. Ctrl-] to detach.[/]" - ) + ), + ) def _handle_autoformalize_command(self, cmd: str): """Backward-compatible wrapper for managed Lean workflow launching.""" @@ -6324,10 +6401,10 @@ def run(self): try: from gauss_cli.skin_engine import get_active_skin _welcome_skin = get_active_skin() - _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.") + _welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.") _welcome_color = _welcome_skin.get_color("banner_text", "#FFF8DC") except Exception: - _welcome_text = "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands." + _welcome_text = "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands." _welcome_color = "#FFF8DC" self.console.print(f"[{_welcome_color}]{_welcome_text}[/]") self.console.print() @@ -7405,7 +7482,10 @@ def _restart_recording(): # Start processing thread process_thread = threading.Thread(target=process_loop, daemon=True) process_thread.start() - + + for startup_input in getattr(self, "_startup_inputs", []) or []: + self._pending_input.put(startup_input) + # Register atexit cleanup so resources are freed even on unexpected exit atexit.register(_run_cleanup) @@ -7475,6 +7555,7 @@ def main( w: bool = False, checkpoints: bool = False, pass_session_id: bool = False, + startup_input: str | list[str] | tuple[str, ...] = None, ): """ Gauss CLI - Interactive AI Assistant @@ -7496,6 +7577,7 @@ def main( resume: Resume a previous session by its ID (e.g., 20260225_143052_a1b2c3) worktree: Run in an isolated git worktree (for parallel agents). Alias: -w w: Shorthand for --worktree + startup_input: Initial commands or messages queued when interactive mode starts Examples: python cli.py # Start interactive mode @@ -7571,6 +7653,7 @@ def main( toolsets_list = ["gauss-cli"] parsed_skills = _parse_skills_argument(skills) + parsed_startup_inputs = _parse_startup_inputs_argument(startup_input) # Create CLI instance cli = GaussCLI( @@ -7585,6 +7668,7 @@ def main( resume=resume, checkpoints=checkpoints, pass_session_id=pass_session_id, + startup_inputs=parsed_startup_inputs, ) if parsed_skills: diff --git a/gauss_cli/autoformalize.py b/gauss_cli/autoformalize.py index 5157996..fa5b6a8 100644 --- a/gauss_cli/autoformalize.py +++ b/gauss_cli/autoformalize.py @@ -1,4 +1,4 @@ -"""Managed Lean autoformalization launcher for Gauss.""" +"""Managed backend session launchers for Gauss.""" from __future__ import annotations @@ -217,6 +217,52 @@ def staged_paths(self) -> dict[str, str]: } +@dataclass(frozen=True) +class ManagedChatRuntime: + """Backend-specific launch arguments and environment for `/chat`.""" + + argv: list[str] + child_env: dict[str, str] + backend_name: str + + +@dataclass(frozen=True) +class ManagedChatLaunchPlan: + """Managed launch plan for `/chat`.""" + + handoff_request: HandoffRequest + backend_name: str + user_instruction: str + active_cwd: Path + + def staged_paths(self) -> dict[str, str]: + """Return the most useful launch metadata for diagnostics/tests.""" + return { + "backend_name": self.backend_name, + "cwd": str(self.active_cwd), + "argv0": self.handoff_request.argv[0] if self.handoff_request.argv else "", + } + + +@dataclass(frozen=True) +class ClaudeAuthStagingPlan: + """Resolved Claude auth inputs for a managed child session.""" + + auth_env: dict[str, str] + copy_oauth_credentials: bool + copy_local_api_key: bool + strip_child_auth_env: bool + + +@dataclass(frozen=True) +class CodexAuthStagingPlan: + """Resolved Codex auth inputs for a managed child session.""" + + copy_local_auth: bool + staged_api_key: str + source_auth_path: Path | None + + @dataclass(frozen=True) class SharedLeanBundle: """Shared Lean assets and paths for a managed autoformalization run.""" @@ -239,6 +285,19 @@ class SharedLeanBundle: skill_revision: str +@dataclass(frozen=True) +class ManagedChatLeanAssets: + """Pinned Lean skill assets that `/chat` can reuse when available.""" + + assets_root: Path + checkout_root: Path + plugin_source: Path + skill_source: Path + scripts_root: Path + references_root: Path + skill_revision: str + + @dataclass(frozen=True) class AutoformalizeBackendRuntime: """Backend-specific launch arguments, environment, and managed context.""" @@ -262,6 +321,51 @@ def cli_only_autoformalize_message() -> str: return cli_only_managed_workflow_message("/autoformalize") +def resolve_managed_chat_request( + user_instruction: str, + config: Mapping[str, Any] | None, + *, + active_cwd: str | None = None, + base_env: Mapping[str, str] | None = None, +) -> ManagedChatLaunchPlan: + """Resolve `/chat` into a managed backend interactive session.""" + include_persisted_env = base_env is None + base_environment = dict(base_env or os.environ) + active_dir = Path(active_cwd or base_environment.get("TERMINAL_CWD") or os.getcwd()).expanduser().resolve() + if not active_dir.exists(): + raise AutoformalizePreflightError(f"Active working directory does not exist: {active_dir}") + + backend_name = _resolve_backend_name(config, base_environment) + requested_mode = _resolve_requested_mode(config) + auth_mode = _resolve_auth_mode(config, base_environment) + managed_state_base = _resolve_managed_state_base(config, base_environment) + real_home = Path(base_environment.get("HOME", str(Path.home()))).expanduser().resolve() + runtime = _resolve_managed_chat_runtime( + backend_name=backend_name, + auth_mode=auth_mode, + user_instruction=str(user_instruction or "").strip(), + base_environment=base_environment, + include_persisted_env=include_persisted_env, + active_cwd=active_dir, + managed_state_base=managed_state_base, + real_home=real_home, + ) + handoff_request = build_handoff_request( + argv=runtime.argv, + cwd=str(active_dir), + env=runtime.child_env, + requested_mode=requested_mode, + label="Gauss chat session", + source="gauss:chat", + ) + return ManagedChatLaunchPlan( + handoff_request=handoff_request, + backend_name=runtime.backend_name, + user_instruction=str(user_instruction or "").strip(), + active_cwd=active_dir, + ) + + def rewrite_forgiving_managed_command(command: str) -> str | None: """Rewrite obvious managed-workflow intents like ``prove`` into slash commands.""" if not isinstance(command, str): @@ -1223,13 +1327,15 @@ def _has_local_claude_api_key(real_home: Path) -> bool: return bool(str(data.get("primaryApiKey", "")).strip()) -def _local_codex_auth_path(real_home: Path, env: Mapping[str, str]) -> Path: +def _local_codex_home(real_home: Path, env: Mapping[str, str]) -> Path: configured_home = str(env.get("CODEX_HOME", "") or "").strip() if configured_home: - codex_home = Path(configured_home).expanduser() - else: - codex_home = real_home / ".codex" - return codex_home / "auth.json" + return Path(configured_home).expanduser() + return real_home / ".codex" + + +def _local_codex_auth_path(real_home: Path, env: Mapping[str, str]) -> Path: + return _local_codex_home(real_home, env) / "auth.json" def _load_local_codex_auth_payload(real_home: Path, env: Mapping[str, str]) -> dict[str, Any]: @@ -1262,6 +1368,44 @@ def _codex_auth_payload_has_api_key(payload: Mapping[str, Any]) -> bool: return auth_mode == "apikey" and bool(str(payload.get("OPENAI_API_KEY", "")).strip()) +def _prepare_managed_chat_lean_assets( + *, + managed_state_base: Path, + env: Mapping[str, str], +) -> ManagedChatLeanAssets | None: + assets_root = managed_state_base / "assets" + assets_root.mkdir(parents=True, exist_ok=True) + checkout_root = _lean4_checkout_root(assets_root) + git_executable = shutil.which("git", path=env.get("PATH")) + if git_executable is None: + if not _lean4_checkout_is_complete(checkout_root): + return None + skill_revision = _read_lean4_checkout_revision(checkout_root) + if not skill_revision: + return None + else: + try: + checkout_root, skill_revision = _ensure_lean4_checkout_assets( + assets_root=assets_root, + env=env, + git_executable=git_executable, + refresh=False, + ) + except AutoformalizeStagingError: + return None + + plugin_source, skill_source, scripts_root, references_root = _lean4_checkout_paths(checkout_root) + return ManagedChatLeanAssets( + assets_root=assets_root, + checkout_root=checkout_root, + plugin_source=plugin_source, + skill_source=skill_source, + scripts_root=scripts_root, + references_root=references_root, + skill_revision=skill_revision, + ) + + def _prepare_shared_bundle( *, backend_name: str, @@ -1345,21 +1489,47 @@ def _resolve_backend_runtime( raise AutoformalizeConfigError(f"Unsupported autoformalize backend: {backend_name}") -def _build_claude_runtime( +def _resolve_managed_chat_runtime( *, + backend_name: str, auth_mode: str, user_instruction: str, - workflow: ManagedWorkflowSpec, base_environment: Mapping[str, str], include_persisted_env: bool, - shared_bundle: SharedLeanBundle, -) -> AutoformalizeBackendRuntime: - claude_exe = _require_executable( - "claude", - "Claude Code CLI not found. Install it with `npm install -g @anthropic-ai/claude-code`.", - base_environment, - ) - real_home = shared_bundle.real_home + active_cwd: Path, + managed_state_base: Path, + real_home: Path, +) -> ManagedChatRuntime: + if backend_name == DEFAULT_AUTOFORMALIZE_BACKEND: + return _build_claude_chat_runtime( + auth_mode=auth_mode, + user_instruction=user_instruction, + base_environment=base_environment, + include_persisted_env=include_persisted_env, + active_cwd=active_cwd, + managed_state_base=managed_state_base, + real_home=real_home, + ) + if backend_name == CODEX_AUTOFORMALIZE_BACKEND: + return _build_codex_chat_runtime( + auth_mode=auth_mode, + user_instruction=user_instruction, + base_environment=base_environment, + include_persisted_env=include_persisted_env, + active_cwd=active_cwd, + managed_state_base=managed_state_base, + real_home=real_home, + ) + raise AutoformalizeConfigError(f"Unsupported autoformalize backend: {backend_name}") + + +def _resolve_claude_auth_staging_plan( + *, + auth_mode: str, + real_home: Path, + base_environment: Mapping[str, str], + include_persisted_env: bool, +) -> ClaudeAuthStagingPlan: has_local_login = _has_local_claude_login(real_home) has_local_api_key = _has_local_claude_api_key(real_home) resolved_auth_env = _resolve_claude_auth_env( @@ -1400,6 +1570,85 @@ def _build_claude_runtime( "`gauss.autoformalize.auth_mode` back to `auto` or `login`." ) + return ClaudeAuthStagingPlan( + auth_env=auth_env, + copy_oauth_credentials=copy_oauth_credentials, + copy_local_api_key=copy_local_api_key, + strip_child_auth_env=strip_child_auth_env, + ) + + +def _resolve_codex_auth_staging_plan( + *, + auth_mode: str, + real_home: Path, + base_environment: Mapping[str, str], + include_persisted_env: bool, +) -> CodexAuthStagingPlan: + local_auth_path = _local_codex_auth_path(real_home, base_environment) + local_auth_payload = _load_local_codex_auth_payload(real_home, base_environment) + has_local_auth = _codex_auth_payload_is_valid(local_auth_payload) + has_local_api_key = _codex_auth_payload_has_api_key(local_auth_payload) + openai_api_key = _resolve_codex_api_key( + base_environment, + include_persisted_env=include_persisted_env, + ) + copy_local_auth = False + staged_api_key = "" + + if auth_mode == "auto": + if has_local_auth: + copy_local_auth = True + elif openai_api_key: + staged_api_key = openai_api_key + else: + raise AutoformalizePreflightError( + "Codex auth not found. Run `codex login`, save `OPENAI_API_KEY`, " + "or set `gauss.autoformalize.auth_mode: login` " + "(or `GAUSS_AUTOFORMALIZE_AUTH_MODE=login`) to launch the normal Codex login flow." + ) + elif auth_mode == "login": + copy_local_auth = has_local_auth + else: + if openai_api_key: + staged_api_key = openai_api_key + elif has_local_api_key: + copy_local_auth = True + else: + raise AutoformalizePreflightError( + "Codex API-key auth not found. Save `OPENAI_API_KEY`, or switch " + "`gauss.autoformalize.auth_mode` back to `auto` or `login`." + ) + + return CodexAuthStagingPlan( + copy_local_auth=copy_local_auth, + staged_api_key=staged_api_key, + source_auth_path=local_auth_path if copy_local_auth else None, + ) + + +def _build_claude_runtime( + *, + auth_mode: str, + user_instruction: str, + workflow: ManagedWorkflowSpec, + base_environment: Mapping[str, str], + include_persisted_env: bool, + shared_bundle: SharedLeanBundle, +) -> AutoformalizeBackendRuntime: + claude_exe = _require_executable( + "claude", + "Claude Code CLI not found. Install it with `npm install -g @anthropic-ai/claude-code`.", + base_environment, + ) + real_home = shared_bundle.real_home + auth_plan = _resolve_claude_auth_staging_plan( + auth_mode=auth_mode, + real_home=real_home, + base_environment=base_environment, + include_persisted_env=include_persisted_env, + ) + backend_home = shared_bundle.managed_root / "claude-home" backend_config_path = backend_home / ".claude.json" mcp_config_path = shared_bundle.mcp_dir / "lean-lsp.mcp.json" @@ -1432,9 +1681,9 @@ def _build_claude_runtime( _stage_claude_credentials( real_home=real_home, claude_home=backend_home, - auth_env=auth_env, - copy_oauth_credentials=copy_oauth_credentials, - copy_local_api_key=copy_local_api_key, + auth_env=auth_plan.auth_env, + copy_oauth_credentials=auth_plan.copy_oauth_credentials, + copy_local_api_key=auth_plan.copy_local_api_key, mcp_servers={"lean-lsp": mcp_server}, ) startup_context_path = _write_startup_context( @@ -1467,10 +1716,10 @@ def _build_claude_runtime( ) child_env = dict(base_environment) - if strip_child_auth_env: + if auth_plan.strip_child_auth_env: for key in CLAUDE_AUTH_ENV_KEYS: child_env.pop(key, None) - child_env.update(auth_env) + child_env.update(auth_plan.auth_env) child_env.update( _base_child_env( managed_context=managed_context, @@ -1513,6 +1762,126 @@ def _build_claude_runtime( ) +def _managed_chat_backend_label(backend_name: str) -> str: + if backend_name == DEFAULT_AUTOFORMALIZE_BACKEND: + return "Claude Code" + if backend_name == CODEX_AUTOFORMALIZE_BACKEND: + return "Codex" + return backend_name + + +def _build_managed_chat_prompt( + *, + backend_name: str, + active_cwd: Path, + user_instruction: str, +) -> str: + backend_label = _managed_chat_backend_label(backend_name) + prompt_parts = [ + f"You are {backend_label} in a Gauss-managed interactive chat session.", + "The user launched `/chat` from the main Gauss CLI and will return there when this session exits.", + f"Current working directory: {active_cwd}.", + "Use this session for onboarding, planning, repository questions, and general discussion before a specific Lean workflow is selected.", + "Use any skills and MCP tools that are already configured in this backend session when they are helpful.", + "If the user is ready to work in Lean, tell them to return to the main Gauss session and use `/project init`, `/project use`, or `/project create`, then `/prove`, `/review`, `/draft`, `/autoprove`, `/formalize`, or `/autoformalize`.", + ] + normalized_instruction = user_instruction.strip() + if normalized_instruction: + prompt_parts.append(f"Initial user request: {normalized_instruction}") + else: + prompt_parts.append("Start by asking what the user wants to do in Open Gauss.") + return " ".join(prompt_parts) + + +def _build_claude_chat_runtime( + *, + auth_mode: str, + user_instruction: str, + base_environment: Mapping[str, str], + include_persisted_env: bool, + active_cwd: Path, + managed_state_base: Path, + real_home: Path, +) -> ManagedChatRuntime: + claude_exe = _require_executable( + "claude", + "Claude Code CLI not found. Install it with `npm install -g @anthropic-ai/claude-code`.", + base_environment, + ) + auth_plan = _resolve_claude_auth_staging_plan( + auth_mode=auth_mode, + real_home=real_home, + base_environment=base_environment, + include_persisted_env=include_persisted_env, + ) + managed_root = _managed_chat_root(managed_state_base, DEFAULT_AUTOFORMALIZE_BACKEND) + backend_home = managed_root / "claude-home" + lean_assets = _prepare_managed_chat_lean_assets( + managed_state_base=managed_state_base, + env=base_environment, + ) + backend_home.mkdir(parents=True, exist_ok=True) + + plugin_root = _sync_prewarmed_claude_plugin( + real_home=real_home, + backend_home=backend_home, + ) + if plugin_root is None and lean_assets is not None: + plugin_root = _install_managed_claude_plugin( + claude_executable=claude_exe, + backend_home=backend_home, + base_environment=base_environment, + marketplace_source=lean_assets.checkout_root, + plugin_source=lean_assets.plugin_source, + ) + _stage_claude_credentials( + real_home=real_home, + claude_home=backend_home, + auth_env=auth_plan.auth_env, + copy_oauth_credentials=auth_plan.copy_oauth_credentials, + copy_local_api_key=auth_plan.copy_local_api_key, + ) + + child_env = dict(base_environment) + if auth_plan.strip_child_auth_env: + for key in CLAUDE_AUTH_ENV_KEYS: + child_env.pop(key, None) + child_env.update(auth_plan.auth_env) + child_env.update( + { + "GAUSS_MANAGED_CHAT": "1", + "GAUSS_MANAGED_CHAT_BACKEND": DEFAULT_AUTOFORMALIZE_BACKEND, + "GAUSS_CHAT_CWD": str(active_cwd), + "GAUSS_MANAGED_STATE_DIR": str(managed_root), + "GAUSS_REAL_HOME": str(real_home), + "HOME": str(backend_home), + "GAUSS_YOLO_MODE": "1", + } + ) + if plugin_root is not None: + child_env.update( + { + "CLAUDE_PLUGIN_ROOT": str(plugin_root), + "LEAN4_PLUGIN_ROOT": str(plugin_root), + "LEAN4_SCRIPTS": str(plugin_root / "lib" / "scripts"), + "LEAN4_REFS": str(plugin_root / "skills" / "lean4" / "references"), + } + ) + argv = [claude_exe] + prompt = _build_managed_chat_prompt( + backend_name=DEFAULT_AUTOFORMALIZE_BACKEND, + active_cwd=active_cwd, + user_instruction=user_instruction, + ) + if prompt: + argv.append(prompt) + return ManagedChatRuntime( + argv=argv, + child_env=child_env, + backend_name=DEFAULT_AUTOFORMALIZE_BACKEND, + ) + + def _build_codex_runtime( *, auth_mode: str, @@ -1528,40 +1897,12 @@ def _build_codex_runtime( base_environment, ) real_home = shared_bundle.real_home - local_auth_path = _local_codex_auth_path(real_home, base_environment) - local_auth_payload = _load_local_codex_auth_payload(real_home, base_environment) - has_local_auth = _codex_auth_payload_is_valid(local_auth_payload) - has_local_api_key = _codex_auth_payload_has_api_key(local_auth_payload) - openai_api_key = _resolve_codex_api_key( - base_environment, + auth_plan = _resolve_codex_auth_staging_plan( + auth_mode=auth_mode, + real_home=real_home, + base_environment=base_environment, include_persisted_env=include_persisted_env, ) - copy_local_auth = False - staged_api_key = "" - - if auth_mode == "auto": - if has_local_auth: - copy_local_auth = True - elif openai_api_key: - staged_api_key = openai_api_key - else: - raise AutoformalizePreflightError( - "Codex auth not found. Run `codex login`, save `OPENAI_API_KEY`, " - "or set `gauss.autoformalize.auth_mode: login` " - "(or `GAUSS_AUTOFORMALIZE_AUTH_MODE=login`) to launch the normal Codex login flow." - ) - elif auth_mode == "login": - copy_local_auth = has_local_auth - else: - if openai_api_key: - staged_api_key = openai_api_key - elif has_local_api_key: - copy_local_auth = True - else: - raise AutoformalizePreflightError( - "Codex API-key auth not found. Save `OPENAI_API_KEY`, or switch " - "`gauss.autoformalize.auth_mode` back to `auto` or `login`." - ) backend_home = shared_bundle.managed_root / "codex-home" codex_home = backend_home / ".codex" @@ -1578,8 +1919,8 @@ def _build_codex_runtime( ) _stage_codex_auth( codex_home=codex_home, - source_auth_path=local_auth_path if copy_local_auth else None, - api_key=staged_api_key, + source_auth_path=auth_plan.source_auth_path, + api_key=auth_plan.staged_api_key, ) startup_context_path = _write_startup_context( @@ -1672,6 +2013,120 @@ def _build_codex_runtime( ) +def _build_codex_chat_runtime( + *, + auth_mode: str, + user_instruction: str, + base_environment: Mapping[str, str], + include_persisted_env: bool, + active_cwd: Path, + managed_state_base: Path, + real_home: Path, +) -> ManagedChatRuntime: + codex_exe = _require_executable( + "codex", + "Codex CLI not found. Install the OpenAI Codex CLI and try again.", + base_environment, + ) + auth_plan = _resolve_codex_auth_staging_plan( + auth_mode=auth_mode, + real_home=real_home, + base_environment=base_environment, + include_persisted_env=include_persisted_env, + ) + managed_root = _managed_chat_root(managed_state_base, CODEX_AUTOFORMALIZE_BACKEND) + backend_home = managed_root / "codex-home" + codex_home = backend_home / ".codex" + lean_assets = _prepare_managed_chat_lean_assets( + managed_state_base=managed_state_base, + env=base_environment, + ) + source_codex_home = _local_codex_home(real_home, base_environment) + for path in (backend_home, codex_home): + path.mkdir(parents=True, exist_ok=True) + _stage_optional_file_copy( + source=source_codex_home / "config.toml", + destination=codex_home / "config.toml", + ) + _stage_optional_tree_copy( + source=source_codex_home / "skills", + destination=codex_home / "skills", + ) + _stage_optional_tree_copy( + source=source_codex_home / ".tmp" / "plugins", + destination=codex_home / ".tmp" / "plugins", + ) + _stage_optional_tree_copy( + source=real_home / ".agents" / "skills", + destination=backend_home / ".agents" / "skills", + ) + _stage_optional_tree_copy( + source=real_home / ".agents" / "plugins", + destination=backend_home / ".agents" / "plugins", + ) + + staged_skill_root: Path | None = None + if lean_assets is not None: + staged_skill_root = backend_home / ".agents" / "skills" / "lean4" + _stage_tree( + source=lean_assets.skill_source, + destination=staged_skill_root, + revision=lean_assets.skill_revision, + ) + _stage_tree( + source=lean_assets.skill_source, + destination=codex_home / "skills" / "lean4", + revision=lean_assets.skill_revision, + ) + _stage_codex_auth( + codex_home=codex_home, + source_auth_path=auth_plan.source_auth_path, + api_key=auth_plan.staged_api_key, + ) + + child_env = dict(base_environment) + for key in CODEX_AUTH_ENV_KEYS: + child_env.pop(key, None) + child_env.update( + { + "GAUSS_MANAGED_CHAT": "1", + "GAUSS_MANAGED_CHAT_BACKEND": CODEX_AUTOFORMALIZE_BACKEND, + "GAUSS_CHAT_CWD": str(active_cwd), + "GAUSS_MANAGED_STATE_DIR": str(managed_root), + "GAUSS_REAL_HOME": str(real_home), + "HOME": str(backend_home), + "CODEX_HOME": str(codex_home), + "GAUSS_YOLO_MODE": "1", + } + ) + if lean_assets is not None: + child_env.update( + { + "LEAN4_PLUGIN_ROOT": str(lean_assets.plugin_source), + "LEAN4_SCRIPTS": str(lean_assets.scripts_root), + } + ) + if staged_skill_root is not None: + child_env["GAUSS_AUTOFORMALIZE_SKILLS_ROOT"] = str(staged_skill_root) + child_env["LEAN4_REFS"] = str(staged_skill_root / "references") + argv = [ + codex_exe, + "--dangerously-bypass-approvals-and-sandbox", + ] + prompt = _build_managed_chat_prompt( + backend_name=CODEX_AUTOFORMALIZE_BACKEND, + active_cwd=active_cwd, + user_instruction=user_instruction, + ) + if prompt: + argv.append(prompt) + return ManagedChatRuntime( + argv=argv, + child_env=child_env, + backend_name=CODEX_AUTOFORMALIZE_BACKEND, + ) + + def _base_child_env( *, managed_context: ManagedContext, @@ -1709,6 +2164,10 @@ def _managed_root(managed_state_base: Path, backend_name: str) -> Path: return backend_root +def _managed_chat_root(managed_state_base: Path, backend_name: str) -> Path: + return managed_state_base / backend_name / "chat" + + def _ensure_git_checkout( *, repo_url: str, @@ -1783,6 +2242,24 @@ def _run( return result +def _stage_optional_file_copy(*, source: Path, destination: Path) -> bool: + if not source.is_file(): + return False + _remove_existing_path(destination) + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(source, destination) + return True + + +def _stage_optional_tree_copy(*, source: Path, destination: Path) -> bool: + if not source.is_dir(): + return False + _remove_existing_path(destination) + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copytree(source, destination, symlinks=True) + return True + + def _stage_tree(*, source: Path, destination: Path, revision: str) -> None: revision_file = destination / ".gauss-managed-revision" if revision_file.exists() and revision_file.read_text(encoding="utf-8").strip() == revision: diff --git a/gauss_cli/banner.py b/gauss_cli/banner.py index 1bd7e02..2ea4068 100644 --- a/gauss_cli/banner.py +++ b/gauss_cli/banner.py @@ -436,7 +436,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}]`/chat`[/] [dim {dim}]open the configured managed backend chat session[/]") 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[/]") @@ -449,7 +449,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str, 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}]`/chat`[/] [dim {dim}]{long_dash} open the configured managed backend chat session 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[/]") diff --git a/gauss_cli/commands.py b/gauss_cli/commands.py index 593214b..da2650e 100644 --- a/gauss_cli/commands.py +++ b/gauss_cli/commands.py @@ -21,7 +21,7 @@ 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", + "/chat": "Open the configured managed backend chat session 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 b5fd9bf..36feaa1 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 `/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. +When someone asks how to use Open Gauss, give them the lowest-friction path first. If they just want orientation or plain-language help in the current session, point them to `/start`. If they want a managed Claude Code or Codex chat session first, point them to `/chat`. If they want to work on Lean code, point them to `/project` so they create or activate a Gauss project, then tell them to run `/prove`, `/autoprove`, `/formalize`, or `/autoformalize` with a natural-language instruction. Example: `/autoprove The de Bruijn - Erdos theorem`. If they attach to a child session with `/swarm attach`, tell them `Ctrl-]` detaches and returns them to the main Gauss session. 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/main.py b/gauss_cli/main.py index 8ceab34..5fad3c0 100644 --- a/gauss_cli/main.py +++ b/gauss_cli/main.py @@ -469,6 +469,7 @@ def cmd_chat(args): "provider": getattr(args, "provider", None), "toolsets": args.toolsets, "skills": getattr(args, "skills", None), + "startup_input": getattr(args, "startup_input", None), "verbose": args.verbose, "quiet": getattr(args, "quiet", False), "query": args.query, @@ -2440,6 +2441,12 @@ def main(): default=False, help="Include the session ID in the agent's system prompt" ) + parser.add_argument( + "--startup-input", + action="append", + default=None, + help=argparse.SUPPRESS, + ) subparsers = parser.add_subparsers(dest="command", help="Command to run") @@ -2523,6 +2530,12 @@ def main(): default=False, help="Include the session ID in the agent's system prompt" ) + chat_parser.add_argument( + "--startup-input", + action="append", + default=None, + help=argparse.SUPPRESS, + ) chat_parser.set_defaults(func=cmd_chat) # ========================================================================= diff --git a/gauss_cli/skin_engine.py b/gauss_cli/skin_engine.py index 4632fde..b02c713 100644 --- a/gauss_cli/skin_engine.py +++ b/gauss_cli/skin_engine.py @@ -185,7 +185,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: }, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.", + "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", @@ -282,7 +282,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: "spinner": {}, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.", + "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", @@ -314,7 +314,7 @@ def get_branding(self, key: str, fallback: str = "") -> str: "spinner": {}, "branding": { "agent_name": "Gauss", - "welcome": "Welcome to Gauss! Type /start or /chat for orientation, or /help for commands.", + "welcome": "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.", "status_glyph": "@", "goodbye": "Goodbye! @", "response_label": " ∑ Gauss ", diff --git a/scripts/install-internal.sh b/scripts/install-internal.sh index f45dcc9..4eb2ce3 100755 --- a/scripts/install-internal.sh +++ b/scripts/install-internal.sh @@ -893,7 +893,7 @@ This Lean workspace is prewarmed and already registered as the active Gauss proj Quickstart: 1. Run `gauss-open-guide` if you want the plain-language walkthrough first. 2. Run `gauss-open-session` for the batteries-included launcher, or `gauss` directly. -3. Use `/chat` if you want orientation before choosing a Lean workflow. +3. Use `/chat` if you want the configured managed backend chat session before choosing a Lean workflow. 4. Then use `/prove`, `/review`, `/draft`, `/autoprove`, `/formalize`, `/autoformalize`, or `/swarm`. 5. Keep paper notes, extracted statements, and scratch proofs in this project. TXT @@ -1138,7 +1138,7 @@ guide_html = f""" Open repo
-

You do not need to understand MCP, marketplace plugins, or agent orchestration to use Open Gauss. If you just want orientation first, start the CLI and type /start 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>.

+

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

30-second version @@ -1179,7 +1179,7 @@ guide_html = f"""
  1. Run gauss.
  2. If you want a guided first step, type /start.
    3. -
  3. If you want a normal conversation first, type /chat.
    4. +
  4. If you want the configured managed backend chat session 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. After that, use /prove, /review, /draft, or /autoprove.
    8. @@ -1530,9 +1530,12 @@ 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. + OpenRouter affects the in-process main chat only; managed workflow backends stay separate. + /start keeps you in Gauss and enables inline onboarding chat before project selection. + /chat opens the configured managed backend chat session and returns you to Gauss when it exits. + gauss-use-claude-backend and gauss-use-codex-backend switch both /chat and the managed Lean workflows. + When the main provider is staged, this launcher opens Gauss automatically and begins with /start. + If no main provider is staged, this launcher runs gauss setup first and then falls back to a shell. PROMPT_TOOLKIT_NO_CPR=1 is enabled to avoid CPR warnings inside tmux. The local guide is written to __GUIDE_PATH__. @@ -1544,10 +1547,14 @@ fi cd "$WORKSPACE_DIR" if [ -t 0 ] && [ -t 1 ]; then + if [ "$launch_gauss" -eq 1 ]; then + exec gauss --startup-input /start "$@" + fi + GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true exec bash -i fi if [ "$launch_gauss" -eq 1 ]; then - gauss "$@" || true + gauss --startup-input /start "$@" || true exit 0 fi exit 1 @@ -1729,7 +1736,7 @@ print_summary() { 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 " /chat # open the configured managed backend chat session 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" @@ -1758,7 +1765,7 @@ print_summary() { echo " - Verified managed /prove staging in: $MANAGED_SELF_CHECK_STATUS." fi echo " - The local guide is written to $GUIDE_DIR/index.html." - echo " - If Open Gauss feels intimidating, start with /start or /chat and ask a normal question." + echo " - If Open Gauss feels intimidating, start with /start for inline onboarding or /chat for managed backend chat." 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_autoformalize.py b/tests/gauss_cli/test_autoformalize.py index 29d9e62..383f8d4 100644 --- a/tests/gauss_cli/test_autoformalize.py +++ b/tests/gauss_cli/test_autoformalize.py @@ -417,6 +417,192 @@ def test_resolve_backend_name_rejects_unknown_backend(): autoformalize._resolve_backend_name(_config(backend="not-a-backend"), {}) +def test_build_claude_chat_runtime_stages_managed_home_and_plugin_context(monkeypatch, tmp_path: Path): + real_home = tmp_path / "real-home" + real_home.mkdir() + (real_home / ".claude.json").write_text( + json.dumps( + { + "mcpServers": { + "existing": { + "type": "stdio", + "command": "true", + } + } + } + ), + encoding="utf-8", + ) + + def fake_sync_prewarmed_claude_plugin(*, real_home: Path, backend_home: Path) -> Path: + del real_home + plugin_root = backend_home / ".claude" / "plugins" / "cache" / "lean4-skills" / "lean4" / "4.4.0" + (plugin_root / "skills" / "lean4" / "references").mkdir(parents=True) + (plugin_root / "lib" / "scripts").mkdir(parents=True) + return plugin_root + + monkeypatch.setattr(autoformalize, "_require_executable", lambda name, _msg, _env: f"/usr/bin/{name}") + monkeypatch.setattr(autoformalize, "_sync_prewarmed_claude_plugin", fake_sync_prewarmed_claude_plugin) + monkeypatch.setattr(autoformalize, "_prepare_managed_chat_lean_assets", lambda **_kwargs: None) + + runtime = autoformalize._build_claude_chat_runtime( + auth_mode="auto", + user_instruction="Explain what /project init does", + base_environment={ + "PATH": "/usr/bin", + "HOME": str(real_home), + "ANTHROPIC_API_KEY": "sk-ant-api03-test", + }, + include_persisted_env=False, + active_cwd=tmp_path, + managed_state_base=tmp_path / "managed-state", + real_home=real_home, + ) + + managed_root = tmp_path / "managed-state" / "claude-code" / "chat" + managed_home = managed_root / "claude-home" + assert runtime.backend_name == "claude-code" + assert runtime.argv[0] == "/usr/bin/claude" + assert "Explain what /project init does" in runtime.argv[1] + assert "skills and MCP tools" in runtime.argv[1] + assert runtime.child_env["HOME"] == str(managed_home) + assert runtime.child_env["GAUSS_MANAGED_CHAT"] == "1" + assert runtime.child_env["GAUSS_MANAGED_CHAT_BACKEND"] == "claude-code" + assert runtime.child_env["GAUSS_CHAT_CWD"] == str(tmp_path) + assert runtime.child_env["GAUSS_MANAGED_STATE_DIR"] == str(managed_root) + assert runtime.child_env["GAUSS_REAL_HOME"] == str(real_home) + assert runtime.child_env["GAUSS_YOLO_MODE"] == "1" + assert runtime.child_env["CLAUDE_PLUGIN_ROOT"].startswith(str(managed_home)) + payload = json.loads((managed_home / ".claude.json").read_text(encoding="utf-8")) + assert payload["primaryApiKey"] == "sk-ant-api03-test" + assert payload["hasCompletedOnboarding"] is True + assert payload["mcpServers"]["existing"]["command"] == "true" + + +def test_build_codex_chat_runtime_stages_managed_home_and_preserves_codex_context(monkeypatch, tmp_path: Path): + real_home = tmp_path / "real-home" + real_home.mkdir() + source_codex_home = tmp_path / "source-codex-home" + (source_codex_home / "skills" / "github-auth").mkdir(parents=True) + (source_codex_home / "skills" / "github-auth" / "SKILL.md").write_text("# github-auth\n", encoding="utf-8") + (source_codex_home / ".tmp" / "plugins").mkdir(parents=True) + (source_codex_home / ".tmp" / "plugins" / "README.md").write_text("plugins\n", encoding="utf-8") + source_config = 'model = "gpt-5.2-codex"\n\n[mcp_servers.demo]\ncommand = "demo"\n' + (source_codex_home / "config.toml").write_text(source_config, encoding="utf-8") + (real_home / ".agents" / "skills" / "assistant-handoff").mkdir(parents=True) + (real_home / ".agents" / "skills" / "assistant-handoff" / "SKILL.md").write_text( + "# assistant-handoff\n", + encoding="utf-8", + ) + (real_home / ".agents" / "plugins").mkdir(parents=True) + (real_home / ".agents" / "plugins" / "marketplace.json").write_text("{}", encoding="utf-8") + + checkout_root = tmp_path / "assets" / "lean4-skills" + plugin_source = checkout_root / "plugins" / "lean4" + skill_source = plugin_source / "skills" / "lean4" + scripts_root = plugin_source / "lib" / "scripts" + references_root = skill_source / "references" + references_root.mkdir(parents=True) + scripts_root.mkdir(parents=True) + (skill_source / "SKILL.md").write_text("# Lean4\n", encoding="utf-8") + lean_assets = autoformalize.ManagedChatLeanAssets( + assets_root=tmp_path / "assets", + checkout_root=checkout_root, + plugin_source=plugin_source, + skill_source=skill_source, + scripts_root=scripts_root, + references_root=references_root, + skill_revision="lean4-chat-test-revision", + ) + + monkeypatch.setattr(autoformalize, "_require_executable", lambda name, _msg, _env: f"/usr/bin/{name}") + monkeypatch.setattr(autoformalize, "_prepare_managed_chat_lean_assets", lambda **_kwargs: lean_assets) + + runtime = autoformalize._build_codex_chat_runtime( + auth_mode="auto", + user_instruction="Plan the next onboarding step", + base_environment={ + "PATH": "/usr/bin", + "HOME": str(real_home), + "CODEX_HOME": str(source_codex_home), + "OPENAI_API_KEY": "sk-openai-test", + }, + include_persisted_env=False, + active_cwd=tmp_path, + managed_state_base=tmp_path / "managed-state", + real_home=real_home, + ) + + managed_root = tmp_path / "managed-state" / "codex" / "chat" + managed_home = managed_root / "codex-home" + managed_codex_home = managed_home / ".codex" + assert runtime.backend_name == "codex" + assert runtime.argv[0] == "/usr/bin/codex" + assert runtime.argv[1] == "--dangerously-bypass-approvals-and-sandbox" + assert "Plan the next onboarding step" in runtime.argv[2] + assert "return to the main Gauss session" in runtime.argv[2] + assert runtime.child_env["HOME"] == str(managed_home) + assert runtime.child_env["CODEX_HOME"] == str(managed_codex_home) + assert runtime.child_env["GAUSS_MANAGED_CHAT"] == "1" + assert runtime.child_env["GAUSS_MANAGED_CHAT_BACKEND"] == "codex" + assert runtime.child_env["GAUSS_CHAT_CWD"] == str(tmp_path) + assert runtime.child_env["GAUSS_MANAGED_STATE_DIR"] == str(managed_root) + assert runtime.child_env["GAUSS_REAL_HOME"] == str(real_home) + assert runtime.child_env["GAUSS_AUTOFORMALIZE_SKILLS_ROOT"] == str( + managed_home / ".agents" / "skills" / "lean4" + ) + assert runtime.child_env["LEAN4_SCRIPTS"] == str(scripts_root) + assert runtime.child_env["LEAN4_REFS"] == str(managed_home / ".agents" / "skills" / "lean4" / "references") + assert "OPENAI_API_KEY" not in runtime.child_env + + assert (managed_codex_home / "skills" / "github-auth" / "SKILL.md").exists() + assert (managed_codex_home / ".tmp" / "plugins" / "README.md").exists() + assert (managed_home / ".agents" / "skills" / "assistant-handoff" / "SKILL.md").exists() + assert (managed_home / ".agents" / "skills" / "lean4" / "SKILL.md").exists() + assert (managed_codex_home / "skills" / "lean4" / "SKILL.md").exists() + assert (managed_codex_home / "config.toml").read_text(encoding="utf-8") == source_config + auth_payload = json.loads((managed_codex_home / "auth.json").read_text(encoding="utf-8")) + assert auth_payload == { + "auth_mode": "apikey", + "OPENAI_API_KEY": "sk-openai-test", + } + + +def test_resolve_managed_chat_request_builds_launch_plan(monkeypatch, tmp_path: Path): + active_cwd = tmp_path / "workspace" + active_cwd.mkdir() + runtime = autoformalize.ManagedChatRuntime( + argv=["/usr/bin/codex", "--dangerously-bypass-approvals-and-sandbox", "prompt"], + child_env={"PATH": "/usr/bin", "CODEX_HOME": "/tmp/codex-home"}, + backend_name="codex", + ) + captured: dict[str, object] = {} + + def fake_build_handoff_request(**kwargs): + captured.update(kwargs) + return SimpleNamespace(**kwargs) + + monkeypatch.setattr(autoformalize, "_resolve_managed_chat_runtime", lambda **_kwargs: runtime) + monkeypatch.setattr(autoformalize, "build_handoff_request", fake_build_handoff_request) + + plan = autoformalize.resolve_managed_chat_request( + "Explain what /project init does", + _config(mode="helper", backend="codex"), + active_cwd=str(active_cwd), + base_env={"PATH": "/usr/bin"}, + ) + + assert plan.backend_name == "codex" + assert plan.user_instruction == "Explain what /project init does" + assert plan.active_cwd == active_cwd.resolve() + assert captured["argv"] == runtime.argv + assert captured["env"] == runtime.child_env + assert captured["cwd"] == str(active_cwd.resolve()) + assert captured["requested_mode"] == "helper" + assert captured["label"] == "Gauss chat session" + assert captured["source"] == "gauss:chat" + + def test_resolve_autoformalize_request_builds_managed_launch_plan(monkeypatch, tmp_path: Path): shared_bundle = _shared_bundle(tmp_path) managed_context = autoformalize.ManagedContext( diff --git a/tests/gauss_cli/test_banner_responsive.py b/tests/gauss_cli/test_banner_responsive.py index 95de1a4..f5fbba6 100644 --- a/tests/gauss_cli/test_banner_responsive.py +++ b/tests/gauss_cli/test_banner_responsive.py @@ -208,7 +208,7 @@ def test_build_welcome_banner_mentions_swarm_in_primary_workflow(monkeypatch): 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 "open the configured managed backend chat session 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_chat_skills_flag.py b/tests/gauss_cli/test_chat_skills_flag.py index 943644a..213ccd3 100644 --- a/tests/gauss_cli/test_chat_skills_flag.py +++ b/tests/gauss_cli/test_chat_skills_flag.py @@ -1,4 +1,5 @@ import sys +from types import SimpleNamespace def test_top_level_skills_flag_defaults_to_chat(monkeypatch): @@ -75,3 +76,83 @@ def fake_cmd_chat(args): "skills": ["gauss-agent-dev"], "command": "chat", } + + +def test_top_level_startup_input_defaults_to_chat(monkeypatch): + import gauss_cli.main as main_mod + + captured = {} + + def fake_cmd_chat(args): + captured["startup_input"] = args.startup_input + captured["command"] = args.command + + monkeypatch.setattr(main_mod, "cmd_chat", fake_cmd_chat) + monkeypatch.setattr( + sys, + "argv", + ["gauss", "--startup-input", "/chat"], + ) + + main_mod.main() + + assert captured == { + "startup_input": ["/chat"], + "command": None, + } + + +def test_chat_subcommand_accepts_startup_input_flag(monkeypatch): + import gauss_cli.main as main_mod + + captured = {} + + def fake_cmd_chat(args): + captured["startup_input"] = args.startup_input + captured["query"] = args.query + + monkeypatch.setattr(main_mod, "cmd_chat", fake_cmd_chat) + monkeypatch.setattr( + sys, + "argv", + ["gauss", "chat", "--startup-input", "/start", "-q", "hello"], + ) + + main_mod.main() + + assert captured == { + "startup_input": ["/start"], + "query": "hello", + } + + +def test_cmd_chat_forwards_startup_input_to_cli_main(monkeypatch): + import gauss_cli.main as main_mod + + captured = {} + + def fake_cli_main(**kwargs): + captured.update(kwargs) + + monkeypatch.setattr(main_mod, "_has_any_provider_configured", lambda: True) + monkeypatch.setattr("cli.main", fake_cli_main) + + args = SimpleNamespace( + model=None, + provider=None, + toolsets=None, + skills=None, + startup_input=["/chat"], + verbose=False, + quiet=False, + query=None, + resume=None, + worktree=False, + checkpoints=False, + pass_session_id=False, + yolo=False, + ) + + main_mod.cmd_chat(args) + + assert captured["startup_input"] == ["/chat"] diff --git a/tests/gauss_cli/test_commands.py b/tests/gauss_cli/test_commands.py index 9f94841..25191d4 100644 --- a/tests/gauss_cli/test_commands.py +++ b/tests/gauss_cli/test_commands.py @@ -64,7 +64,7 @@ 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["/chat"] == "Open the configured managed backend chat session 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 f2b9206..ddb1030 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 @@ -176,6 +176,7 @@ printf '%s\n' "$SUMMARY_OUTPUT" [[ "$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" +[[ "$SUMMARY_OUTPUT" == *"begins with /start"* ]] || die "expected launcher summary to mention automatic /start" echo "==> Verifying no-provider launcher fallback state" cp "$GAUSS_HOME/.env" "$GAUSS_HOME/.env.backup" @@ -202,11 +203,11 @@ 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 -grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected interactive shell fallback in launcher" +[[ "$NO_PROVIDER_SUMMARY" == *"/chat opens the configured managed backend chat session"* ]] || die "expected provider notes to mention managed /chat" +[[ "$NO_PROVIDER_SUMMARY" == *"runs gauss setup first"* ]] || die "expected missing-provider summary to mention setup fallback" +grep -F "GAUSS_FORCE_FIRST_TIME_SETUP=1 gauss setup || true" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to restore first-run setup fallback when no provider is staged" +grep -F "gauss --startup-input /start" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected launcher to auto-start gauss with /start" +grep -F "exec bash -i" "$HOME/.local/bin/gauss-launch-session" >/dev/null || die "expected interactive shell fallback when no provider is staged" mv "$GAUSS_HOME/.env.backup" "$GAUSS_HOME/.env" echo "==> Verifying Lean bootstrap failures surface useful diagnostics" diff --git a/tests/test_cli_handoff_command.py b/tests/test_cli_handoff_command.py index 224afcb..3fe65d0 100644 --- a/tests/test_cli_handoff_command.py +++ b/tests/test_cli_handoff_command.py @@ -351,31 +351,87 @@ def test_project_lock_blocks_workflow_commands_before_project_selection(): assert "/chat" in rendered -def test_chat_command_enables_chat_mode_before_project_selection(): +def test_chat_command_dispatches_to_managed_interactive_runner(): cli_obj = _make_cli() cli_obj._app = object() - cli_obj._project_state = MagicMock( - return_value=(None, "ambient", "No active Gauss project found.") + task = SimpleNamespace(task_id="chat-001", status="running", pty_master_fd=99) + swarm = MagicMock() + swarm.spawn_interactive.return_value = task + plan = SimpleNamespace( + backend_name="codex", + handoff_request=SimpleNamespace( + argv=["/usr/bin/codex", "--dangerously-bypass-approvals-and-sandbox", "prompt"], + cwd="/tmp", + env={"PATH": "/usr/bin", "CODEX_HOME": "/tmp/codex-home"}, + ), ) - assert cli_obj._plain_input_requires_project() is True - assert cli_obj.process_command("/chat") is True + with patch.object(cli_mod, "resolve_managed_chat_request", return_value=plan), \ + patch.object(cli_mod, "SwarmManager", return_value=swarm), \ + patch.object(cli_obj, "_attach_to_swarm_task") as mock_attach: + assert cli_obj.process_command("/chat") is True - assert cli_obj._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 + swarm.spawn_interactive.assert_called_once() + kwargs = swarm.spawn_interactive.call_args.kwargs + assert kwargs["theorem"] == "managed chat" + assert kwargs["description"] == "managed chat" + assert kwargs["argv"] == ["/usr/bin/codex", "--dangerously-bypass-approvals-and-sandbox", "prompt"] + assert kwargs["cwd"] == "/tmp" + assert kwargs["workflow_kind"] == "chat" + assert kwargs["workflow_command"] == "/chat" + assert kwargs["backend_name"] == "codex" + assert kwargs["env"]["CODEX_HOME"] == "/tmp/codex-home" + mock_attach.assert_called_once_with("chat-001") + + +def test_chat_command_with_payload_forwards_startup_message(): + cli_obj = _make_cli() + cli_obj._app = object() + task = SimpleNamespace(task_id="chat-002", status="running", pty_master_fd=99) + swarm = MagicMock() + swarm.spawn_interactive.return_value = task + plan = SimpleNamespace( + backend_name="claude-code", + handoff_request=SimpleNamespace( + argv=["/usr/bin/claude", "managed prompt with payload"], + cwd="/tmp", + env={"PATH": "/usr/bin", "HOME": "/tmp/home"}, + ), + ) + + with patch.object(cli_mod, "resolve_managed_chat_request", return_value=plan) as mock_resolve, \ + patch.object(cli_mod, "SwarmManager", return_value=swarm), \ + patch.object(cli_obj, "_attach_to_swarm_task") as mock_attach: + assert cli_obj.process_command("/chat Explain what /project init does") is True + mock_resolve.assert_called_once_with( + "Explain what /project init does", + cli_obj.config, + active_cwd="/tmp", + ) + kwargs = swarm.spawn_interactive.call_args.kwargs + assert kwargs["theorem"] == "Explain what /project init does" + assert kwargs["description"] == "Explain what /project init does" + assert kwargs["argv"] == ["/usr/bin/claude", "managed prompt with payload"] + assert kwargs["backend_name"] == "claude-code" + mock_attach.assert_called_once_with("chat-002") -def test_chat_command_with_payload_queues_plain_message(): + +def test_chat_status_explains_new_managed_session_semantics(): cli_obj = _make_cli() cli_obj._app = object() - cli_obj._pending_input = MagicMock() + swarm = MagicMock() - assert cli_obj.process_command("/chat Explain what /project init does") is True + with patch.object(cli_mod, "SwarmManager", return_value=swarm), \ + patch.object(cli_obj, "_active_managed_backend_name", return_value="codex"): + assert cli_obj.process_command("/chat status") is True - assert cli_obj._chat_mode_enabled is True - cli_obj._pending_input.put.assert_called_once_with("Explain what /project init does") + swarm.spawn_interactive.assert_not_called() + rendered = "\n".join(call.args[0] for call in cli_obj.console.print.call_args_list) + assert "managed backend chat session" in rendered + assert "codex" in rendered + assert "/autoformalize-backend" in rendered + assert "/start" in rendered def test_start_command_enables_chat_mode_and_shows_first_steps(): diff --git a/tests/test_run_agent.py b/tests/test_run_agent.py index c23ebf5..058a6c4 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 "point them to /start or /chat" in prompt + assert "point them to /start if they want inline orientation or plain-language help" in prompt + assert "point them to /chat if they want a managed Claude Code or Codex chat session" in prompt assert "point them to /project" in prompt assert "/autoprove The de Bruijn - Erdos theorem" in prompt assert "Ctrl-] detaches and returns them to the main Gauss session" in prompt diff --git a/website/docs/getting-started/start-here.md b/website/docs/getting-started/start-here.md index 5c10ce7..5de0d4d 100644 --- a/website/docs/getting-started/start-here.md +++ b/website/docs/getting-started/start-here.md @@ -10,7 +10,7 @@ OpenGauss is for Lean work, but you do **not** need to understand MCP, plugin in If you only want a guided first step, use `/start`. -If you only want to ask questions first, use `/chat`. +If you want a managed Claude Code or Codex chat session first, use `/chat`. If you want OpenGauss to work inside a Lean project, use `/project`. @@ -24,7 +24,7 @@ If you want OpenGauss to work inside a Lean project, use `/project`. ## 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. +- `/chat` opens the configured managed backend chat session before you choose a project. - `/project init` tells OpenGauss that the current Lean repository is your working project. - `/project use ` points OpenGauss at an already-initialized project somewhere else on disk. - `/project create --template-source ` creates a new Lean project and registers it. @@ -38,7 +38,7 @@ If you want OpenGauss to work inside a Lean project, use `/project`. 2. If Morph shows a **Claim**, **Save**, or similar action for the session, use it early. The exact button text can change, but temporary sessions are easier to lose than claimed ones. 3. Run `gauss-open-guide` if the browser guide is not already visible. -4. If you want orientation first, type `/start` or `/chat`. +4. If you want orientation first, type `/start`, or use `/chat` for the configured managed backend chat session. 5. If you want to work on a Lean project, clone or open it and then run `/project init` or `/project use`. ### Making It Persistent @@ -80,7 +80,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 `/chat` if you want the configured managed backend chat session first - use `/project init` if you are already inside a Lean repository - use `/project create --template-source ` if you need a new project diff --git a/website/docs/reference/slash-commands.md b/website/docs/reference/slash-commands.md index e13e76b..e5814c7 100644 --- a/website/docs/reference/slash-commands.md +++ b/website/docs/reference/slash-commands.md @@ -13,7 +13,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. | +| `/chat [question]` | Open the configured managed backend chat session 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 cc20736..6220ed9 100644 --- a/website/docs/user-guide/cli.md +++ b/website/docs/user-guide/cli.md @@ -18,7 +18,7 @@ gauss --resume gauss chat -q "hello" ``` -Inside the interactive CLI, `/start` and `/chat` are the simplest on-ramps when you want orientation 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. `/start` keeps you in Gauss; `/chat` yields the terminal to the configured managed backend and returns you to Gauss when it exits. ## Primary Workflow