Definition docstrings

Stream: FLT

[Kevin Buzzard]

Yesterday I spent some time making CI more picky, basically because my eyesight is not what it once was and when I make font sizes bigger it's annoying to have lines which are over 100 characters. So now FLT has a bunch of linters running and if your PR doesn't pass them, it will fail CI.

However there are already a bunch of things merged into the project that would have failed CI but didn't, because they were merged before yesterday. These things are now tracked in the file scripts/nolints.json. This file was 250 lines long yesterday and almost all complaints in it are of the form "this definition doesn't have a docstring". If you see some definitions in there and you think you know what they are, then feel free to write a PR adding docstrings and then run the magic incantation lake exe runLinter --update FLT and you'll find that the file magically gets smaller. For example I made a PR adding a bunch of docstrings yesterday in the adele files, so I could get on top of where we were, and then I made this https://github.com/ImperialCollegeLondon/FLT/pull/442 and the nolints file went from 250 lines to 200 :-)

My priority at the minute is to get docstrings on the declaractions which are "active" parts of the project (e.g. adeles right now, Hecke operators later this week when I get back to them)