Excessive memory consumption

Stream: general

[Ashvni Narayanan]

I had a file with 0 sorrys. I moved some lemmas in this file to the relevant files, after which my files stopped compiling / started giving dozens of excessive memory consumption errors. What did I do wrong?

Any help is appreciated, thank you!

[Johan Commelin]

do you also get the error when you compile in a terminal?

[Ashvni Narayanan]

How does one do that?

[Yakov Pechersky]

I would just do Restart Lean in VSCode. Or reopen VSCode.

[Ashvni Narayanan]

Yakov Pechersky said:

I would just do Restart Lean in VSCode. Or reopen VSCode.

I tried both. Does not seem to be working :(

[Johan Commelin]

@Ashvni Narayanan are you on Windows, or another OS?

[Johan Commelin]

Also: In VScode, how many files do you have open?

[Ashvni Narayanan]

Johan Commelin said:

Ashvni Narayanan are you on Windows, or another OS?

Windows

[Johan Commelin]

Ok, in the "Start menu" search for "git bash"

[Ashvni Narayanan]

Johan Commelin said:

Also: In VScode, how many files do you have open?

Currently, one.

[Johan Commelin]

then you will get a terminal. with cd some_directory you can change directories till you are in your mathlib folder

[Johan Commelin]

In there, you can type leanproject build

[Johan Commelin]

Ashvni Narayanan said:

Johan Commelin said:

Also: In VScode, how many files do you have open?

Currently, one.

Ooh, that sounds bad...

[Kevin Buzzard]

Ashvni it might be easier to just sort this out on the discord. give me 10 minutes to finish cleaning the kitchen and I'll be there.