Stream: new members
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!
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.
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?
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.
Andrew Elsey (Jul 25 2020 at 13:43):
I guess we'll probably have to go that route. Great, thank you for the information!
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"?
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
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".
Andrew Elsey (Jul 25 2020 at 15:17):
Okay, thanks, I'll look into it!
Mario Carneiro (Jul 25 2020 at 16:49):
@Andrew Elsey I describe the general technique in this post
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