CI update

Stream: FLT

[Kevin Buzzard]

I've spent the day working on CI for FLT. We now have activated a bunch of linters in CI which will check for things like: FLT.lean not being a list of the files in the project, lines being more than 100 characters long, definitions not having docstrings and so on. I did a bunch of work on the project today which caused several PRs to pick up merge conflicts; I fixed the conflicts because I could see how I'd caused them, but in the process of merging master I of course triggered the new CI, so I'm really sorry @Salvatore Mercuri (FLT#414) and @Matthew Jasper (FLT#432), I broke your PRs! Hopefully it's nothing worse than having to add a few docstrings, but another change was that I streamlined imports so there is a chance that you might have had to add some back to get things working again. Looks like all the Lean code is compiling now at least...

[Matthew Jasper]

FLT#432 is working again

[Kevin Buzzard]

Thanks and sorry! I'll review it :-) I've had enough of infrastructure for one day...

[Salvatore Mercuri]

FLT#414 also now passing!