## Stream: general

### Topic: Documenting Core

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

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

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

#### 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?

#### Kevin Buzzard (Sep 08 2020 at 16:47):

I kind of want them there by 5th October

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

#### Kevin Buzzard (Sep 08 2020 at 16:49):

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

#### Kevin Buzzard (Sep 08 2020 at 16:49):

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

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

#### 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

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

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

#### Rob Lewis (Sep 08 2020 at 18:03):

Now or whenever you have time, of course!

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

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

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

#### Bryan Gin-ge Chen (Sep 08 2020 at 21:32):

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

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

Thanks Bryan!

#### Rob Lewis (Sep 09 2020 at 14:43):

Maybe we can sneak lean#463 in for Kevin

#### 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