global project timeout (lean3)

Stream: general

[Thorsten Altenkirch]

I have installed a global project (leanproject global-install) so that I don't always have to create this pesky src directory etc everywhere.
This works fine on my laptop but on my desktop I get a timeout when "import tactic" (excessive memory consumption).
This is on a shared directory - maybe this causes some confusion?

[Thorsten Altenkirch]

(deleted)

[Kevin Buzzard]

Do you have mathlib oleans on the desktop? What happens if you manually try compiling a random file in mathlib which is a long way from logic, e.g some random file about polynomials? You can do lean --make path.to.file.lean.

[Thorsten Altenkirch]

Ok, it seems completely broken. I can't even load my old files anymore. I think I am going to reinstall lean.

[Eric Wieser]

It wouldn't surprise me if you are the only user of global-install on this zulip instance

[Thorsten Altenkirch]

This is really strange: I reinstalled lean3, I am using a local project, I did leanproject get-mathlib-cache, I reinstalled the lean extension on visual studio but I still get

invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)

while the same project loads fine on my laptop???

[Eric Wieser]

What does lean --path give from the folder of that local project?

[Floris van Doorn]

Does this persist after running Lean: Restart (or restarting VSCode)? What happens if you do leanproject build from the command line? Did you make sure to open the project (not a single file)?

[Thorsten Altenkirch]

(base) psztxa@IMAC-DGKYNHM5JV3X automaton-in-lean % lean --path
{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/Users/psztxa/Library/CloudStorage/OneDrive-TheUniversityofNottingham/COMP2012-LAC-22-23/automaton-in-lean/leanpkg.path",
  "path": [
    "/Users/psztxa/.elan/toolchains/leanprover-community--lean---3.45.0/bin/../library",
    "/Users/psztxa/.elan/toolchains/leanprover-community--lean---3.45.0/bin/../lib/lean/library",
    "/Users/psztxa/Library/CloudStorage/OneDrive-TheUniversityofNottingham/COMP2012-LAC-22-23/automaton-in-lean/_target/deps/mathlib/src",
    "/Users/psztxa/Library/CloudStorage/OneDrive-TheUniversityofNottingham/COMP2012-LAC-22-23/automaton-in-lean/./src"
  ]
}

[Thorsten Altenkirch]

Just to clarify: it is not just one project, my lean installation seems to be broken altogether. However, I thought that reinstalling lean and reinstalling the lean extension would fix it.

[Thorsten Altenkirch]

Yes, I have restarted vs code and I have now also tried leanproject build

[Thorsten Altenkirch]

no luck :-(

[Mauricio Collares]

By reinstalling lean, do you (also) mean deleting ~/.elan?

[Mauricio Collares]

It's possible that you accidentally edited a .lean file inside this directory after using "Go to Definition" on your editor, which would cause cache problems. Deleting the directory is safe if you have an internet connection when elan tries to redownload the Lean binaries (well, I guess you'll lose overrides and stuff, but perhaps that's good?)

[Thorsten Altenkirch]

After reinstalling another time it now works. No idea what was wrong but thank you for your advice.