Zulip Chat Archive

Stream: new members

Topic: Memory Issues for Very Large Mutual Inductive?

view this post on Zulip Andrew Elsey (Jul 25 2020 at 13:16):

Hi , Lean Scrub here. I'm working with my colleagues to embed a rapidly growing DSL in Lean. We're tied into Lean as we needs its excellent semantics/math formalisms. Right now, I'm running into pesky "excessive memory consumption" issues stemming from maybe 800-1000 LOC and a few ~100-200 line mutual inductives. These mutual inductives might need to reach > 1000 LOC (maybe a few thousand, if possible). Maybe I'm being stupid, but I can't find any way online to increase the memory allocated to Lean. More info: Developing out of VSCode with the Lean plugin on an Ubuntu Docker. Is increasing the memory even an option? Any pointers or documentation on how to do that? Would compiling instead be the way to go for us? Sorry to bother and greatly appreciate any help!

view this post on Zulip Rob Lewis (Jul 25 2020 at 13:19):

You can increase the Lean: Memory Limit option in VSCode, which defaults to something like 4gb iirc.

view this post on Zulip Andrew Elsey (Jul 25 2020 at 13:30):

Oh duh, see that. Thank you! That's a little scary, however...if I'm running into memory issues at 4gb, when we scale to an order of magnitude+, it sounds like our only hope is compiling?

view this post on Zulip Johan Commelin (Jul 25 2020 at 13:31):

I certainly recommend putting stuff in different files and compiling them. It will give some speedup. Not sure if it will save much memory, though.

view this post on Zulip Andrew Elsey (Jul 25 2020 at 13:43):

I guess we'll probably have to go that route. Great, thank you for the information!

view this post on Zulip Scott Morrison (Jul 25 2020 at 13:58):

Also, hopefully, you've seen the various tales of woe and warning about working with mutual here, and considered the advice that usually it's better to avoid that keyword and just "roll your own"?

view this post on Zulip Andrew Elsey (Jul 25 2020 at 14:31):

I haven't, actually. Not sure what you mean by roll my own. If you have any protips, they're very welcome. The issue is a lot of our grammar productions interact with each other, and have the potential to become very big, so mutual seems ostensibly necessary in my limited understanding

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:43):

Mutual inductive types are automatically unraveled by lean 3 into inductive types, but humans can sometimes do this process better -- "rolling their own".

view this post on Zulip Andrew Elsey (Jul 25 2020 at 15:17):

Okay, thanks, I'll look into it!

view this post on Zulip Mario Carneiro (Jul 25 2020 at 16:49):

@Andrew Elsey I describe the general technique in this post

view this post on Zulip Andrew Elsey (Jul 25 2020 at 17:19):

Thanks Mario, that's a huge help, I'm going to try to apply that

Last updated: May 14 2021 at 06:16 UTC