mysterious hang bug

Stream: maths

[The Leanest]

Hi! I'm using mathlib 3 and when I try to run a file with even a single import statement, it hangs without printing anything (presumably it is hanging on the import statement). Why might this happen??

[Kevin Buzzard]

there are about 10 different reasons why it might happen :-/

[Kevin Buzzard]

are you happy with the command line? How did you create your project? Is the project mathlib itself or an independent project?

[Yaël Dillies]

Do you get the dreaded orange bar of hell?

[Adam Topaz]

The most likely cause is that you might be missing the mathlib olean files, but as Kevin said, we need more info about your setup, and particularly about how you set up your project.

[The Leanest]

I used leanpkg to create the project and then added the dependency with leanpkg add

[Johan Commelin]

That means that lean is compiling half of mathlib, and hence takes 1h15 before that import statement is done.