[RFC] JSON package / library config info output

[digama0]

Processing lakefile.lean is a nontrivial cost (~200ms) and a minimum requirement to do anything with lake packages. I think it would be good for lake to generate a parsed version of (some of) the information in a package configuration and stick it somewhere in the build directory, along with a trace so that it is easy to determine if the information is out of date. Then many activities with package management can be handled by reading the JSON file instead of the lakefile, using the trace to determine whether to call lake to refresh the contents of the file. (This could also be part of lake-manifest.json.)

[digama0]

(This is not just about making lake itself faster, but also for better interop for programs that aren't lake to locate files in lean projects. In my case this came up when looking at making lake exe cache more robust and not mathlib-specific.)

[tydeu]

I agree with this and have been sketching out some ideas on how to do this in my own notes. My only point of contention with this proposal is that I do think builds/scripts should still use the complete lakefile data (ideally, through, preprocessed as a olean). On the other hand, I am pretty confident that package management, lake env, and other smaller tools could avoid the lakefile entirely in the common case and just use (new) data in lake-manifest.json.

[digama0]

Using an olean is currently problematic unless you are either lake or link to lake, which is difficult to do reliably right now since lake .a files are not distributed with the nightly that is supposed to process the lakefile.

[tydeu]

Yeah, but I would expect builds and scripts to be done using lake so that should not be a problem.

[digama0]

I don't think lake exe cache can call lake internals, for example, because it is compiled separately. It would have to be run in the interpreter to be able to use lake stuff.

[tydeu]

@digama0 why would lake exe cache be building things?

[digama0]

Right now it is reimplementing a lot of lake's build invalidation logic with the trace files and such. A tool in this class would be basically covered if the manifest included information about the source search path and IR search path for the files in the package.

The reason for this is that it needs to reliably determine what files would cause lake build to do something nontrivial.

[tydeu]

Oh, I certainly assent to putting information like that in the manifest. That was not what I thought you were talking about. I thought you were hoping to determine what things need to be built and how to build them solely through the manifest (or other static information), which is not really possible considering Lake's arbitrarily customizable builds (which notably have precedent in e.g. Haskell's Shake or Ruby's Rake).

[digama0]

"How to build them" clearly requires oleans, since lakefiles can contain build code. Still, it would be nice if we could improve the "linking to lake" situation for that. (Another thing I want to float by you is splitting lake into a separate package with just the requirements to interpret a lakefile, including custom build scripts etc., but not the CLI and things like that. That is, the "lakefile file format", which would allow for alternative lake implementations. From what I can tell, you have actually tweaked import Lake to only contain this information, there are many files not imported when you do this.)

[tydeu]

Still, it would be nice if we could improve the "linking to lake" situation for that.

I fully agree with this. I also do not think the core team is against it, I just think no one has been motivated enough / had enough cycles to do so.

Another thing I want to float by you is splitting lake into a separate package with just the requirements to interpret a lakefile, including custom build scripts etc., but not the CLI and things like that.

I do not think the complexities that come with making that a separate package are worth the cost. However, as you said, I have tried to organize Lake such that (if the oleans were present) a user would be able to just import this stuff without getting everything else as well.