Standard library reference

Stream: new members

[ahmεd667]

Hello! Is there some sort of a website which indexes the signatures and docs for (at least) the standard library of Lean? I couldn't find anything in the links mentioned on the Lean homepage or searching this Zulip chat.

[Jireh Loreaux]

docs#Nat you can find the Std reference on the left-hand side bar.

[Jireh Loreaux]

The fact that Std's documentation is incorporated as part of mathlib's documentation is mentioned at the bottom of the README: https://github.com/leanprover/std4

[Jireh Loreaux]

On the community website, the link to the docs is the "API documentation"

[ahmεd667]

Thank you! Indeed I missed the community website

[Jireh Loreaux]

Please note the warning which still applies:

The community is currently in the middle of switching from using Lean 3 to using Lean 4. This website is still being updated, and some pages have outdated information about Lean 3 (these pages are marked with a prominent banner). The old Lean 3 community website has been archived.

[Jireh Loreaux]

But the API documentation is for Lean 4, so that's not applicable to your specific question.

[ahmεd667]

Is there yet something like this, but for third-party libs as well? Think NPM or Hackage. Just using Google/Github search isn't giving me a lot of results

[Jireh Loreaux]

There is no package manager at this point for Lean 4. However, the documentation generator which builds the pages linked above is https://github.com/leanprover/doc-gen4, and I believe you can use it for individual packages, but I've never done this myself. @Henrik Böving is the primary developer of doc-gen4, and he will likely be able to say more, or point you to the correct resources.

[Henrik Böving]

ahmεd667 said:

Is there yet something like this, but for third-party libs as well? Think NPM or Hackage. Just using Google/Github search isn't giving me a lot of results

We don't have a thing where you can upload your documentation yet but in principle it should be clear from the doc-gen README how to add it to your own project. YOu can then host it locally with some HTTP server or put it on the web if you want, e.g. @Siddhartha Gadgil did this in the past iirc.

[Siddhartha Gadgil]

Yes, I have hosted the docs from the code in my course within my course website at http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html.

[Siddhartha Gadgil]

And also the documentation of the formalization of Gardam's theorem is at http://math.iisc.ac.in/~gadgil/unit_conjecture/UnitConjecture.html

[ahmεd667]

Thank you all for you answers :)