Excessive memory consumption error

Stream: new members

[Will Midwood]

Hi all,

I've been encountering the error "excessive memory consumption detected at 'type checker' (potential solution ..)", I understand that there has been a few similar threads pertaining to this error, to which I've tried the solutions to. I've tried:

• Running leanproject get-cache
• Running leanproject get-mathlib-cache
• Restarting the VS-Code lean server (countless times)
• Running leanproject build
• Running source ~/.profile

I'm not actually sure how to increase the memory consumption threshold. I'm running this in Alma Linux and I've recently upgraded my mathlib. Any help would be much appreciated :)

[Alex J. Best]

What project are you working on (mathlib, project depending on mathlib)? You could also try uninstalling and reinstalling your lean toolchain with elan. What is the output of leanproject build?

[Will Midwood]

I'm working on a project that depends on mathlib, I think the output of the leanproject build was exit code 1, but I'll double check when I can.

[Alex J. Best]

you could try deleting the _target folder, running leanproject get-mathlib-cache and leanproject build again and pasting the whole output here

[Will Midwood]

Here is the output:

Building project dissertation
configuring dissertation 0.1
mathlib: trying to update _target/deps/mathlib to revision 50092e4a9fda259fe1c6430468f3fac003d43f56
> git checkout --detach 50092e4a9fda259fe1c6430468f3fac003d43f56    # in directory _target/deps/mathlib
HEAD is now at 50092e4a9f feat(analysis/convolution): integral of a convolution over positive reals (#18353)
> lean --make src
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.

[Kevin Buzzard]

cool -- you have a broken setup. Are you working inside a project? What's the output of ls?

[Kevin Buzzard]

Something which can often be helpful in situations like this is sending a screenshot of VS Code open, with the file explorer tab open and your project directory opened, and also a juicy error in the infoview. But I think we're closing in on the issue.

[Alex J. Best]

did you try uninstalling and reinstalling the toolchain?

[Will Midwood]

@Alex J. Best If you are referring to your previous comment, then yes, otherwise I'm not too familiar on what that is.

[Will Midwood]

The output of ls is:
leanpkg.path leanpkg.toml MT4519LectureNotes.pdf src/ _target/

[Alex J. Best]

How did you install lean? You should hopefully have used elan to manage different lean versions, if you uninstall the toolchain and reinstall it it could help

[Alex J. Best]

What does elan toolchain list show in the terminal

[Alex J. Best]

and elan self update for good measure

[Will Midwood]

elan toolchain list yields:

stable (default)
leanprover-community/lean:3.50.3

[Will Midwood]

elan self update only yields:
#info: checking for self-updates

[Kevin Buzzard]

Which version of elan are you on?

[Alex J. Best]

Yeah I would say try elan toolchain uninstall both of them and delete the _target folder, then try leanpkg configure leanproject get-m from the project root again

[Amos Turchet]

sorry for revamping this thread: I seem to have the same issue trying to get a project to work. I have in previous days made (what I believe are) the same installation steps in other M1 Macs and everything works. When I try to do the same now i get the error

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

Some possibly useful info:
Working on Mac mini (M1 chip, 2020)
elan 1.4.5 ( )
elan toolchain list: stable (default)
leanprover-community/lean:3.50.3

[Kevin Buzzard]

Does the project depend on mathlib and if so, have you got a fully-compiled mathlib? What happens if you just try and compile a file from the project on the command line?

[Amos Turchet]

Yes

[Amos Turchet]

In fact I tried open one of the files from the math library in VSCode and I get the same issue

[Amos Turchet]

I even tried creating a new project with nothing on it to see if the issue was that but I got the same result

[Kevin Buzzard]

How did you create this new project?

[Amos Turchet]

Via leanproject

[Kevin Buzzard]

And it worked fine with no errors?

[Amos Turchet]

The leanproject yes

[Amos Turchet]

The issue comes up in VSCode with any lean file

[Kevin Buzzard]

And what happens if you compile the lean file on the command line?

[Kevin Buzzard]

How much RAM do you have, BTW?

[Amos Turchet]

I haven’t tried

[Amos Turchet]

I will as soon as I’m
Back on the computer

[Amos Turchet]

8GB btw

[Amos Turchet]

This is what I got running leanproject build

diophantine_approx % leanproject build
Building project Venez
configuring Venez 0.1
mathlib: trying to update _target/deps/mathlib to revision 4d06b17aea8cf2e220f0b0aa46cd0231593c5c97
> git checkout --detach 4d06b17aea8cf2e220f0b0aa46cd0231593c5c97    # in directory _target/deps/mathlib
HEAD is now at 4d06b17aea chore(data/set/intervals/monotone): fix names (#18924)
> lean --make src

[Riccardo Brasca]

This looks good. After leanproject build do you still have the error in VS Code (maybe restart it)?

[Amos Turchet]

Yes! In fact something even stranger happend

[Amos Turchet]

I tried loading the Atelier files and everything works in VSCode

[Amos Turchet]

But the other project still gives me the "excessive memory..." error

[Riccardo Brasca]

That's weird (for those not there, the Atelier files are a normal Lean project).

[Amos Turchet]

I also tried opening up the project in a different computer at home at everything works also in VSCode

[Amos Turchet]

I was wondering whether to reinstall VSCode completely

[Filippo A. E. Nuccio]

Just to be sure: what is the memory limit set on the machine where this does not work? You can go (in VSCode) to Settings, type "Lean" in the field up in the window, and check "Memory Limit".

[Amos Turchet]

Its 4096

[Filippo A. E. Nuccio]

Well, certainly enough.

[Amos Turchet]

The strange thing is that I get this issue only inside the folder project "diophantine approx" but not with other projects, nor in different computers with the same project

[Filippo A. E. Nuccio]

Ah, so you can obtain a working copy of mathlib (with no link to dioph. approx) on that machine?

[Amos Turchet]

apprently yes

[Filippo A. E. Nuccio]

perhaps try a leanproject clean followed by a leanproject upgrade-mathlib? Then I am out of suggestions...

[Riccardo Brasca]

I agree, it seems that something messed up your olean

[Amos Turchet]

unfortunatly that didnt' work :smiling_face_with_tear:

[Amos Turchet]

(thanks guys for the help)

[Amos Turchet]

I'll try reinstall VSCode again

[Filippo A. E. Nuccio]

I am not 100% sure this is related to VSCode, but since I am not 2% sure of anything else, I cannot advice against it...

[Amos Turchet]

I thought that since running it from the terminal via leanproject build worked the issue was VSCode, but I might be totally wrong

[Amos Turchet]

I honestly have no idea what is going wrong

[Filippo A. E. Nuccio]

Nor have I, so go for a re-install of VSCode, with :fingers_crossed:

[Amos Turchet]

reinstalling VSCode didn't solve the problem unfortunatly

[Amos Turchet]

in fact now I get the same issue also in the file NumberTheory.lean in the atelier files at the command
import number_theory.zsqrtd.basic

[Filippo A. E. Nuccio]

Do you think you can uninstall and reinstall elan?

[Amos Turchet]

I tried uninstall "everything" elan, mathlib etc and reinstalling everythin, now things are in fact worse

[Amos Turchet]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Issues.20with.20Installation.20.28Mac.20M1.29

[Amos Turchet]

the "worse" part was solved but reinstalling everything after deleting all mathlib didn't solve the problem

[Amos Turchet]

now the error message is slightly different (but similar)
invalid import: data.option.defs excessive memory consumption detected at 'type checker' (potential solution: increase memory consumption threshold)

[Eric Rodriguez]

can you redownload the whole repository and show the terminal steps?

[Amos Turchet]

from the leanproject get?

[Eric Rodriguez]

yeah from there should be good

[Amos Turchet]

the leanproject get gives

leanproject get https://github.com/adomani/Atelier_Lean_2023.git
Cloning from https://github.com/adomani/Atelier_Lean_2023.git
configuring rome 0.1
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 401924, done.
remote: Counting objects: 100% (689/689), done.
remote: Compressing objects: 100% (245/245), done.
remote: Total 401924 (delta 564), reused 530 (delta 444), pack-reused 401235
Receiving objects: 100% (401924/401924), 221.18 MiB | 7.01 MiB/s, done.
Resolving deltas: 100% (322537/322537), done.
> git checkout --detach 25a9423c6b2c8626e91c688bfd6c1d0a986a3e6e    # in directory _target/deps/mathlib
HEAD is now at 25a9423c6b chore(*): add mathlib4 synchronization comments (#18772)
Looking for mathlib oleans for 25a9423c6b
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 3093 [00:05, 530.61/s]
amoswork@Mac-mini-di-Amos LEAN % cd Atelier_Lean_2023
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % leanproject get-mathlib-cache
Looking for mathlib oleans for 25a9423c6b
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 3093 [00:05, 537.80/s]

[Amos Turchet]

I also did a leanproject get-mathlib-cache at the end but it didn't make any difference

[Kevin Buzzard]

So there is a chance that you've got corrupted mathlib oleans I guess. You could remove the file .mathlib/25a9423c6b2c8626e91c688bfd6c1d0a986a3e6e.tar.xz from your system and then run leanproject get-m again.

[Amos Turchet]

ok I removed the file you suggested and run leanproject get-m
then code .
and I got the same issue

[Kevin Buzzard]

There is also a chance that you've got a corrupted core Lean installation; to fix that you need to remove the directory .elan/toolchains/leanprover-community--lean---3.50.3 and the file .elan/update-hashes/leanprover-community--lean---3.50.3 and then run leanproject get-m again (which will redownload Lean)

[Kevin Buzzard]

No wait -- it all compiles fine on the command line, right?

[Amos Turchet]

btw the memory limit for Lean in VSCode is set to 4096

[Kevin Buzzard]

I wouldn't bother doing this. If you had a borked Lean then you wouldn't be able to compile on the command line. The problem must be somewhere with VS Code.

[Kim Liesinger]

Did you change any settings in VSCode, e.g. hard code a path of Lean or something? (Hopefully not! But something like this could cause a problem.)

[Amos Turchet]

yes the command line does not get any issue

[Amos Turchet]

here's the terminal output of leanproject build

Building project rome
configuring rome 0.1
mathlib: trying to update _target/deps/mathlib to revision 7d34004e19699895c13c86b78ae62bbaea0bc893
> git checkout --detach 7d34004e19699895c13c86b78ae62bbaea0bc893    # in directory _target/deps/mathlib
HEAD is now at 7d34004e19 chore(*): add mathlib4 synchronization comments (#18966)
> lean --make src
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:8:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:15:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:23:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:28:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:34:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:40:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:49:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:9:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Logic_Tutorial.lean:55:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:41:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:46:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:85:48: error: invalid expression
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:85:57: error: invalid expression
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:30:0: warning: declaration 'rome.is_limit_const' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:76:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:41:0: warning: declaration 'rome.is_limit_add' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:83:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:62:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:51:0: warning: declaration 'rome.is_limit_mul_const_left' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:55:0: warning: declaration 'rome.linear_at_0' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:57:0: warning: declaration 'rome.sandwich' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:90:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:64:0: warning: declaration 'rome.limit_add_const' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Class.lean:113:0: warning: declaration 'rome.linear_add_cnst_of_affine' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:71:0: warning: declaration 'rome.linear_add_cnst_of_affine' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Class.lean:120:0: warning: declaration 'rome.affine_of_linear_add_cnst' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:74:0: warning: declaration 'rome.affine_of_linear_add_cnst' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Functions_Tutorial.lean:79:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:46:0: warning: declaration 'rome.preimage' uses sorry
module.to_distrib_mul_action : distrib_mul_action A M
module.add_smul : ∀ (r s : A) (x : M), (r + s) • x = r • x + s • x
module.zero_smul : ∀ (x : M), 0 • x = 0
I.carrier : set A
I.add_mem' : ?M_1 ∈ I.carrier → ?M_2 ∈ I.carrier → ?M_1 + ?M_2 ∈ I.carrier
I.zero_mem' : 0 ∈ I.carrier
I.smul_mem' : ∀ (c : A) {x : A}, x ∈ I.carrier → c • x ∈ I.carrier
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:79:0: warning: declaration 'rome.preimage' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:65:0: warning: declaration 'rome.intersection' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:81:58: error: failed to synthesize type class instance for
A : Type,
_inst_1 : comm_ring A,
I J : ideal A,
x y : A,
ᾰ : x ∈ I,
ᾰ : x ∈ J
⊢ has_inter (ideal A)
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:88:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:144:34: error: failed to synthesize type class instance for
A : Type,
_inst_1 : comm_ring A,
u : Aˣ
⊢ has_inv A
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:117:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:130:0: warning: declaration 'rome.quot' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: parsing at li/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:165:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:147:0: warning: declaration 'rome.ideal.unit_mul_mem_iff_mem' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: parsing at li/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:110:0: warning: declaration 'rome.preimage_prime' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: parsing at li/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: parsing at li/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: rome.nat.my_induction/- Checking 3 declarations (plus 0 automatically generated ones) in the current file with 26 linters -/

[Amos Turchet]

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS. -/
#check @rome.nnreal.my_induction /- argument 3: (P_zero : P 0) -/

/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:139:0: warning: declaration 'sum_squares_mod_4' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: rome.nat.my_i/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:155:0: warning: declaration 'three_mod_four_is_inert' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:162:0: warning: declaration 'three_mod_four_if_inert' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: rome.nat.my_i/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:168:0: warning: declaration 'Fermat' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:179:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:203:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/NumberTheory.lean:211:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: rome.nat.my_induction/- Checking 1 declarations (plus 0 automatically generated ones) in the current file with 26 linters -/


/- All linting checks passed! -/
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean:209:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean:204:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/generalizations/1.generalizations.presentationTemplate.lean: rome.nat._exampleTry this: exact monotone_const
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % rm .mathlib/25a9423c6b2c8626e91c688bfd6c1d0a986a3e6e.tar.xz
rm: .mathlib/25a9423c6b2c8626e91c688bfd6c1d0a986a3e6e.tar.xz: No such file or directory
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % rm ~/.mathlib/25a9423c6b2c8626e91c688bfd6c1d0a986a3e6e.tar.xz
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % leanproject get-m
Looking for mathlib oleans for 7d34004e19
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 3113 [00:05, 544.00/s]
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % code .
amoswork@Mac-mini-di-Amos Atelier_Lean_2023 % leanproject build
Building project rome
configuring rome 0.1
mathlib: trying to update _target/deps/mathlib to revision 7d34004e19699895c13c86b78ae62bbaea0bc893
> git checkout --detach 7d34004e19699895c13c86b78ae62bbaea0bc893    # in directory _target/deps/mathlib
HEAD is now at 7d34004e19 chore(*): add mathlib4 synchronization comments (#18966)
> lean --make src
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:60:0: warning: declaration 'rome.is_limit_mul_const_left' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:66:0: warning: declaration 'rome.sandwich' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:99:0: error: invalid definition, '|' or ':=' expected
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:73:0: warning: declaration 'rome.limit_add_const' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:85:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:92:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:99:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Limits.lean:45:0: warning: declaration 'rome.is_limit_add' uses sorry
module.to_distrib_mul_action : distrib_mul_action A M
module.add_smul : ∀ (r s : A) (x : M), (r + s) • x = r • x + s • x
module.zero_smul : ∀ (x : M), 0 • x = 0
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:46:0: warning: declaration 'rome.preimage' uses sorry
I.carrier : set A
I.add_mem' : ?M_1 ∈ I.carrier → ?M_2 ∈ I.carrier → ?M_1 + ?M_2 ∈ I.carrier
I.zero_mem' : 0 ∈ I.carrier
I.smul_mem' : ∀ (c : A) {x : A}, x ∈ I.carrier → c • x ∈ I.carrier
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:79:0: warning: declaration 'rome.preimage' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:144:34: error: failed to synthesize type class instance for
A : Type,
_inst_1 : comm_ring A,
u : Aˣ
⊢ has_inv A
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:147:0: warning: declaration 'rome.ideal.unit_mul_mem_iff_mem' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:65:0: warning: declaration 'rome.intersection' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:81:58: error: failed to synthesize type class instance for
A : Type,
_inst_1 : comm_ring A,
I J : ideal A,
x y : A,
ᾰ : x ∈ I,
ᾰ : x ∈ J
⊢ has_inter (ideal A)
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Class.lean:110:0: warning: declaration 'rome.preimage_prime' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:88:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:130:0: warning: declaration 'rome.quot' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:165:0: warning: declaration '[anonymous]' uses sorry
/Users/amoswork/Desktop/LEAN/Atelier_Lean_2023/src/Ring_Ideals_Tutorial.lean:117:0: warning: declaration '[anonymous]' uses sorry
external command exited with status 1
Command '['leanpkg', 'build']' returned non-zero exit status 1.

[Kevin Buzzard]

In VS Code File -> Preferences -> Settings, search for lean. When you see Lean: Executable Path does it say lean?

[Amos Turchet]

yes it says lean

[Kevin Buzzard]

For Lean: Time Limit does it say some large number? (mine says 1000000)

[Amos Turchet]

time limit is set to 100000

[Kim Liesinger]

Oh, you said above the memory limit is set to 4096. Can you try something larger?

[Kevin Buzzard]

I think that's probably enough. What happens if you just restart Lean after the error with ctrl-shift-p and then type "Lean: restart"?

[Amos Turchet]

restarting lean gives me back the same issue

[Amos Turchet]

maybe I should restart the computer?

[Amos Turchet]

(out of ideas otherwise)

[Kim Liesinger]

Try increasing the memory limit first!

[Amos Turchet]

how much should i do it?

[Kim Liesinger]

Kevin's message was not referring to my suggestion, but to your message about the time limit.

[Kim Liesinger]

How much do you have? :-)

[Kim Liesinger]

I think 8gb is meant to be plenty for mathlib?

[Amos Turchet]

I have 16GB

[Amos Turchet]

I'll try 8192

[Kim Liesinger]

You'll probably have to restart Lean after changing the setting. Just restarting VSCode is probably simplest.

[Amos Turchet]

i did restart lean from VSCOde

[Amos Turchet]

and i restarted VSCode
it got "kind of slow" but the error message is gone :tada:

[Amos Turchet]

does Lean really need that much memory?

[Kevin Buzzard]

I got annoyed with my 16 gig machine and upgraded to a 32 gig machine because I use Lean a lot. But I survived with a 16 gig machine for years (when mathlib was smaller)

[Amos Turchet]

I was just puzzled I didn't have the same issue in other Mac with the same settings

[Amos Turchet]

glad that at least this solved the problem

[Amos Turchet]

and thanks so much for the help!

[Yaël Dillies]

I personally just use gitpod.io even though my machine is a beast (a few people here can attest) because downloading cache is too slow on my student connection.