feat: detect default target on runLinter

[austinletson]

Now runLinter will try to detect all root modules of the default build targets of type lean_exe or lean_lib in Lake's environment using the same resolveDefaultPackageTarget function as lake build.

Closes #795

[austinletson]

awaiting-review

[kim-em]

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

[austinletson]

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

Hmm, this does seem like it could cause the same issue. Is there an example of a safe way to access Lake's internal API? I based this PR on this zulip thread about accessing Lake dependencies in for Mathlibs lake exe mk_all.

Another thought, does the fact that runLinter.lean is built separately from the rest of std as a lean_exe help us out at all?

[austinletson]

Related to this, I created a Zulip thread asking about a Lake command that would provide module and dependency information so we wouldn't have to use Lake's internals in cases such as these. (link)

[tydeu]

@semorrison

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

The problem there just appears to be that a shared library for Lake is not included in the currently Lean distro. That seems like it could be remedied relatively easily if necessary.

[kim-em]

@semorrison

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

The problem there just appears to be that a shared library for Lake is not included in the currently Lean distro. That seems like it could be remedied relatively easily if necessary.

@tydeu, yes please.