Import into lakefile?

Stream: lean4

[Thomas Murrills]

Is it possible to import non-builtin modules into the lakefile?

To #xy, in my use case, I'd like to manipulate the same data in a lake facet/target as I do across a subprocess boundary (in a subprocess called by my facet). This involves e.g. sending json to and from the subprocess. In order for it to have the same format, I duplicate the structures that derive ToJson/FromJson—and the types and API held by those structures—so that they appear in both the lakefile and in files for the exe defining my subprocess.

This seems fragile! :) (It's also a bit inconvenient, and makes things harder to maintain; my lakefile is growing very complex.) Is there a better way, outside of doing something cursed? Am I missing a simpler approach?

I would be okay with my base definitions living in a whole separate package to avoid circularity, but when I tried that, it didn't seem to work.

[Mac Malone]

Unfortunately, no. Lake configuration files can only import code from core modules.

[Thomas Murrills]

I see. Is this intended to remain this way? And/or do you know of any workarounds? Currently I'm considering having a custom elaborator in my lakefile that "pseudo-imports" code at a filepath by essentially copying over the source and parsing/elaborating it in the lakefile. That would obviously be...a suboptimal approach, but it might help make things maintainable. :sweat_smile: