Zulip Chat Archive

Stream: general

Topic: mathlib hanging

Christopher Upshaw (Aug 22 2021 at 01:09):

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 (Aug 22 2021 at 01:39):

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 (Aug 22 2021 at 01:40):

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 (Aug 23 2021 at 19:03):

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

Christopher Upshaw (Aug 23 2021 at 19:17):

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 (Aug 23 2021 at 19:56):

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

Eric Wieser (Aug 23 2021 at 19:57):

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

Eric Wieser (Aug 23 2021 at 20:13):

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

Christopher Upshaw (Aug 24 2021 at 23:23):

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 (Aug 24 2021 at 23:53):

So remove the directory called _target and then type leanproject up

Kevin Buzzard (Aug 24 2021 at 23:54):

Or maybe leanproject get-m will help

Last updated: Aug 03 2023 at 10:10 UTC