cache error: dependency loop found involving Mathlib!

Stream: mathlib4

[Xavier Roblot]

Since yesterday, I was getting the following error message when I tried to update the cache:

% lake exe cache get
uncaught exception: dependency loop found involving Mathlib!

After a lot of experiments, I found out that the error happens because some files were importing all of Mathlib, that is starting with the line:

import Mathlib

I understand this is a bad practice in general but this is a development branch and it is useful to have access to all of Mathlib sometimes when developing.

Anyway, I just wanted to put the information out there in case somebody else has the same issue.

[Kim Morrison]

Are you saying you get this error in any downstream project that contains a file with import Mathlib? If that is the case, it is a problem we should fix.

[Michael Rothgang]

FWIW, I thought you meant "on a branch of mathlib, I have a file which does import Mathlib". Feel free to clarify which one you meant :-)

[Xavier Roblot]

Michael Rothgang said:

FWIW, I thought you meant "on a branch of mathlib, I have a file which does import Mathlib". Feel free to clarify which one you meant :-)

Yes, that what I meant: it happened on a branch of Mathlib in which some files were importing all of Mathlib.

[Xavier Roblot]

Kim Morrison said:

Are you saying you get this error in any downstream project that contains a file with import Mathlib? If that is the case, it is a problem we should fix.

I'll see if I can reproduce the error in a cleaner way.

[Eric Wieser]

I guess the failure mode here is more generally:

• Start a new branch with a clean cache
• Make an import loop and commit, which breaks the build
• Clear your local cache
• Attempt to get a partial cache, which fails to compute the needed files because of the import loop

[Eric Wieser]

I think the desired behavior is to cut all the files implicated in the loop, and fetch the cache upstream of them, rather than the error that it sounds like is happening

[Xavier Roblot]

I made #27915 following Eric suggestion.

[Kevin Buzzard]

I have no problems importing mathlib in scratch files in mathlib; it sounds to me like Xavier must have been taking an already-existing file and then increasing the imports to import Mathlib? At least this is the only way I can envisage trouble (and in this case it's pretty clear that there will be trouble).

[Eric Wieser]

I think the issue is that the trouble is worse than it should be

[Xavier Roblot]

Kevin Buzzard said:

I have no problems importing mathlib in scratch files in mathlib; it sounds to me like Xavier must have been taking an already-existing file and then increasing the imports to import Mathlib? At least this is the only way I can envisage trouble (and in this case it's pretty clear that there will be trouble).

Yes, this one in on me. Having a file that import Mathlib is fine but then this file should not be listed in Mathlib.lean. Somehow, I didn't realized that this was the problem at first, maybe because I could not download the cache and build (efficiently) Mathlib. It seems however that there is an error message that warns about that:

% lake build
✖ [242/7003] Running Mathlib
error: build cycle detected:
  +Mathlib.Loop:leanArts
  +Mathlib.Loop:olean
  +Mathlib:setup
  +Mathlib:leanArts
  +Mathlib:olean
  +Mathlib.Loop:setup
  mathlib/Mathlib:leanArts
  mathlib/Mathlib:default
  +Mathlib.Loop:leanArts
✖ [243/7003] Running Mathlib.Loop
error: /Users/roblot/Desktop/EnCours/Lean/Lean4/mathlib4-alt/Mathlib/Loop.lean: bad import 'Mathlib'

So I might have missed that or is it a new thing?
Anyway, since I clearly did something wrong, I am not sure there is the need for a fix.

[Kim Morrison]

It does seem like we could go ahead and download the cache anyway in this situation!