Can I run CI locally?

Stream: mathlib4

[Dominic Steinitz]

Is there some way of running the CI operations locally so as not to have to wait for CI to send me a message saying I had forgotten to do something?

[Michael Rothgang]

What exactly do you really want to do? CI does some things you're not interested in.

[Michael Rothgang]

lake build builds all your code; lake exe runLinter runs the linters on each file. lake exe lint-style checks for remaining style issues. These should get you most of the way.

[Junyan Xu]

#lint at the end of each file you changed may be good enough for catching things forgotten (docstrings, etc.)

[Michael Rothgang]

Indeed; lake exe runLinter will take in the order of a few minutes; #lint on a single file in the order of seconds.

[Junyan Xu]

Yeah, those global linters requiring compiling the whole mathlib are proably faster to run on the cloud.

[Dominic Steinitz]

Thank you both :-)