Skip to content

Commit b5b5495

Browse files
Restore top-level Gauss entry and repurpose chat
1 parent 054c88e commit b5b5495

13 files changed

Lines changed: 213 additions & 154 deletions

File tree

agent/prompt_builder.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,9 +67,9 @@ def _scan_context_content(content: str, filename: str) -> str:
6767
"a general self-summary unless the user explicitly asks. When asked who you "
6868
"are, answer briefly and return to the work. "
6969
"When the user is trying to use Open Gauss itself or seems unsure how to "
70-
"start, give them the lowest-friction path first: point them to /start if "
71-
"they want inline orientation or plain-language help, point them to /chat "
72-
"if they want a managed Claude Code or Codex chat session, and point them to /project "
70+
"start, give them the lowest-friction path first: point them to /chat if "
71+
"they want inline orientation or plain-language help, point them to /managed-chat "
72+
"if they want a managed Claude Code or Codex child session, and point them to /project "
7373
"when they are ready to create or activate a Gauss project. After that, "
7474
"tell them to run /prove, /autoprove, /formalize, or /autoformalize "
7575
"followed by a natural-language instruction, for example /autoprove The "

cli.py

Lines changed: 85 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -2423,7 +2423,7 @@ def show_help(self):
24232423
_cprint(f"\n {_DIM}Active project: {project_summary}{_RST}")
24242424
else:
24252425
_cprint(
2426-
f"\n {_DIM}No active project — use /start for inline onboarding, /chat for managed backend chat, or /project init, "
2426+
f"\n {_DIM}No active project — use /chat for inline onboarding, /managed-chat for a managed backend child session, or /project init, "
24272427
f"/project convert, /project create <path>, or /project use <path>.{_RST}"
24282428
)
24292429

@@ -2440,7 +2440,7 @@ def show_help(self):
24402440
)
24412441

24422442
_cprint(
2443-
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, "
2443+
f"\n {_DIM}Tip: Start with /chat for inline onboarding if you want orientation first. Use /managed-chat if you want the configured managed backend child session. Use /project when you're ready to work in a Lean repo, "
24442444
f"then launch /prove, /review, /checkpoint, /refactor, /golf, /draft, /autoprove, /formalize, or /autoformalize.{_RST}"
24452445
)
24462446
_cprint(f" {_DIM}Multi-line: Alt+Enter for a new line{_RST}")
@@ -3375,8 +3375,9 @@ def _project_lock_allows_command(self, command: str) -> bool:
33753375
"""Return whether *command* remains available before project selection."""
33763376
cmd_lower = command.lower().strip()
33773377
allowed_prefixes = (
3378-
"/start",
33793378
"/chat",
3379+
"/managed-chat",
3380+
"/start",
33803381
"/project",
33813382
"/help",
33823383
"/quit",
@@ -3411,8 +3412,8 @@ def _print_project_lock_notice(self, *, command_label: str) -> None:
34113412
f"{prefix} Use /project init, /project convert, /project create <path>, or /project use <path> first.",
34123413
)
34133414
self._print_surface_notice(
3414-
"[dim]If you only want orientation first, run `/start` for inline onboarding chat or `/chat` for the configured managed backend chat session.[/]",
3415-
"If you only want orientation first, run /start for inline onboarding chat or /chat for the configured managed backend chat session.",
3415+
"[dim]If you only want orientation first, run `/chat` for inline onboarding chat or `/managed-chat` for the configured managed backend child session.[/]",
3416+
"If you only want orientation first, run /chat for inline onboarding chat or /managed-chat for the configured managed backend child session.",
34163417
)
34173418
self._print_surface_notice(
34183419
f"[dim]{detail}[/]",
@@ -3488,7 +3489,7 @@ def _active_managed_backend_name(self) -> str:
34883489
except AutoformalizeConfigError:
34893490
return str(active_backend_raw or available[0])
34903491

3491-
def _spawn_managed_chat_session(self, payload: str):
3492+
def _spawn_managed_chat_session(self, payload: str, *, workflow_command: str = "/managed-chat"):
34923493
"""Launch a managed provider chat child session and return the task metadata."""
34933494
plan = resolve_managed_chat_request(
34943495
payload,
@@ -3505,33 +3506,86 @@ def _spawn_managed_chat_session(self, payload: str):
35053506
cwd=plan.handoff_request.cwd,
35063507
env=plan.handoff_request.env,
35073508
workflow_kind="chat",
3508-
workflow_command="/chat",
3509+
workflow_command=workflow_command,
35093510
backend_name=plan.backend_name,
35103511
)
35113512
return task, description, plan.backend_name
35123513

35133514
def _handle_chat_command(self, cmd: str):
3514-
"""Handle `/chat` by opening the configured managed backend chat session."""
3515+
"""Handle `/chat` by enabling inline top-level chat mode."""
3516+
parts = cmd.strip().split(maxsplit=1)
3517+
payload = parts[1].strip() if len(parts) > 1 else ""
3518+
lowered = payload.lower()
3519+
3520+
if lowered == "status":
3521+
state_label = "on" if self._chat_mode_active() else "off"
3522+
self._print_surface_notice(
3523+
f"[dim]`/chat` is {state_label}. When it is on, plain text goes to the main interactive provider in the current Gauss session. "
3524+
"Use `/chat off` to return to top-level command mode, or `/managed-chat` if you want the configured managed backend child session.[/]",
3525+
f"`/chat` is {state_label}. When it is on, plain text goes to the main interactive provider in the current Gauss session. "
3526+
"Use /chat off to return to top-level command mode, or /managed-chat if you want the configured managed backend child session.",
3527+
)
3528+
return
3529+
3530+
if lowered in {"off", "disable", "stop"}:
3531+
self._chat_mode_enabled = False
3532+
self._print_surface_notice(
3533+
"[dim]`/chat` is off. Plain text stays at the top-level Open Gauss prompt until you run `/chat` again.[/]",
3534+
"`/chat` is off. Plain text stays at the top-level Open Gauss prompt until you run /chat again.",
3535+
)
3536+
return
3537+
3538+
if lowered in {"on", "enable", "start"}:
3539+
payload = ""
3540+
3541+
self._chat_mode_enabled = True
3542+
self._print_surface_notice(
3543+
"[bold green]`/chat` is on.[/] "
3544+
"[dim]Plain text now goes to the main interactive provider even without an active Gauss project.[/]",
3545+
"`/chat` is on. Plain text now goes to the main interactive provider even without an active Gauss project.",
3546+
)
3547+
self._print_surface_notice(
3548+
"[dim]Next: use `/project use <path>` for an existing Lean repo, `/project init` in the current repo, "
3549+
"`/project create <path> --template-source <template-or-git-url>` for a new one, or `/managed-chat` if you want the configured managed backend child session instead.[/]",
3550+
"Next: use /project use <path> for an existing Lean repo, /project init in the current repo, /project create <path> --template-source <template-or-git-url> for a new one, or /managed-chat if you want the configured managed backend child session instead.",
3551+
)
3552+
self._print_surface_notice(
3553+
"[dim]When the project is ready, run `/prove`, `/review`, `/draft`, `/autoprove`, or `/swarm`.[/]",
3554+
"When the project is ready, run /prove, /review, /draft, /autoprove, or /swarm.",
3555+
)
3556+
if payload:
3557+
self._print_surface_notice(
3558+
"[dim]`/chat` is sending your message to the main interactive provider.[/]",
3559+
"`/chat` is sending your message to the main interactive provider.",
3560+
)
3561+
if hasattr(self, "_pending_input") and hasattr(self._pending_input, "put"):
3562+
self._pending_input.put(payload)
3563+
else:
3564+
self._print_surface_notice(
3565+
"[bold yellow]Chat queue is not available in this mode.[/]",
3566+
"Chat queue is not available in this mode.",
3567+
)
3568+
3569+
def _handle_managed_chat_command(self, cmd: str):
3570+
"""Handle `/managed-chat` by opening the configured managed backend child session."""
35153571
parts = cmd.strip().split(maxsplit=1)
35163572
payload = parts[1].strip() if len(parts) > 1 else ""
35173573
lowered = payload.lower()
35183574

35193575
if lowered == "status":
35203576
active_backend = self._active_managed_backend_name()
35213577
self._print_surface_notice(
3522-
"[dim]`/chat` opens the configured managed backend chat session "
3523-
f"(`{active_backend}`). Use `/autoformalize-backend` to switch backends, or `/start` "
3524-
"for inline onboarding chat in the current Gauss session.[/]",
3525-
f"`/chat` opens the configured managed backend chat session ({active_backend}). "
3526-
"Use /autoformalize-backend to switch backends, or /start for inline onboarding chat in the current Gauss session.",
3578+
"[dim]`/managed-chat` opens the configured managed backend child session "
3579+
f"(`{active_backend}`). Use `/autoformalize-backend` to switch backends, or `/chat` for inline onboarding in the current Gauss session.[/]",
3580+
f"`/managed-chat` opens the configured managed backend child session ({active_backend}). "
3581+
"Use /autoformalize-backend to switch backends, or /chat for inline onboarding in the current Gauss session.",
35273582
)
35283583
return
35293584

35303585
if lowered in {"off", "disable", "stop"}:
35313586
self._print_surface_notice(
3532-
"[dim]Inline `/chat` mode has been removed. "
3533-
"Use `/start` for inline onboarding chat, or run `/chat` to open the managed backend chat session.[/]",
3534-
"Inline /chat mode has been removed. Use /start for inline onboarding chat, or run /chat to open the managed backend chat session.",
3587+
"[dim]`/managed-chat` is not a persistent mode. Run `/chat` if you want inline onboarding in the current Gauss session.[/]",
3588+
"`/managed-chat` is not a persistent mode. Run /chat if you want inline onboarding in the current Gauss session.",
35353589
)
35363590
return
35373591

@@ -3541,9 +3595,12 @@ def _handle_chat_command(self, cmd: str):
35413595
task = None
35423596
description = payload.strip() or "managed chat"
35433597
backend_name = self._active_managed_backend_name()
3544-
with self._busy_command(self._slow_command_status("/chat")):
3598+
with self._busy_command(self._slow_command_status("/managed-chat")):
35453599
try:
3546-
task, description, backend_name = self._spawn_managed_chat_session(payload)
3600+
task, description, backend_name = self._spawn_managed_chat_session(
3601+
payload,
3602+
workflow_command="/managed-chat",
3603+
)
35473604
except (AutoformalizeError, HandoffError) as exc:
35483605
print(f"(>_<) {exc}")
35493606
return
@@ -3560,37 +3617,10 @@ def _handle_chat_command(self, cmd: str):
35603617
)
35613618

35623619
def _handle_start_command(self, cmd: str):
3563-
"""Handle `/start` with a short first-step guide and chat-mode enablement."""
3564-
parts = cmd.strip().split(maxsplit=1)
3565-
payload = parts[1].strip() if len(parts) > 1 else ""
3566-
3567-
self._chat_mode_enabled = True
3568-
self._print_surface_notice(
3569-
"[bold green]`/start` is on.[/] "
3570-
"[dim]Plain text now goes to the main interactive provider even without an active Gauss project.[/]",
3571-
"`/start` is on. Plain text now goes to the main interactive provider even without an active Gauss project.",
3572-
)
3573-
self._print_surface_notice(
3574-
"[dim]Next: use `/chat` if you want the configured managed backend chat session, `/project use <path>` for an existing Lean repo, "
3575-
"`/project init` in the current repo, or `/project create <path> --template-source <template-or-git-url>` for a new one.[/]",
3576-
"Next: use /chat if you want the configured managed backend chat session, /project use <path> for an existing Lean repo, /project init in the current repo, or /project create <path> --template-source <template-or-git-url> for a new one.",
3577-
)
3578-
self._print_surface_notice(
3579-
"[dim]When the project is ready, run `/prove`, `/review`, `/draft`, `/autoprove`, or `/swarm`.[/]",
3580-
"When the project is ready, run /prove, /review, /draft, /autoprove, or /swarm.",
3581-
)
3582-
if payload:
3583-
self._print_surface_notice(
3584-
"[dim]`/start` is sending your message to the main interactive provider.[/]",
3585-
"`/start` is sending your message to the main interactive provider.",
3586-
)
3587-
if hasattr(self, "_pending_input") and hasattr(self._pending_input, "put"):
3588-
self._pending_input.put(payload)
3589-
else:
3590-
self._print_surface_notice(
3591-
"[bold yellow]Chat queue is not available in this mode.[/]",
3592-
"Chat queue is not available in this mode.",
3593-
)
3620+
"""Compatibility alias for `/chat`."""
3621+
suffix = cmd.strip()[len("/start"):]
3622+
forwarded = f"/chat{suffix}" if suffix else "/chat"
3623+
self._handle_chat_command(forwarded)
35943624

35953625
def _setup_swarm_completion_callback(self):
35963626
"""Wire up a one-time callback so finished swarm tasks notify the TUI."""
@@ -4092,10 +4122,12 @@ def process_command(self, command: str) -> bool:
40924122

40934123
if cmd_lower in ("/quit", "/exit", "/q"):
40944124
return False
4095-
elif cmd_lower == "/start" or cmd_lower.startswith("/start "):
4096-
self._handle_start_command(cmd_original)
40974125
elif cmd_lower == "/chat" or cmd_lower.startswith("/chat "):
40984126
self._handle_chat_command(cmd_original)
4127+
elif cmd_lower == "/managed-chat" or cmd_lower.startswith("/managed-chat "):
4128+
self._handle_managed_chat_command(cmd_original)
4129+
elif cmd_lower == "/start" or cmd_lower.startswith("/start "):
4130+
self._handle_start_command(cmd_original)
40994131
elif cmd_lower == "/help":
41004132
self.show_help()
41014133
elif cmd_lower == "/project" or cmd_lower.startswith("/project "):
@@ -6401,10 +6433,10 @@ def run(self):
64016433
try:
64026434
from gauss_cli.skin_engine import get_active_skin
64036435
_welcome_skin = get_active_skin()
6404-
_welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands.")
6436+
_welcome_text = _welcome_skin.get_branding("welcome", "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands.")
64056437
_welcome_color = _welcome_skin.get_color("banner_text", "#FFF8DC")
64066438
except Exception:
6407-
_welcome_text = "Welcome to Gauss! Type /start for inline onboarding, /chat for managed backend chat, or /help for commands."
6439+
_welcome_text = "Welcome to Gauss! Type /chat for inline onboarding, /project for project setup, or /help for commands."
64086440
_welcome_color = "#FFF8DC"
64096441
self.console.print(f"[{_welcome_color}]{_welcome_text}[/]")
64106442
self.console.print()

gauss_cli/banner.py

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -438,8 +438,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
438438

439439
if simplified:
440440
right_lines.append(f"[bold {accent}]Start Here[/]")
441-
right_lines.append(f"[{text}]`/start`[/] [dim {dim}]turn on onboarding mode and see the first steps[/]")
442-
right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]open the configured managed backend chat session[/]")
441+
right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]turn on onboarding mode and see the first steps[/]")
443442
right_lines.append(f"[{text}]`/project`[/] [dim {dim}]select or create a Gauss project[/]")
444443
right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]guided Lean workflow[/]")
445444
right_lines.append(f"[{text}]`/review`[/] [dim {dim}]review, checkpoint, refactor, golf[/]")
@@ -451,8 +450,7 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
451450
right_lines.append(f"[{text}]`/help`[/] [dim {dim}]commands and diagnostics[/]")
452451
else:
453452
right_lines.append(f"[bold {accent}]Start Here[/]")
454-
right_lines.append(f"[{text}]`/start`[/] [dim {dim}]{long_dash} turn on onboarding mode and show the first steps[/]")
455-
right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} open the configured managed backend chat session before choosing a project[/]")
453+
right_lines.append(f"[{text}]`/chat`[/] [dim {dim}]{long_dash} turn on onboarding mode and show the first steps[/]")
456454
right_lines.append(f"[{text}]`/project`[/] [dim {dim}]{long_dash} create, convert, inspect, or switch the active project[/]")
457455
right_lines.append(f"[{text}]`/prove`[/] [dim {dim}]{long_dash} spawn a guided managed proving agent[/]")
458456
right_lines.append(f"[{text}]`/review`[/] [dim {dim}]{long_dash} review, checkpoint, refactor, or golf Lean proofs[/]")
@@ -474,7 +472,6 @@ def build_welcome_banner(console: Console, model: str, cwd: str,
474472

475473
right_lines.append("")
476474
summary_parts = [
477-
"/start",
478475
"/chat",
479476
"/project",
480477
"/prove",

gauss_cli/commands.py

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,7 @@
2020
# Commands organized by category for better help display
2121
COMMANDS_BY_CATEGORY = {
2222
"Start Here": {
23-
"/start": "Show the first-step guide and enable plain-language chat mode",
24-
"/chat": "Open the configured managed backend chat session before choosing a Gauss project",
23+
"/chat": "Show the first-step guide and enable plain-language chat mode",
2524
"/project": "Create, convert, inspect, or switch the active Gauss project",
2625
},
2726
"Workflow": {
@@ -38,6 +37,7 @@
3837
"/swarm": "Show workflow agents · /swarm attach <id> · /swarm cancel <id>",
3938
},
4039
"Session": {
40+
"/managed-chat": "Open the configured managed backend child session and return to Gauss when it exits",
4141
"/new": "Start a new session (fresh session ID + history)",
4242
"/reset": "Start a new session (alias for /new)",
4343
"/clear": "Clear screen and start a new session",
@@ -75,8 +75,8 @@
7575

7676
_FRIENDLY_ENTRY_ALIASES = {
7777
"chat": "/chat",
78-
"start": "/start",
79-
"begin": "/start",
78+
"start": "/chat",
79+
"begin": "/chat",
8080
"project": "/project",
8181
"help": "/help",
8282
}
@@ -93,7 +93,7 @@
9393

9494
_FRIENDLY_FUZZY_TARGETS = {
9595
"chat": "/chat",
96-
"start": "/start",
96+
"start": "/chat",
9797
"project": "/project",
9898
"help": "/help",
9999
}
@@ -113,7 +113,7 @@ def rewrite_friendly_entry_command(command: str) -> str | None:
113113

114114
lowered = " ".join(text.lower().split())
115115
if lowered in _FRIENDLY_ENTRY_PHRASES:
116-
return "/start"
116+
return "/chat"
117117

118118
parts = text.split(maxsplit=1)
119119
token = _normalize_entry_token(parts[0])
@@ -141,6 +141,8 @@ def rewrite_friendly_slash_command(command: str) -> str | None:
141141
parts = text.split(maxsplit=1)
142142
token = parts[0].strip().lower()
143143
remainder = parts[1].strip() if len(parts) > 1 else ""
144+
if token == "/start":
145+
return None
144146
if token in COMMANDS:
145147
return None
146148

0 commit comments

Comments
 (0)