`EnvExtension` for in-code configuration

[xubaiw]

How about adding an EnvExtension to lake so that we can add to package configuration directly in code with CoreM?

The original thought is to trace external files in include_str, and it comes to a more generalized pattern:

1. include_str can specify the external file to trace with this extension.
2. lean4-alloy can notify lake to build the generated file.
3. codes can now depend on some common packages for system library searching heuristics.

[xubaiw]

But now I'm not very clear about the type of this extension. Shall we expose a full StateT m PackageConfig or to have some restriction on that?

[tydeu]

To clarify, do you mean an environment extension that is is used when elaborating the lakefile or an extension that is used when elaborating source files in the package? If you mean the later, this would require some form import or plugin to augment the environment as lake doesn't currently have any direct control over source file elaboration.

[xubaiw]

Oh I made a mistake on how lake works. I mean the source file. So we may have to hack into leanc for this to work.

[tydeu]

Fyi, I closed this as it was born from a confusion about how Lake works and that confusion has been cleared up.

[gebner]

This was a bit of #xy, but the original issue is still unsolved. Should we add another issue for "how to tell lake about dependencies like files read by include_str"?

[tydeu]

Should we add another issue for "how to tell lake about dependencies like files read by include_str"?

@gebner Sure. A clear issue on matter explain what is desired would be good. It wasn't even clear to me that was primary proposition here. (I see that is used sort of as a motivating example, but the proposed feature was very different.)

[gebner]

Done. leanprover/lean4#2762