Zulip Chat Archive

Stream: new members

Topic: emacs


view this post on Zulip Alexandre Rademaker (Oct 23 2018 at 14:02):

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.

view this post on Zulip Rob Lewis (Oct 23 2018 at 14:07):

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.

view this post on Zulip Reid Barton (Oct 23 2018 at 14:07):

C-c SPC

view this post on Zulip Alexandre Rademaker (Oct 23 2018 at 14:13):

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

view this post on Zulip Rob Lewis (Oct 23 2018 at 14:17):

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?

view this post on Zulip Rob Lewis (Oct 23 2018 at 14:18):

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

view this post on Zulip Alexandre Rademaker (Oct 23 2018 at 14:25):

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

view this post on Zulip Aniruddh Agarwal (May 16 2020 at 21:06):

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.

view this post on Zulip Mario Carneiro (May 16 2020 at 21:07):

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

view this post on Zulip Aniruddh Agarwal (May 16 2020 at 21:07):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 21:07):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 21:08):

in vscode there is a "Lean: Restart" command

view this post on Zulip Reid Barton (May 16 2020 at 21:09):

C-c C-r

view this post on Zulip Reid Barton (May 16 2020 at 21:10):

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

view this post on Zulip Aniruddh Agarwal (May 16 2020 at 21:10):

That worked, ty!

view this post on Zulip Aniruddh Agarwal (May 16 2020 at 21:11):

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

view this post on Zulip Reid Barton (May 16 2020 at 21:11):

Yes

view this post on Zulip Reid Barton (May 16 2020 at 21:11):

I have this among my custom-set-variables:

 '(lean-memory-limit 8192)

view this post on Zulip Reid Barton (May 16 2020 at 21:11):

I think it means 8G

view this post on Zulip Reid Barton (May 16 2020 at 21:12):

The default is ridiculously low

view this post on Zulip Jalex Stark (May 16 2020 at 22:54):

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?

view this post on Zulip Sam Lichtenstein (May 16 2020 at 23:07):

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

view this post on Zulip Reid Barton (May 16 2020 at 23:53):

I'm not sure whether VSCode has the same default

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 00:10):

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

view this post on Zulip Reid Barton (May 17 2020 at 06:25):

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

view this post on Zulip Jalex Stark (May 30 2020 at 22:38):

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

view this post on Zulip Alex J. Best (May 30 2020 at 22:43):

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

view this post on Zulip Jalex Stark (May 30 2020 at 22:45):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:54):

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

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 23:01):

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

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 23:01):

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

view this post on Zulip Jalex Stark (May 30 2020 at 23:02):

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

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 23:03):

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

view this post on Zulip Jalex Stark (May 30 2020 at 23:24):

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


Last updated: May 17 2021 at 22:15 UTC