docs: fix incorrect CLI commands, flags, and API examples#13
Merged
Conversation
This commit fixes numerous documentation errors to ensure all examples
and command references accurately reflect the actual implementation:
CLI Commands:
- Change `http start` to `http serve` (correct command name)
- Change `mcp start` to `mcp serve` (correct command name)
- Fix default port from 8000 to 8001 for HTTP server
- Fix default host from 127.0.0.1 to localhost for HTTP server
- Fix default limit from 10 to 5 for search command
CLI Flags:
- Change `--pkg` to `--package` (or `-p`) for search command
- Remove non-existent `--log-level` from mcp serve command
- Fix chat command flags: use `--backend`, `--lean-api-key`, `--debug`
instead of non-existent `--model` and `--api-key`
CLI Subcommands:
- Remove non-existent `configure show` and `configure reset` subcommands
- Remove non-existent `data list` and `data status` subcommands
- Document actual subcommands: `configure api-key`, `configure openai-key`,
`data fetch`, `data clean`
API Examples:
- Fix field access: `results.items` → `results.results`
- Fix field name: `item.informal_name` → `item.informal_description`
- Fix method name: `get_citations()` → `get_dependencies()`
- Update all port references from 8000 to 8001
HTTP Server Documentation:
- Fix endpoint: `/api/v1/citations/{item_id}` →
`/api/v1/statement_groups/{group_id}/dependencies`
- Update response JSON examples to match actual API structure
MCP Server Documentation:
- Fix tool names: remove incorrect `lean_explore_` prefixes
- Use correct tool names: `search`, `get_by_id`, `get_dependencies`
- Fix parameter names to match actual tool signatures
All documentation now accurately reflects the codebase implementation.
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
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.
This commit fixes numerous documentation errors to ensure all examples and command references accurately reflect the actual implementation:
CLI Commands:
http starttohttp serve(correct command name)mcp starttomcp serve(correct command name)CLI Flags:
--pkgto--package(or-p) for search command--log-levelfrom mcp serve command--backend,--lean-api-key,--debuginstead of non-existent--modeland--api-keyCLI Subcommands:
configure showandconfigure resetsubcommandsdata listanddata statussubcommandsconfigure api-key,configure openai-key,data fetch,data cleanAPI Examples:
results.items→results.resultsitem.informal_name→item.informal_descriptionget_citations()→get_dependencies()HTTP Server Documentation:
/api/v1/citations/{item_id}→/api/v1/statement_groups/{group_id}/dependenciesMCP Server Documentation:
lean_explore_prefixessearch,get_by_id,get_dependenciesAll documentation now accurately reflects the codebase implementation.