refactor(cli): remove 9 unused slash commands, fix help text bugs#2
Merged
Conversation
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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
/clear,/sessions,/login,/status,/branches,/agents,/tasks,/questions,/instructions/leancommand to tab completion and help (existed but was hidden)/autonomous fullto tab completionRemoved commands
/clear/new/sessions/resumewith no args does the same thing/login/status/proof/branches/proof/agents/tasks/questions/answeris kept/instructionsReport functions on
AppStateare retained as public API for dashboard/headless use.Test plan
cargo build -p openproof-clicargo clippy -p openproof-cli -p openproof-core -- -D warningscargo test --workspace(23 pass)cargo fmt --check/helpoutput is clean and accurate/leantab-completes and shows Lean state