Zulip Chat Archive

Stream: general

Topic: Excessive memory consumption


view this post on Zulip Ashvni Narayanan (Jan 28 2021 at 21:20):

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!

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:21):

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

view this post on Zulip Ashvni Narayanan (Jan 28 2021 at 21:21):

How does one do that?

view this post on Zulip Yakov Pechersky (Jan 28 2021 at 21:26):

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

view this post on Zulip Ashvni Narayanan (Jan 28 2021 at 21:29):

Yakov Pechersky said:

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

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

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:31):

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

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:31):

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

view this post on Zulip Ashvni Narayanan (Jan 28 2021 at 21:31):

Johan Commelin said:

Ashvni Narayanan are you on Windows, or another OS?

Windows

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:32):

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

view this post on Zulip Ashvni Narayanan (Jan 28 2021 at 21:32):

Johan Commelin said:

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

Currently, one.

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:32):

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

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:32):

In there, you can type leanproject build

view this post on Zulip Johan Commelin (Jan 28 2021 at 21:33):

Ashvni Narayanan said:

Johan Commelin said:

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

Currently, one.

Ooh, that sounds bad...

view this post on Zulip Kevin Buzzard (Jan 28 2021 at 21:38):

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.


Last updated: May 08 2021 at 04:14 UTC