PR : lint style not finding file

Stream: new members

[Hannah Fechtner]

I've just made a very simple PR, but it's not passing the lint-style step.

This is the error I'm getting:

uncaught exception: no such file or directory (error code: 2)
32
  file: Mathlib/Algebra/Module/Zlattice/Basic.lean

I have not touched anything in that file. However, I do see that it's right there in Mathlib!
Screenshot 2024-10-21 at 9.46.19 PM.png

And then I'm getting this message from the bot:

@github-actions[bot] commented on this pull request.

In Mathlib.lean:

> @@ -514,9 +515,9 @@ import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.Torsion
 import Mathlib.Algebra.Module.ULift
-import Mathlib.Algebra.Module.ZLattice.Basic
-import Mathlib.Algebra.Module.ZLattice.Covolume
 import Mathlib.Algebra.Module.ZMod
[imports (comment with "bot fix style" to have the bot commit all style suggestions)] reported by reviewdog 🐶

⬇️ Suggested change
-import Mathlib.Algebra.Module.ZMod
+import Mathlib.Algebra.Module.ZLattice.Basic
+import Mathlib.Algebra.Module.ZLattice.Covolume
+import Mathlib.Algebra.Module.ZMod
In Mathlib.lean:

> +import Mathlib.Algebra.Module.Zlattice.Basic
+import Mathlib.Algebra.Module.Zlattice.Covolume
[imports (comment with "bot fix style" to have the bot commit all style suggestions)] reported by reviewdog 🐶

⬇️ Suggested change
-import Mathlib.Algebra.Module.Zlattice.Basic
-import Mathlib.Algebra.Module.Zlattice.Covolume

I sincerely doubt I should be manually messing around with files unrelated to my PR

[Hannah Fechtner]

do I need to further update mathlib somehow? I did git pull on the master branch, and then made my own branch from there. this was all today, so I cannot imagine it would be that out-of-date

[Julian Berman]

I don't know much about how this works in Mathlib4's CI but I see your PR (which is https://github.com/leanprover-community/mathlib4/pull/18036/files for anyone else) makes changes to Mathlib.lean -- how did you make those / was it by hand? IIRC the one thing I do know is I think that file is supposed to be auto-generated by some script in the repo.

[Julian Berman]

In particular I think you're adding a new file, so something should be adding it to Mathlib.lean, but I think that's not something you do by hand (but let's find out...).

[Julian Berman]

Depending on the answer to ^, what's there now doesn't look right (i.e. the PR is breaking something AFAICT), so I'd run lake exe mk_all again -- you should end up with a diff that only adds one line to Mathlib.lean, not one that adds a line and changes the case on others. (If that doesn't happen, then probably come back and mention that).

[Hannah Fechtner]

Oh, yup, that's very weird (in the Mathlib.lean). I did not generate it by hand - I ran lake exe mk_all

[Hannah Fechtner]

Screenshot 2024-10-22 at 8.31.38 AM.png

[Hannah Fechtner]

Trying to run it again made no changes

[Hannah Fechtner]

But I see that somehow the order of imports is different from that in the master branch:
Screenshot 2024-10-22 at 8.32.03 AM.png

[Damiano Testa]

The shell script that existed before the lean executable explicitly specified what order to sort the files. I thought that the lean executable would have a similar test, but I do not remember the details, I would have to look at this again.

[Damiano Testa]

I checked out your PR and ran mk_all and on my computer it reorders the files:

$ lake exe mk_all --git
Updating 'Mathlib.lean'

$ git diff
diff --git a/Mathlib.lean b/Mathlib.lean
index 647e3836db..36da462b51 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -515,9 +515,9 @@ import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.Torsion
 import Mathlib.Algebra.Module.ULift
+import Mathlib.Algebra.Module.ZLattice.Basic
+import Mathlib.Algebra.Module.ZLattice.Covolume
 import Mathlib.Algebra.Module.ZMod
-import Mathlib.Algebra.Module.Zlattice.Basic
-import Mathlib.Algebra.Module.Zlattice.Covolume
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Algebra.MonoidAlgebra.Defs
 import Mathlib.Algebra.MonoidAlgebra.Degree

[Damiano Testa]

So, it looks like the ordering of files is computer dependent... again! :smile:

[Damiano Testa]

For the moment, just go with the order that CI wants. I will try to figure out where the correct "locale" should be used.

[Hannah Fechtner]

Hmm, I just manually re-ordered it, but it's still not finding the file?
Screenshot 2024-10-22 at 8.41.20 AM.png
So maybe I have deeper issues

[Damiano Testa]

Sorry, there is a capitalization issue.

[Damiano Testa]

(Not sure if someone had already mentioned this, but I just noticed.)

[Hannah Fechtner]

oh I see it!

[Edward van de Meent]

ZLattice vs Zlattice

[Damiano Testa]

Right, it is ZL... not Zl...! :smile:

[Hannah Fechtner]

Oy gevalt! But it's lowercase throughout my entire copy of Mathlib

[Damiano Testa]

So, that is good, I think: sorting should be machine-independent, but casing affects the alphabetical order (as expected).

[Damiano Testa]

Ok, this is a completely separate issue from mk_all not working: this is progress, we are zooming in on where the root issue is.

[Damiano Testa]

You are probably on a case-insensitive system (Windows, maybe)?

[Hannah Fechtner]

Is there any way to automatically get that fixed?
It seems like I am not on an updated copy of mathlib?

[Hannah Fechtner]

I'm on a Mac
in VSCode

[Hannah Fechtner]

Sonoma 14.6.1

[Damiano Testa]

Ok, it is weird that lean had not complained earlier about wrong capitalization, then...

[Damiano Testa]

I am not sure that I know how to fix the root cause, but currently lean is only complaining about the files in Mathlib.lean, right? Simply use what CI wants and let's hope that at least the PR is fixed.

[Hannah Fechtner]

fingers crossed! waiting to see if it will build now

[Damiano Testa]

Ok, linting seems to have gone through!

[Damiano Testa]

I am wondering why you have a lake-manifest change: that should not be there either.

[Hannah Fechtner]

That only appeared after I ran "lake update" and "lake exe cache get"
(Which I did because I thought that might automatically fix the Mathlib.lean)

[Damiano Testa]

Ok, lake update is something that you should never have to use with mathlib. lake exe cache get is something that you should always use! :smile:

[Damiano Testa]

I would probably revert the lake-manifest change, since the dependencies of mathlib have to be carefully picked for everything to work "in-sync" and it is a very delicate issue.

[Hannah Fechtner]

so, if I'm working on a branch of mathlib, how should I update mathlib? (I originally did
git pull on the master branch, and then made a new branch for my PR. but what if I want to update mathlib once I've started working on the PR? is that git merge master?)

[Yaël Dillies]

Yes, exactly. git merge master or git rebase master

[Damiano Testa]

Yes, git pull retrieves the latest version of everything, after that, git merge origin/master will put the master changes on your branch.

[Hannah Fechtner]

thanks!

[Hannah Fechtner]

ohh okay, so I switch back to master, git pull there, and then go to my branch and do git merge master

[Damiano Testa]

I need to go now, but I think that the CI issues are either resolved, or almost resolved!

[Hannah Fechtner]

thank you so much for your help!! I truly appreciate it

[Damiano Testa]

git pull will pull everything and origin/master (rather than master) is where it will store the changes to master, if you are on a branch.

[Julian Berman]

(I noticed it was a capitalization issue, and suspected you were on macOS with case insensitive filesytems, but I didn't see where the bug could be, as as far as I could tell mk_all is using the Lean file walking APIs. I only scanned the rest of the thread, but it does seem worth minimizing if we suspect there's an actual bug.)

[Damiano Testa]

Summarizing, it seems that mk_all produced a case-desensitivized list of module names. mk_all gets this like from (ultimately) docs#System.FilePath.walkDir and we are wondering whether this is a bug in walkDir or whether it is some post-processing (that does not appear to be there) after that.

[Damiano Testa]

Does this sound right?

[Julian Berman]

That sounds right -- "surely" ZLattice isn't the only module which begins with two capitals is it? Surely there's some other module called ZMod or something? Because the output was just title casing those two lines.

[Yaël Dillies]

Anything containing NNRat, NNReal, ENNReal for sure, yes

[Julian Berman]

Oh I bet I know what the issue is.

[Julian Berman]

Hah yes I guessed right. (But I need to figure out why my guess is right before I spoil the fun.)

[Julian Berman]

OK I can't guess how it happened, but some Eric (or other equivalent) may come along and have a guess. Anyways, I think what happened is ZLattice was recently renamed from Zlattice in https://github.com/leanprover-community/mathlib4/commit/85d6c78ac5782869d041c2ca6d3ca83cdde412c3 -- and somehow on your filesystem this change wasn't picked up. What I don't have a guess on is why -- on macOS renames of this sort are invisible because the two paths are equivalent, but git mv normally is good enough that even macOS is OK with picking this up when pulling a branch with commits that do these moves.

[Julian Berman]

TL;DR there's a bug somewhere in something, but pretty sure my guess would be "not Lean and not mk_all.lean", it's somewhere else in the workflow, and I can't reproduce it with "obvious" things like "clone mathlib4 from before that commit and then pull after it", doing so produces the correct result, so something else must have happened but not 100% sure what.

[Yaël Dillies]

Julian Berman said:

I think what happened is ZLattice was recently renamed from Zlattice in https://github.com/leanprover-community/mathlib4/commit/85d6c78ac5782869d041c2ca6d3ca83cdde412c3

The opposite rename happened, as per the commit you are linking Nevermind I can't read

[Damiano Testa]

It's pretty cool how case-insensitivity is a hindrance to mathematical development.