Memory Issues for Very Large Mutual Inductive?

Stream: new members

[Andrew Elsey]

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]

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

[Andrew Elsey]

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]

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]

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

[Scott Morrison]

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]

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]

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]

Okay, thanks, I'll look into it!

[Mario Carneiro]

@Andrew Elsey I describe the general technique in this post

[Andrew Elsey]

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