bug in lean imports

Stream: general

[Mario Carneiro]

@Sebastian Ullrich I guess no one has ever tried to use 7 dots in a row in relative imports, but it doesn't work. The = should be a += here, and I tested that if you put import .......test it counts as only one level up (and in general k dots means k mod 3 levels up)

[Sebastien Gouezel]

Mario Carneiro said:

Sebastian Ullrich I guess no one has ever tried to use 7 dots in a row in relative imports, but it doesn't work. The = should be a += here, and I tested that if you put import .......test it counts as only one level up (and in general k dots means k mod 3 levels up)

I was just trying to see if I could store the lftcm tutorials in docs. It wouldn't make sense to have absolute imports there, so I tried with relative imports and I was bitten by this. Do we have the power to fix this now? (For now, I have lowered the depth of subdirectories to avoid more than 3 levels for files calling for_mathlib, but this is really just a workaround)

[Rob Lewis]

Probably good to file as a Lean bug report!

[Sebastien Gouezel]

lean#396