Automatically detect module for lake exe runLinter

[austinletson]

Instead of users manually providing a module to lint with the lint-module input, automatically detect which module to lint.

Depending on how this automatic detection works, we may still want to allow users to manually specify which module to lint.

[kim-em]

I think we can just look for e.g.

@[default_target]
lean_lib Mathlib

and decide on the basis of that to run it on Mathlib.

It would be nice if there were a way to query lake directly for this! @tydeu, any ideas there?

[digama0]

Should this issue be moved to batteries?

[austinletson]

The original intention here was detection contained in lean-action, similar to the detection of Mathlib in detect_mathlib.sh.

However, if batteries's lake exe runLinter will be the standard way to lint lean projects it seems generally useful to have dynamic default module detection. My understanding is that currently the default module to lint is Batteries so if you run lake exe runLinter (instead of lake exe runLinter SomeModule for instance) in a downstream package it still lints the entirety of batteries.

[tydeu]

As a more general question: should we have a lake lint that functions similar to lake test but for linting?

[austinletson]

@tydeu Would this be a good use case for lake install.

Users could run lake install lean-lint and lake exe lean-lint? Similar to the rust-clippy linter usage?

[kim-em]

@tydeu, in the meantime, do you have a suggestion for what we ask lake here?

In batteries we need to generate lake exe runLinter Batteries, in mathlib lake exe runLinter Mathlib, etc.

I think getting the answer to: "please tell me all defaultTarget lean_libs" would suffice here.

[digama0]

This is not difficult to do using the Lake API. I just want this to be a Batteries issue so that the implementation task is not lost. (For that matter we should also have a mathlib issue tracking using the Lake API in cache.)

[kim-em]

Okay: leanprover-community/batteries#795

[oliver-butterley]

This is not difficult to do using the Lake API. I just want this to be a Batteries issue so that the implementation task is not lost. (For that matter we should also have a mathlib issue tracking using the Lake API in cache.)

Prior to runLinter being updated to autodetect the module:

Is there an easy way to ask Lake what is the default module? Would a similar method exist to ask for the requires?

Of course it can be done by a script reading the lakefile but I perhaps there is a more elegant way.

[tydeu]

@oliver-butterley A script is the best solution at the present. I do hope to implement better solutions in the future.

[kim-em]

Mario and Mac's answers seem to contradict here. Can't we do this via the Lake API, rather than scraping the lakefile?

[tydeu]

@semorrison I fully agree with Mario's answer. By "script", a meant some Lean code using the Lake API. The alternative I understood @oliver-butterley to be suggesting was doing this through the Lake CLI, which is not possible at present.

[oliver-butterley]

Indeed, I was hoping that the API mentioned by Mario was exposed in the Lake CLI. I.e., that something like lake info followed by package, lean_lib or requires would return the respective data of the current project directory.

Thanks for the clarification.

[kim-em]

Any hints about the relevant API function? :-)

[austinletson]

leanprover-community/batteries#811 should resolve this.

I used the resolveDefaultPackageTarget function to match the behavior of lake build, although there may be a more straightforward method.

[austinletson]

I am closing this as not planned since it is out of score for lean-action. leanprover-community/batteries#811 should still resolve this, however lean-action users should wrap any usage of the batteries linter in lake lint