runLinter should determine the target module by asking Lake

[semorrison]

No description provided.

[austinletson]

I created draft PR #811, in which the current target module is either the first lean_exe root module or the module corresponding to the first lean_lib in Lake's environment. However, I assume we want a more flexible default.

What criteria should we use to determine the target module(s)? Are there cases where we want to run the linter on multiple modules by default?

If we are okay with linting multiple modules by default, what about "lint all modules inside either a default target lean_exe root or default target lean_lib in the Lake workspace"?

[austinletson]

I have updated #811 to use any root modules of lean_exe or lean_lib default targets.