Skip to content

Add user-facing documentation#78

Merged
justincasher merged 7 commits into
mainfrom
justin/docs
Apr 19, 2026
Merged

Add user-facing documentation#78
justincasher merged 7 commits into
mainfrom
justin/docs

Conversation

@justincasher
Copy link
Copy Markdown
Owner

@justincasher justincasher commented Apr 19, 2026

Summary

  • Creates a docs/ folder with seven pages covering getting started, the CLI, the MCP server, the API client, the local backend, configuration, and data models
  • Adds a docs/README.md index with a backend-comparison table and links to each page
  • Links the new docs from the main README.md so they're discoverable in-repo

Creates a docs/ folder with getting-started, CLI reference, MCP server,
API client, local backend, configuration, and data models pages, and
links them from the README so contributors and users can find them
without relying solely on the hosted docs site.
Switches the docs list in the root README and in docs/README.md from
bullets to a two-column table so the page and its description line up
visually.
Covers prerequisites (elan/lake, OPENROUTER_API_KEY, the [extract] extra),
the four stages (doc-gen4 -> parse -> informalize -> embed -> index),
common invocations for full rebuilds and single-stage reruns, the main
flags, and the timestamped output layout under LEAN_EXPLORE_DATA_DIR.
Rewrites every em dash in the documentation, using colons for
definitional lists, parentheses for asides, and semicolons or sentence
breaks where the dash was separating independent clauses.
Readers need install instructions first; the docs table now follows
installation so it lands in a more natural spot for people skimming the
README top-to-bottom.
Promotes the license line into its own section at the bottom so the flow
reads installation -> documentation -> contributing -> cite -> license.
Surfaces the list of packages LeanExplore covers immediately after the
one-line description, so readers see the scope before hitting install
instructions.
@justincasher justincasher merged commit 449c820 into main Apr 19, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant