Zulip Chat Archive

Stream: general

Topic: Documenting Core


view this post on Zulip Kevin Buzzard (Sep 08 2020 at 16:41):

I'm writing lecture notes for my undergraduates. I don't like linking to raw code in the github lean and mathlib repos in these notes, because some students have no interest in Lean and don't want to click on a link in good faith and be taken to something intimidating. Now we have the docs though, so I'm upgrading my notes and adding links.

A lot of what I'm doing in my notes is super-foundational stuff though, so in core, and I'm noticing that the link I have for e.g. transitive is kind of hopeless, as it doesn't have a docstring. I'm sure there all sorts of ways of adding docstrings to core defs but rather than launching in I thought I'd ask here as to what the preferred form of a PR would take. Ideally I'd only like to add about ten docstrings I suspect, but one might argue that they're important for mathematicians.

view this post on Zulip Rob Lewis (Sep 08 2020 at 16:43):

If they're normal doc strings on declarations, and they don't forward-reference things in mathlib, you can PR them to core just like you would to mathlib.

view this post on Zulip Rob Lewis (Sep 08 2020 at 16:44):

All at once or as you write them, doesn't really matter. If there are certain people you want to review them it's a good idea to tag them though. Not everyone watches core PRs very closely.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 16:47):

If I PR them to core then they may not appear in the docs immediately though, am I correct?

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 16:47):

I kind of want them there by 5th October

view this post on Zulip Rob Lewis (Sep 08 2020 at 16:48):

Right, but I think we're due for a release soonish, since nat.pow is finally dead. And a docs-only release would be very easy.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 16:49):

OK I will make some PR's to core. Thanks.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 16:49):

My memory was that this was not how we documented core tactics.

view this post on Zulip Rob Lewis (Sep 08 2020 at 16:51):

The tactic docs are different because they're not just doc strings. You added a bunch of tactic_doc_entrys which are defined in mathlib.

view this post on Zulip Rob Lewis (Sep 08 2020 at 16:54):

By the way, if you're linking to the docs from your notes, you should consider linking to http://leanprover-community.github.io/mathlib_docs/find/transitive instead of the direct link. This is the pattern docs#transitive uses. It will be more robust if declarations change files, which isn't likely to happen for transitive, but maybe for others

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2020 at 17:56):

It's relatively easy to make a new release of community Lean. If anyone feels like we're due for one, feel free to ping me and I can put one together within a few hours. (It's reviewing that's the hard part, and Gabriel's been doing a great job of keeping up with that.)

view this post on Zulip Rob Lewis (Sep 08 2020 at 18:03):

I'd be ready now, to be honest, I'm actively fighting nat.pow and would love to have those changes go live.

view this post on Zulip Rob Lewis (Sep 08 2020 at 18:03):

Now or whenever you have time, of course!

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2020 at 18:57):

There are two open PRs which have been active recently: lean#458 and lean#462. From what I can tell they're both fairly close to being merged (?), so I'll wait a bit longer for those.

view this post on Zulip Reid Barton (Sep 08 2020 at 19:03):

I'd be just as happy to have a release happen before lean#458--it's not urgent for me, and both it and the nat.pow change will require fairly large changes to mathlib, which might be easier to deal with separately.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 21:24):

I just made a small core branch and tried to push to github and I get a permissions error. Do I have write access to non-master branches of leanprover-community/lean? I am kbuzzard on github.

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2020 at 21:32):

@Kevin Buzzard I've just sent you an invitation.

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 14:26):

Since lean#462 has been merged, I'm planning to release 3.20.0c later today (unless @Gabriel Ebner beats me to it).

view this post on Zulip Rob Lewis (Sep 09 2020 at 14:28):

Thanks Bryan!

view this post on Zulip Rob Lewis (Sep 09 2020 at 14:43):

Maybe we can sneak lean#463 in for Kevin

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 14:52):

Yes, I promise not to start working on this before so any other PRs that managed to get merged before then will make it into 3.20.0c as well.


Last updated: May 12 2021 at 23:13 UTC