lint about mathlib-tools HOT 7 CLOSED

This sounds like a good idea. Do you have a more specific description? Or even an implementation? I already thought that mk_all could be a leanproject command (without necessarily removing the bash version from the mathlib repository). This would be trivial to implement. What requires a bit of thinking is the Lean part. I know mathlib CI runs lean --run scripts/lint_mathlib.lean, but I guess copying that file to leanproject is not quite right.

from mathlib-tools.

Maybe the best thing to do would be a way to reliably simulate locally whatever CI does. To make sure that the two don't diverge, we could consider making CI run leanproject ci as well. Changes to CI would then be changes to leanproject. I have no idea of this is a good idea. @robertylewis @gebner what do you think?

from mathlib-tools.

I think they already wrote they prefer not to use leanproject in CI, but maybe this was not a general comment.

from mathlib-tools.

I think it's probably better to keep CI separate from leanproject.

You can very easily mimic what CI does, if you're in a mathlib repo:

./scripts/mk_all.sh
lean --run scripts/lint_mathlib.lean
./scripts/rm_all.sh

but this has side effects. It will create nolints.txt in whichever directory you run it in. It will remove any all.lean files that already existed, which could be annoying. It will also take quite a while to run and will be silent until the end.

If you're doing this in a non-mathlib repo, then obviously the lint_mathlib.lean script won't work. We could probably refactor the linter code a bit to produce a function that will lint a project (given by the root directory). Then your script will need to create all.lean for the project, create a .lean file that imports this and runs the right lint command, and call Lean on it.

I don't think this offers much for mathlib. Linting requires building all of mathlib first; we're moving away from doing that locally. If you push to a branch to get oleans, you might as well just look at the CI lint output there. The main use is for projects importing mathlib.

from mathlib-tools.

Ok, I can easily run those three lines locally when needed. So let's not do anything for now.

from mathlib-tools.

What if we created a general hook in leanproject so that, if there's a script scripts/lint.sh in the repo, leanproject lint would call it?

from mathlib-tools.

If there is enough motivation for linting we can make everything from leanproject, without a shell script. But it doesn't seem high priority.

from mathlib-tools.