From 99ab1a6c455ceec008487b827b830f287f67ea7c Mon Sep 17 00:00:00 2001 From: markm39 Date: Fri, 27 Mar 2026 22:39:20 -0500 Subject: [PATCH] refactor(cli): remove 9 unused slash commands, fix help text bugs Remove redundant and trivial commands that overlap with /proof or the TUI: - /clear (duplicate of /new), /sessions (duplicate of /resume) - /status, /branches, /agents, /tasks (trivial inspection, covered by /proof) - /questions, /instructions, /login (low-value or non-functional) Bug fixes: - Help text said "q quits" but quit is Ctrl+C -- fixed - /lean command existed but was missing from tab completion and help -- added - /autonomous full subcommand missing from tab completion -- added --- README.md | 14 +--- crates/openproof-cli/src/slash_commands.rs | 81 ++-------------------- crates/openproof-core/src/commands.rs | 11 +-- 3 files changed, 9 insertions(+), 97 deletions(-) diff --git a/README.md b/README.md index 65e3ab3..ec4a1a8 100644 --- a/README.md +++ b/README.md @@ -113,10 +113,7 @@ Inside the interactive TUI, type `/` followed by a command. | Command | Description | |---------|-------------| | `/new ` | Start a new session | -| `/clear [title]` | Create a new session (alias) | -| `/resume <session-id>` | Switch to a different session | -| `/sessions` | List all sessions | -| `/status` | Current session status | +| `/resume <session-id>` | Switch to a different session (no args opens picker) | ### Proving @@ -126,8 +123,9 @@ Inside the interactive TUI, type `/` followed by a command. | `/lemma <label> :: <statement>` | Create a lemma node | | `/verify` | Trigger Lean verification manually | | `/proof` | Show proof state and node tree | +| `/lean` | Inspect Lean state (scratch file, verification, history) | | `/focus <id\|clear>` | Focus on a specific branch or node | -| `/autonomous start\|stop\|step\|status` | Control autonomous proving loop | +| `/autonomous start\|full\|stop\|step\|status` | Control autonomous proving loop | | `/agent spawn <role> <task>` | Spawn a specific agent (planner, prover, repairer, retriever, critic) | ### Corpus and sync @@ -146,12 +144,7 @@ Inside the interactive TUI, type `/` followed by a command. | Command | Description | |---------|-------------| | `/nodes` | List all proof nodes | -| `/branches` | Show branch status | -| `/agents` | Show agent status | -| `/tasks` | Show task queue | -| `/questions` | Show pending clarification questions | | `/answer <option\|text>` | Answer a pending question | -| `/instructions` | Display AGENTS.md instructions | | `/memory` | Show workspace memory | | `/remember <text>` | Save to workspace memory | | `/remember global <text>` | Save to global memory | @@ -163,7 +156,6 @@ Inside the interactive TUI, type `/` followed by a command. | `/paper` | Display compiled paper | | `/export paper\|tex\|lean\|all` | Export proof in various formats | | `/dashboard` | Open web dashboard | -| `/login` | Sync auth credentials | ## Search strategies diff --git a/crates/openproof-cli/src/slash_commands.rs b/crates/openproof-cli/src/slash_commands.rs index a43c605..487172d 100644 --- a/crates/openproof-cli/src/slash_commands.rs +++ b/crates/openproof-cli/src/slash_commands.rs @@ -1,4 +1,4 @@ -//! Slash-command dispatch (`/help`, `/status`, `/autonomous`, etc.). +//! Slash-command dispatch (`/help`, `/new`, `/autonomous`, etc.). //! //! All `/command` strings entered by the user flow through //! `apply_local_command`. Each command arm is self-contained: it reads from @@ -43,21 +43,15 @@ pub fn apply_local_command( "Help", [ "/help", - "/status", "/new <title>", - "/clear [title]", "/resume <session-id>", "/nodes", - "/branches", - "/agents", - "/tasks", "/focus <branch-id|node-id|clear>", "/agent spawn <role> <task>", "/proof", + "/lean", "/paper", - "/questions", "/answer <option-id|text>", - "/instructions", "/memory", "/remember <text>", "/remember global <text>", @@ -66,30 +60,16 @@ pub fn apply_local_command( "/corpus status|search <query>|ingest|recluster", "/sync status|enable|disable|drain", "/export paper|tex|lean|all", - "/autonomous status|start|stop|step", + "/autonomous status|start|full|stop|step", "/theorem <label> :: <statement>", "/lemma <label> :: <statement>", "/verify", - "/login", "/dashboard", - "/sessions", - "Tab focuses panes. Enter sends. q quits.", + "Tab focuses panes. Enter sends. Ctrl+C quits.", ] .join("\n"), ); } - "/status" => { - emit_local_notice(tx, state, store, "Status", state.status_report()); - } - "/branches" => { - emit_local_notice(tx, state, store, "Branches", state.branches_report()); - } - "/agents" => { - emit_local_notice(tx, state, store, "Agents", state.agents_report()); - } - "/tasks" => { - emit_local_notice(tx, state, store, "Tasks", state.tasks_report()); - } "/new" => { let write = state.create_session(if arg_text.is_empty() { None @@ -111,27 +91,6 @@ pub fn apply_local_command( ), ); } - "/clear" => { - let write = state.create_session(if arg_text.is_empty() { - None - } else { - Some(arg_text) - }); - persist_write(tx.clone(), store.clone(), write); - emit_local_notice( - tx, - state, - store, - "Session", - format!( - "Cleared into new session: {}.", - state - .current_session() - .map(|session| session.title.clone()) - .unwrap_or_else(|| "OpenProof Rust Session".to_string()) - ), - ); - } "/resume" => { if arg_text.is_empty() { state.overlay = Some(openproof_core::Overlay::SessionPicker { @@ -322,24 +281,6 @@ pub fn apply_local_command( emit_local_notice(tx, state, store, "Paper", "No active session.".to_string()); } } - "/questions" => { - emit_local_notice( - tx, - state, - store, - "Questions", - state.pending_question_report(), - ); - } - "/instructions" => { - let context = crate::system_prompt::load_prompt_context(); - let content = if context.instructions.trim().is_empty() { - "No AGENTS.md instructions loaded.".to_string() - } else { - context.instructions - }; - emit_local_notice(tx, state, store, "Instructions", content); - } "/memory" => { let context = crate::system_prompt::load_prompt_context(); let content = if context.memory.trim().is_empty() { @@ -420,15 +361,6 @@ pub fn apply_local_command( "/theorem" => apply_statement_command(tx, state, store, ProofNodeKind::Theorem, arg_text), "/lemma" => apply_statement_command(tx, state, store, ProofNodeKind::Lemma, arg_text), "/verify" => start_verify_active_node(tx, state, store), - "/login" => { - emit_local_notice( - tx, - state, - store, - "Login", - "Use `openproof login` from another shell to import the current Codex ChatGPT login.".to_string(), - ); - } "/dashboard" => { let store_dash = store.clone(); let tx_dash = tx.clone(); @@ -455,11 +387,6 @@ pub fn apply_local_command( } }); } - "/sessions" => { - state.overlay = Some(openproof_core::Overlay::SessionPicker { - selected: state.selected_session, - }); - } _ => { emit_local_notice( tx, diff --git a/crates/openproof-core/src/commands.rs b/crates/openproof-core/src/commands.rs index b6ecc6a..33f8fb7 100644 --- a/crates/openproof-core/src/commands.rs +++ b/crates/openproof-core/src/commands.rs @@ -3,21 +3,15 @@ use crate::state::AppState; /// All known slash commands for tab completion. pub const SLASH_COMMANDS: &[&str] = &[ "help", - "status", "new", - "clear", "resume", "nodes", - "branches", - "agents", - "tasks", "focus", "agent spawn", "proof", + "lean", "paper", - "questions", "answer", - "instructions", "memory", "remember", "share", @@ -35,14 +29,13 @@ pub const SLASH_COMMANDS: &[&str] = &[ "export all", "autonomous status", "autonomous start", + "autonomous full", "autonomous stop", "autonomous step", "theorem", "lemma", "verify", - "login", "dashboard", - "sessions", ]; /// Compute tab completions for the current command buffer.