Zulip Chat Archive

Stream: condensed mathematics

Topic: docstrings


view this post on Zulip Kevin Buzzard (Apr 05 2021 at 13:41):

As Johan knows, I am trying to get on top of what has been done so far so I can take more of a lead in the project now my teaching is essentially over for the year. I'm doing this by writing module docstrings for every file in the module_docstrings branch.

view this post on Zulip Johan Commelin (Apr 05 2021 at 13:47):

@Kevin Buzzard together with @Mario Carneiro I've been doing more work on the rescale_iso branch. We'll take care of any merge conflicts.

view this post on Zulip Johan Commelin (Apr 05 2021 at 13:47):

One thing that we did is moving all the rescale.lean files into a rescale/ subdirectory of src/.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 13:47):

I've not yet got to the murky details of the rescalings.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 13:48):

My branch does literally nothing other than adding module docstrings and some other files called stuff like FILES.md which contain a summary (basically written for me -- they will go stale at some point and might need to be removed) of what is happening in each directory.

view this post on Zulip Johan Commelin (Apr 09 2021 at 06:55):

Massive thanks to @Kevin Buzzard for writing lots and lots of docstrings all through the project. There are now also FILES.md in most directories, summarising which files are there, and what they do.


Last updated: May 09 2021 at 15:11 UTC