elaboration slowness

Stream: lean4

[Arthur Paulino]

Hello :wave:
We've developed a custom DSL for ZK circuit building called Aiur. This is its elaboration metaprogram.

However, as the program we write on it grows, the elaboration time grows too much to the point of making the development process too painful.

We've split the code written on that DSL in multiple files (as per this PR), but I'm wondering if there's anything else we could do to make it go faster.

Thanks!

[Arthur Paulino]

Let me simplify the question: are there general techniques for speeding up the elaboration of code written in a custom DSL?

[Henrik Böving]

I'd say what you are doing looks fine (well, apart from the awful indentation of the ite IMO :P) and you should profile it. I guess there might be a way to add parallelism into the elaboration if that's not already happening but that would be about the only thing that comes to mind.