Zulip Chat Archive

Stream: general

Topic: bug in lean imports


view this post on Zulip Mario Carneiro (Dec 24 2018 at 14:22):

@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)

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 20:31):

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)

view this post on Zulip Rob Lewis (Jul 19 2020 at 20:35):

Probably good to file as a Lean bug report!

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 20:46):

lean#396


Last updated: May 06 2021 at 22:13 UTC