test/change.lean

Stream: mathlib4

[Thomas Browning]

When I run git clone https://github.com/leanprover-community/mathlib4.git, I get the following warning:

warning: the following paths have collided (e.g. case-sensitive paths
on a case-insensitive filesystem) and only one from the same
colliding group is in the working tree:

  'test/Change.lean'
  'test/change.lean'

and then when I run git checkout my_branch, I get the following error:

error: Your local changes to the following files would be overwritten by checkout:
        test/Change.lean
Please commit your changes or stash them before you switch branches.
Aborting

Has anyone else run into this issue?

[Damiano Testa]

I've received a message from @Buster and I'm about to push a name change PR!

[Damiano Testa]

I introduced test/Change.lean to test the change? tactic, but did not realize that this would overwrite test/change.lean on case-insensitive systems.

[Damiano Testa]

#6821

[Damiano Testa]

I'll also write a script to try to avoid this sort of issue in the future!

[Damiano Testa]

git ls-files | sort --ignore-case | uniq -D --ignore-case

seems to work for checking paths that are the same ignoring case.

[Damiano Testa]

The PR is merged! If you pull now, things should work again.

Scott, thanks for merging quickly!

[Damiano Testa]

Let me know if this causes more problems.

[Scott Morrison]

For anyone else who encounters this, I actually couldn't pull the new commit, and had to delete my master branch and check it out again. Fun adventures in case sensitivity!

[Damiano Testa]

Wow! I am sorry to have caused this! Would it make sense to add the pipe above to linting, in order to avoid this kind of issue in the future? If so, I am happy to learn how to do it, but I would appreciate some guidance!

[Alex J. Best]

I would simply add this to the style linter script, similar to how https://github.com/leanprover-community/mathlib4/blob/master/scripts/lint-style.sh#L48-L55 is implementated

[Damiano Testa]

Alex, thanks! I'll do that!

[Damiano Testa]

#6825

Disclaimer: I think that this might be the first time that some bash code that I wrote gets reviewed!

[Damiano Testa]

Would it be useful to have something like

import Lean.Elab.Command

namespace lintUpperLowerCase
open Lean

def toLowerRepetitions (names : Array Name) : List (List Name) :=
let sorted := names.qsort fun n1 n2 ↦ (n1.toString.toLower < n2.toString.toLower)
let groups := sorted.toList.groupBy fun n1 n2 ↦ (n1.toString.toLower == n2.toString.toLower)
groups.filter (List.length · != 1)

elab "#case_clashes" : command => do
  let env := ← getEnv
  let modNames := env.header.moduleNames.push env.mainModule
  match toLowerRepetitions modNames with
    | [] => return ()
    | reps => logInfo (reps.foldl (fun x y => (m!"{x}").compose (m!"{y}\n"))
      "The following groups of files are the same modulo upper/lower-case:\n\n")

end lintUpperLowerCase

as a Lean command, maybe added to #lint?

[Damiano Testa]

Linting for #6825 passed. I have now pushed branch#adomani/testUpperLowerLinter, where I created an empty CODe_OF_CONDUCT.md file to check that the linter would pick it up (it does on my computer).

[Damiano Testa]

Success: it failed!

[Eric Wieser]

I don't think doing this within lean is helpful; we want to protect against clashes in non-lean files too

[Damiano Testa]

Yes, I agree. Also, the test branch duplicated an md file and the linter caught it.

[Johan Commelin]

Thanks! I kicked it on the bors queue