doc-gen
doc-gen copied to clipboard
leanprover-community
Generate HTML documentation for mathlib and Lean
This doesn't actually work yet, but contains enough to debug the renderer on the latex.md file Blocked by https://github.com/executablebooks/mdit-py-plugins/pull/46
As this screenshot, display of `unit.star` is glitched.  OS is android. Here is the link. [matrix.pivot.list_transvec_col_mul_last_row_drop](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/transvection.html#matrix.pivot.list_transvec_col_mul_last_row_drop)
Thanks to work by @zhangir-azerbayev , we have a dataset of every declaration in (a recent version of) mathlib translated to natural language. People from OpenAI are interested in improving...
The docs for `list` render as:  However, if we run that code: ```lean inductive {u} my_list (T : Type u) : Type u | nil : Π {T :...
Searching the mathlib library contents in the documentation and filtering of the resulting set of declarations. One is now able to: - search through the declaration names, the module names...
This isn't a full conversion, but should still work after this restructure. The motivation here is to try and separate out "things specific to mathlib" from "things other lean projects...
Example: https://eric-wieser.github.io/mathlib-import-graph/?highlight=core:data.dlist&docs_url=https://leanprover-community.github.io/mathlib_docs/
Originally reported by @ericrbg [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/docgen.20not.20linkifying/near/261243836): > Why do we have that in [the docs for `localization`](https://leanprover-community.github.io/mathlib_docs/ring_theory/localization.html), `is_localization.mk'` doesn't link, when it does exist with exactly that name? (docs#is_localization.mk') As...
I've found the startup time for the search to be very painful, especially since when I click a search result and find its the wrong one, I have to start...
Metadata
Owner
Metadata
Generate HTML documentation for mathlib and Lean