lake stack overflow

Stream: general

[Johan Commelin]

chore(Data/Int/Defs): clear out Init/Data/Int/Basic #14759

In this PR lake build just hangs, whereas lake exe cache clean aborts with a stack overflow...
What is going on?

cc @Mac Malone

[Ruben Van de Velde]

I think it's been a loop in the import graph when I've had those symptoms

[Henrik Böving]

Lake should be capable of detecting import loops afaik

[Ruben Van de Velde]

"should" or "is"? :)

[Ruben Van de Velde]

Looks like my diagnosis was correct

[Arthur Paulino]

If not Lake, it wouldn't be too hard to upgrade cache to detect cyclic dependencies before blowing up the stack by keeping track of a visited data structure in the hashing routine

[Henrik Böving]

Ruben Van de Velde said:

"should" or "is"? :)

src/lake/Lake/Build/Fetch.lean:/-- A recursive build of a Lake build store that may encounter a cycle. -/
src/lake/Lake/Build/Fetch.lean:/-- Log build cycle and error. -/
src/lake/Lake/Build/Fetch.lean:@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
src/lake/Lake/Build/Fetch.lean:  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"

is

[Ruben Van de Velde]

I wonder what Johan ran into, then

[Ruben Van de Velde]

Does it catch a file importing itself directly?

[Henrik Böving]

@Mac Malone ?

[Mac Malone]

Yes, Lake does catch a file importing itself. There is even a test for that. Lake should be incapable of looping. However, it has been observed that a lake build of Mathlib can hang with improper imports (though this does not happen if smaller subsets of Mathlib with the bad import are built). I have yet to figure out why.

[Mac Malone]

This example has given me some ideas, though, so I will take a look again.

[Mac Malone]

Sadly, my idea did not bear fruit. :-(