Linkify builtin types like `Sort`, `Prop`, and `Pi`

leanprover / doc-gen4

Document Generator for Lean 4

Apache License 2.0

65 stars 41 forks source link

Linkify builtin types like `Sort`, `Prop`, and `Pi` #90

Open eric-wieser opened 1 year ago

eric-wieser commented 1 year ago

It would be good to forward-port the features from:

[x] https://github.com/leanprover-community/doc-gen/pull/172 Instance lists for builtin types, like we already have for inductive types
[ ] https://github.com/leanprover-community/doc-gen/pull/173 Distinguishing between different ways of printing pi types. This probably should adapt to the Lean4 changes around pretty-printing.
[ ] https://github.com/leanprover-community/doc-gen/pull/174 Linkifying these special types

The PRs above are all centered around this page: https://leanprover-community.github.io/mathlib_docs/foundational_types.html

hargoniX commented 1 year ago

In general it is unclear right now what thing we want to use for documentation that is not directly related to code. Despite building doc-gen4 I have in fact basically no clue about web development at all :D so implementing this type of prose documentation is something I don't want to invest too much time on when I can instead be helping at the code generator front.

There have also been a few people that want to integrate existing documentation tools better with the Lean stuff like LeanInk so maybe this would be the place for documentation like this to live? I'm unsure, where to put what documentation is still an open question :/

eric-wieser commented 1 year ago

The prose itself isn't really what matters here; it's primarily about being able to ask "what instances does mathlib put on pi types", which is very much directly related to code. The components of doing so are roughly:

finding somewhere to emit "Instances for" for these special builtin types. If you don't want to write any prose, don't bother. Headings alone is enough for now.
modifying the scraping component to detect typeclasses on pi and Prop etc (you might already have code that does this if you copied it from doc-gen 3)
Modifying the Lean4 equivalent of pp.links to attach links to these builtin types

hargoniX commented 1 year ago

I do have an implementation in #93 for sort variants. I am not yet sure how to do pi types in the current framework. It might be that this requires a patch similar to the one we had for function applications with constants in the compiler.