Skip to content

For agents and chats

This handbook is for people and for agents. Do not scrape the HTML. Fetch the markdown.

Start here

File What it is
llms.txt Curated index. Fetch this first.
llms-full.txt The same core pages, concatenated.
raw/ One page at a time, as Markdown. Example: raw/guide/hello-world.md.
robots.txt Allows crawlers; points at llms.txt and the sitemap.

HTML lives at the same path without raw/ and without .md. GitLab source of truth: li-langverse/lic-docs.

Read before you claim what Li does

  1. Provability gaps — today vs target. lic build is not a Lean certificate yet.
  2. Agent handover formats — how Li expects agents to work in a repo.
  3. li-agent-manifest.toml — commands to run (lic check, lic diagnose, tests).
  4. Documentation style — do not invent features; do not skip the gap register.

Suggested ingest

1. GET https://docs.lilangverse.xyz/llms.txt
2. If the task is small, GET the linked raw/*.md pages you need.
3. If the task is “learn Li” or you have budget, GET llms-full.txt.
4. Before writing code or promising proofs, GET raw/verification/provability-gaps.md.

In a clone of this repo, read docs/ directly. Do not paste secrets, tokens, or .env files into a chat.

What not to do

  • Do not treat the styled HTML as the source. The source is Markdown.
  • Do not say lic build runs Lean or closes all proofs unless the gap page says that row is closed.
  • Do not copy ten-page tables from the design spec into a prompt when a link will do.
  • Release notes and daily reports are optional; they are not in llms-full.txt on purpose.