PRs that change CI

Stream: CSLib

[Fabrizio Montesi]

Dear all,
I've added a label for PRs called 'CI Change' (https://github.com/leanprover/cslib/issues?q=label%3A%22CI%20Change%22). Please use it when submitting PRs that change our CI and/or testing infrastructure, so that we can be extra careful when dealing with a batch of PRs that await merge.

[Chris Henson]

I realized we haven't been great about using this label, so I added it to some current PRs. Let's try to prioritize these in the order of merging to prevent any unexpected CI failures.

To keep everyone appraised, here is a short summary:

• cslib#181 has the net effect of checking for missing docs, thanks to everyone for quickly adding these!
• cslib#184 removes the mergeWithGrind linter. We can add this back later in a weekly test like Mathlib does, but this currently gives a -47.3% reduction in build instructions that will make both local development and CI much faster. (And make nightly-testing easier for me to maintain)
• cslib#189 I just opened to check for problematic grind annotations. It identified several that I for the time being have added as testing exceptions that we should follow up on in later PRs.

[Fabrizio Montesi]

Does cslib#181 still need help?

[Chris Henson]

Yes, there are four docstrings remaining that I believe are all in files where you are the listed author.

[Fabrizio Montesi]

Will get to it asap.

[Fabrizio Montesi]

almost there, fixing a merge conflict

[Chris Henson]

Okay, thanks! I think the other two will not merge conflict, but ping me if there's any issues.

[Chris Henson]

Yeah, I merged main on them to be safe and retrigger CI, no conflict.

[Chris Henson]

All of these have been merged, thank you for the reviews. For currently open PRs, please merge main to pick up these changes.