Testing new linter framework

Stream: mathlib4

[Damiano Testa]

One part of adding linters is slower build times. In a PR that is already delegated, I am trying to mitigate this, by getting linters to only run on files that are git-modified.

This works well with Linux computers (at least, it works well on mine!) and I checked that it does not seem to break the online server (and assumes that every file is modified).

Could someone using Windows or MacOs try out the command below?

Thanks!

import Lean

open Lean

def isGitModified (modName : Name) : IO Bool := do
  -- On the `whitespace` test file we always return `true`, since we want the linter to inspect
  -- the file.
  if modName == `MathlibTest.Whitespace then
    return true
  let diffFiles ← (do
    let gd ← IO.Process.run {cmd := "git", args := #["diff", "--name-only", "master..."]}
    pure (some gd)) <|> pure none
  if let some diffFiles := diffFiles then
    if diffFiles.isEmpty then return false
    let diffModules ← (diffFiles.trimAscii.toString.splitOn "\n").mapM
      fun s : String => (moduleNameOfFileName s none <|> return Name.anonymous : IO Name)
    return diffModules.contains modName
  else
    return true

-- Replace `Mathlib.Tactic.Linter.Whitespace` with files that are locally modified/non-modified
-- and see if there are any errors and whether the result is actually correct!
#eval
  isGitModified `Mathlib.Tactic.Linter.Whitespace

[Aaron Liu]

do I just paste this into a scratch file

[Damiano Testa]

Yes, please and see whether you get consistent information.

[Damiano Testa]

(In doubt, the linter should think that every file is modified.)

[Damiano Testa]

In case you are curious, the linter is calling git diff --name-only master... from the shell and then checking whether the currently modified file is in the list or not.

[Damiano Testa]

What I am not sure about is what happens if the git call fails/breaks something.

[Aaron Liu]

I tried it on master and it returns false on Mathlib.Tactic.Linter.Whitespace
then I tried it on my branch where I have modified Mathlib.Order.RelClasses, it returns false on Mathlib.Tactic.Linter.Whitespace but returns true on Mathlib.Order.RelClasses
commenting out and uncommenting the #eval to run the command again doesn't change anything

[Damiano Testa]

Ok, so this seems to behave as intended, thanks!

[Damiano Testa]

What system is this?

[Damiano Testa]

(Note that a file that is modified, but the changes have not been committed, does not count as modified as far as this command is concerned. The actual linter that uses this command has a separate mechanism to detect this, not relying on git.)

[Aaron Liu]

Damiano Testa said:

What system is this?

not sure what exactly you're looking for

[Aaron Liu]

the #version command outputs

Lean 4.27.0-rc1
Target: x86_64-w64-windows-gnu Windows

[Damiano Testa]

Did you use it with Windows? MacOs? Linux?

[Damiano Testa]

My main concern is that relying on calling external commands, such as git could have unintended consequences on the linter, which I want to avoid as much as possible.

[Damiano Testa]

However, I only have access to Linux computers and I would like to see some evidence that the same behaviour that I see also applies to different operating systems.

[Chris Henson]

If you need to do this for individual files as that type signature suggests, would it be a little nicer to use the exit code from for instance git diff --quiet master -- Mathlib/Tactic/Linter/Whitespace.lean? This should also detect unstaged changes.

[Damiano Testa]

I like the idea of the exit code for individual files! I think that the reason I got to this, is that in an earlier prototype, I was storing all the modified files in an environment extension once, and then I was reading that value on each file. I later decided to run git on every file, with a mechanism to avoid running it on every command of every file.

[Damiano Testa]

However, given the granular, per file approach, your solution looks cleaner, I agree. Thanks!

[Michael Rothgang]

Can somebody on windows test this, please? I'd love to get this merged, but would prefer even more to know that this seems to work on windows.

[Michael Rothgang]

Just checking: if git is not installed, this code will exit gracefully --- right?

[Eric Wieser]

What happens if this is in a depth-1 repository clone where there is no prior history?

[Eric Wieser]

Michael Rothgang said:

I'd love to get this merged

Does "this" correspond toa PR? I don't see it up-thread.

[Michael Rothgang]

This corresponds to #26299

[Kim Morrison]

This feels really scarily hacky, and I hope we don't merge anything where the linter framework queries git. Sorry. :-(

[Kim Morrison]

If we need to do things like this, it must be done from the outside: some test in CI decides which files have been modified, and re-runs lake build with different settings to enable additional linters.

[Damiano Testa]

How about this, instead.

In CI, we set the linters off. However, while CI is building, we create copies of the modified files only and on those we run the linters.

[Damiano Testa]

This means that the modified files will be built twice: once in CI without linters and once in CI with linters.

[Damiano Testa]

The advantage, though, is that all the files downstream of the changes only get built once and without the linters.

[Damiano Testa]

Since the new files need to be built with the linters on anyway, the overall cost is just building one extra time the modified files without the linters.

[Edward van de Meent]

i think this setup will not have the intended effect when a PR adds a new linter?

[Edward van de Meent]

since it won't lint the downstream files with the new linter

[Damiano Testa]

This issue was there before. This change is intended only for linters that have already passed over mathlib.

[Michael Rothgang]

If you make a PR modifying this linter, you'd disable this change, and once CI passes, revert it. This is a tiny bit annoying, but I don't anticipate many modifications to the whitespace linter.