chore: adjustments to runLinter so it can be used downstream

[kim-em]

No description provided.

[digama0]

Is there anything we can do to make the default module be the current package instead of Std always? Otherwise I think this will have to be called as lake exe runLinter Mathlib from mathlib.

[kim-em]

Is there anything we can do to make the default module be the current package instead of Std always? Otherwise I think this will have to be called as lake exe runLinter Mathlib from mathlib.

@tydeu, any suggestions?

leanprover-community/mathlib4#8461 is already using lake exe runLinter Mathlib.

[digama0]

I gave this a bit of a think and I think there is nothing that can be done with the current design of lake, unless the linter is turned into a script (which both changes the interface, and also makes it run interpreted). Options considered:

• Influence elaboration somehow so that the name of the current project is embedded in the executable.
  • We can't do this right now because we have no way to influence elaboration other than through builtin options. It would be nice to have a way to declare defs that are reachable from elaboration, similar to autogenerated files like version.h in lean4 repo.
• Call lake to get the name of the default_target(s) and the roots for it.
  • Can't do it because we didn't get lake dump-config.
• Have lake pass us this information in env vars.
  • Lake doesn't tell us much other than the LEAN_SRC_PATH and other things tailored for lean use. It doesn't even say what the current project folder is.
• Add extra hard-coded CLI args to the lake_exe in the lakefile.
  • This seems relatively simple to implement, but lake doesn't do it currently. I'll try to make a PR for this.

Given this, I'll just merge it as-is and we can pursue alternatives in a future PR.

[tydeu]

While I think many of @digama0's feature suggestions are generally reasonable (so feel free to create issues for them!), lake exe runLinter Mathlib looks quite good to me! Nonetheless, one way to achieve a shorter command in the current setup would be a have a lint script that just builds and runs the linter on Mathlib (i.e., in a similar manner to the exe CLI command).