mathlib hanging

Stream: general

[Christopher Upshaw]

So starting yesterday afternoon, whenever I try to import a file from mathlib the lean server just hangs. Keeping the last messages from before I typed the last letter of the path.

For example if I type "import tactic" I get "invalid import: tacti" with the server apparently not doing anything.
I've tried letting it sit for over 10 minutes, and if I restart lean sometimes the line counter at the bottom of the screen goes up, but even when that number goes back to 1 I don't get any messages from lean until I erase the import line.

Anyone have any idea what's going on?

[Yaël Dillies]

Welcome to the orange bar hell! This is pretty common for the Lean server to get hanged up like that. The solution is to get yourself a cache (the .olean files) which will set the server up straight again. You do that using leanproject get-cache (with an optional --rev name_of_the_branch) and restart the server.

[Yaël Dillies]

For some reason, this happens pretty often when you write imports. I'd suggest writing the new import commented out, and then uncomment it. That'll avoid the server seeing the in-between states.

[Christopher Upshaw]

Hmm I did leanproject get-cache and its still hanging instead of importing linear_algebra.clifford_algebra.default. This used to work.

[Christopher Upshaw]

Huh, it looks like my leanpkg.toml got corrupted in some sort of very subtle way? So that leanproject was ignoring the mathlib dependency? Or something? Weird.

[Eric Wieser]

I'm pleased to hear someone else is looking at the clifford algebra stuff!

[Eric Wieser]

Are you working in mathlib itself or a project depending on mathlib?

[Eric Wieser]

Are you working in mathlib itself or a project depending on mathlib?

[Christopher Upshaw]

A project depending on mathlib.

Now it at least doesn't hang, but instead I get "invalid import: data.vector.basic
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)" Which is weird. This was working great until last week.

[Kevin Buzzard]

So remove the directory called _target and then type leanproject up

[Kevin Buzzard]

Or maybe leanproject get-m will help