Lake now selects a different executable when there are multiple with the same name.

[semorrison]

Std and Mathlib have both previously had a lean_exe called runLinter.

Prior to v4.1.0-rc1, in Mathlib, running runLinter would run the Mathlib one. After v4.1.0-rc1, it instead runs the Std one.

This had the unfortunate effect of allowing us to merge the first attempted bump to v4.1.0-rc1 while linting was actually failing, because this change had effectively disabled linting in CI!

As a workaround for now, I have renamed runLinter to Mathlib to runMathlibLinter.

Proposed change:

• restore the original behaviour, so the "furthest downstream" executable wins.
• possibly give a warning?
• whatever is different from previously, document in RELEASES.md

This issue may be sufficient to cut a new release candidate, depending on how strongly people feel about the naming of the linter executable.

[tydeu]

@semorrison Ah, the problem here is packages and executable now have a strict order and the current package is at the end of that order (because it is a topological ordering of dependencies). Previously, they had no defined order and it was just pure luck that Mathlib won (likely because it is alphabetically before Std and Lake uses an RBMap). I think the solution here is to check the workspace root first before checking the packages.

[tydeu]

@semorrison Also note the correct one can also be run disambiguated via mathlib/runLinter (which the CI should maybe use?)

[tydeu]

@semorrison Oh, and the name of the executable can be changed independently of the target via the exeName setting.

Finally, did this turn out to be a blocker? Or can a fix wait for later?

[semorrison]

No, no blocker. I just renamed the Mathlib runLinter to runMathlibLinter. It's good to know mathlib/runLinter would have worked.

In the longer term we've realised that Std's and Mathlib's runLinter are essentially duplicated code, and probably should be combined (it's a trivial generalization of the Std linter script).

So I think the low-urgency resolution to this issue should be:

• prefer executables from the current project