emacs

Stream: new members

[Alexandre Rademaker]

how to show a type info of a region? If I have a cursor on a symbol it shows me in the mini-buffer the type, but if I select an expression I don't have the type in the mini-buffer.

[Rob Lewis]

There's a hole command for doing this -- put {! !} around the expression. Then there's a key command to trigger the hole command but I forget what it is in emacs.

[Reid Barton]

C-c SPC

[Alexandre Rademaker]

hum, it didn't find one valid identifier. Assuming that once the mini-buffer is called I have to use the Infer

[Rob Lewis]

It should say "Infer type of the expression in the hole", maybe it's not displaying properly. Hole commands are slightly buggy sometimes. Do you have a small example I could try?

[Rob Lewis]

I'm on VS Code, so we can at least see if it's an editor issue.

[Alexandre Rademaker]

I will try with VS. Maybe I can isolate a fragment to show here. I will try

[Aniruddh Agarwal]

I'm trying to edit some files in mathlib in emacs with lean-mode, and I'm getting a ton of "excessive memory consumption detected" errors. I don't normally get these errors when editing lean files in smaller projects.

[Mario Carneiro]

you ran out of memory, random things are failing. Restart lean

[Aniruddh Agarwal]

Sorry, what does "restart lean" mean? Should I restart emacs?

[Mario Carneiro]

ah, I don't know what the emacs command for this is

[Mario Carneiro]

in vscode there is a "Lean: Restart" command

[Reid Barton]

C-c C-r

[Reid Barton]

The cause could also be you accidentally modified something in mathlib and need to rebuild it

[Aniruddh Agarwal]

That worked, ty!

[Aniruddh Agarwal]

Can I increase the memory consumption limit to prevent the error from occuring again?

[Reid Barton]

Yes

[Reid Barton]

I have this among my custom-set-variables:

 '(lean-memory-limit 8192)

[Reid Barton]

I think it means 8G

[Reid Barton]

The default is ridiculously low

[Jalex Stark]

Reid Barton said:

I have this among my custom-set-variables:

 '(lean-memory-limit 8192)

should VSCode users also worry about increasing the memory budget?

[Sam Lichtenstein]

How does one set the VSCode analog of the lean-memory-limit emacs variable that Reid alludes to below?

[Reid Barton]

I'm not sure whether VSCode has the same default

[Bryan Gin-ge Chen]

The default for vscode-lean is 4096. I've never had to change it.

[Reid Barton]

I think in emacs it's 1G for some reason.

[Jalex Stark]

Bryan Gin-ge Chen said:

The default for vscode-lean is 4096. I've never had to change it.

any advice on how to change it? my only strategy was to try ctrl-shift-p: lean in vscode and see if it had a button for "open the settings file"
I'm currently in a state where I can use lean for a few minutes after restarting the server, but memory slowly leaks until it hits the limit, then i can't do anything and have to restart it. I have enough memory on my machine that "give it 3x more space" would be fine, and would let me live with this state for a while longer until i can figure out the cause

[Alex J. Best]

Click the cog on the lean extension in the sidebar to open the extension settings, then scroll down to Lean: Memory limit

[Jalex Stark]

hmm i'm not sure what "cog on the lean extension in the sidebar" means, actually I'm not sure I know "sidebar" means

[Kevin Buzzard]

You can just go file -> preferences -> settings and then search for lean

[Bryan Gin-ge Chen]

Here's a screenshot of the sidebar. The cog is at the very bottom. Screenshot-2020-05-30-19.00.46.png

[Bryan Gin-ge Chen]

I guess it's officially called the "Activity bar": https://code.visualstudio.com/docs/getstarted/userinterface

[Jalex Stark]

Thanks, I feel pretty silly. I clicked on that cog, but I thought I was looking for something lean specific

[Bryan Gin-ge Chen]

Yeah, the way VS Code organizes settings definitely takes some getting used to.

[Jalex Stark]

now that I've set my memory to 16k MB, i'm not getting weird errors, and suggest and library_search seem to be running significantly faster. my lean memory usage seems to hover just above 4GB most of the time and spike when i use the aforementiond search tactics