Documenting Core

Stream: general

[Kevin Buzzard]

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.

[Rob Lewis]

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.

[Rob Lewis]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

I kind of want them there by 5th October

[Rob Lewis]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Rob Lewis]

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.

[Rob Lewis]

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

[Bryan Gin-ge Chen]

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.)

[Rob Lewis]

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

[Rob Lewis]

Now or whenever you have time, of course!

[Bryan Gin-ge Chen]

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.

[Reid Barton]

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.

[Kevin Buzzard]

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.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Rob Lewis]

Thanks Bryan!

[Rob Lewis]

Maybe we can sneak lean#463 in for Kevin

[Bryan Gin-ge Chen]

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