Skip to content

feat: API map index generator and guide - #1473

Open
Robby955 wants to merge 1 commit into
leanprover-community:masterfrom
Robby955:api-map-site-index
Open

feat: API map index generator and guide#1473
Robby955 wants to merge 1 commit into
leanprover-community:masterfrom
Robby955:api-map-site-index

Conversation

@Robby955

Copy link
Copy Markdown
Contributor

This adds a small index generator for the API maps: lake exe api_map_index reads the API-map.yaml files and writes docs/APIMap.html in the doc-site layout, so the existing maps are browsable in one place. A short guide for writing map entries is included at docs/API_MAP_GUIDE.md. It complements the per-area maps being added under #1414 and picks up new ones automatically. Nothing in the repo invokes the generator yet: the site build would add lake exe api_map_index next to its existing lake exe stats mkHTML step to publish the page.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@github-actions github-actions Bot added the CI label Jul 31, 2026
@Robby955
Robby955 force-pushed the api-map-site-index branch from f574e33 to 38401fb Compare July 31, 2026 01:55
@Robby955
Robby955 marked this pull request as ready for review July 31, 2026 02:38
Comment thread scripts/APIMapIndex.lean

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this all looks really good. But I think we should think about whether html is the correct output for this.

Maybe if we output a json or a (large) yaml file containing all of the necessary information, on the website rep we can include a page which displays that json or yaml in nice ways. I've found this approach often works better (and we should likely do that for the stats page aswell). I think the TODO list is done in this was as an example.

(I also think the html outputted would no longer be compatible with the format of the website).

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll take a look!

@jstoobysmith jstoobysmith self-assigned this Jul 31, 2026
@jstoobysmith jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 31, 2026
@Robby955

Copy link
Copy Markdown
Contributor Author

Reworked as suggested: the HTML output is gone, and the script now emits a single YAML data file, docs/_data/APIMap.yml, mirroring the repo's existing data-file exporter pattern with the same mkFile convention and uncommitted artifact. It carries each map's path, title, overview, parents, references and requirements with completion counts and GitHub links, so the website repo can render it the same way as the task list.

@Robby955
Robby955 force-pushed the api-map-site-index branch from 38401fb to b308117 Compare July 31, 2026 15:29
@Robby955

Copy link
Copy Markdown
Contributor Author

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants