Type checker runs out of memory

Stream: maths

[Quarrie]

For some reason, whenever I try to typecheck my project I run into a compiler error that says that Lean ran out of memory at "type checker."

[Quarrie]

I searched the error in the Zulip archive and could only find one other instance of it, which was apparently resolved by getting up-to-date oleans. I tried this. It did not solve anything.

[Kevin Buzzard]

Is this lean 3 or lean 4? Are you using mathlib?

[Quarrie]

Lean 3.50.3 with what was the latest version of mathlib a few weeks ago

[Mauricio Collares]

Mathlib was only bumped to 3.50.3 a week ago. Are you using elan? It is highly recommended (over installing specific lean versions using your package manager, that is).

[Mauricio Collares]

Any given mathlib commit is associated to a specific lean version (via the leanpkg.toml) file, and the oleans only work for that particular version. Elan takes care of that for you by downloading and using the version declared in the leanpkg.toml file.

[Kevin Buzzard]

Are you working in mathlib itself or in a project which depends on mathlib? Does leanproject get-m, run in your project, fix the problem?

[Quarrie]

Mauricio Collares said:

Mathlib was only bumped to 3.50.3 a week ago. Are you using elan? It is highly recommended (over installing specific lean versions using your package manager, that is).

Yes, I am using elan/leanproject, learned that the hard way lol

[Quarrie]

Kevin Buzzard said:

Are you working in mathlib itself or in a project which depends on mathlib? Does leanproject get-m, run in your project, fix the problem?

Depends on mathlib, and I already checked

[Kevin Buzzard]

After leanproject get-m, what happens if you try leanproject build on the command line?

[Quarrie]

Kevin Buzzard said:

After leanproject get-m, what happens if you try leanproject build on the command line?

Well, I get a bunch of compiler errors that imply that none of the import statements are being accepted, and in VSCode itself I still get this error on the imports

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

[Kevin Buzzard]

Just to be clear -- are you trying leanproject build in the root directory of your project? What does lean --make src/ do? If imports aren't being accepted then your project is corrupt in some way. Perhaps you want to post the leanpkg.path and leanpkg.toml from your project.

[Quarrie]

lean --make src/ parses the entirety of mathlib.

[Quarrie]

and yes, I am running build from project root

[Quarrie]

leanpkg.path

builtin_path
path _target/deps/mathlib/src
path ./src

leanpkg.toml

[package]
name = "mathlib-tensor-lib"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "46a64b5b4268c594af770c44d9e502afc6a515cb"}

[Kevin Buzzard]

and what's the output of leanproject get-m?

[Quarrie]

Looking for mathlib oleans for 46a64b5b42
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 3020 [00:15, 193.30/s]

[Kevin Buzzard]

Assuming it just downloads oleans as normal, the most common issue which causes errors such as yours is that someone has edited your set-up of core Lean by accident (e.g. by jumping to definition and then pressing a key). You can fix this with brute force uninstalling Lean 3.50.3 with rm -rf ~/.elan/toolchains/leanprover-community--lean---3.50.3 ~/.elan/update-hashes/leanprover-community--lean---3.50.3 and then trying lean --make src again; then elan should redownload Lean and hopefully it fixes your problem.

[Quarrie]

Trying that nwo

[Quarrie]

It did not, in fact, fix my problem.

[Quarrie]

Is it possible to update the leanproject utility in-place? I tested creating a new project, and it seems to think the latest Lean version is 3.33.0 even though 3.50.3 is the only one I have installed.

[Kevin Buzzard]

There is some debugging output when you make a new project which at some point essentially prints out a random version of Lean. Are you sure that your new project thinks it's on 3.33.0, or was this part of random debugging output? What does the leanpkg.toml have to say about the matter? That is the source of truth.