Declare extra dependencies of Lean files

[gebner]

Lean files can use elaborators that read files at compile time. For example include_str in doc-gen4 reads the specified file during compilation and inserts the file's contents as a string literal. The Base.lean file contains this:

def styleCss : String := include_str "../../static/style.css"

If static/style.css changes, then Base.lean needs to be recompiled.

leanprover/lake#58 suggested adding an environment extension which stores the referenced files. Then include_str would add the filename to the environment extension. Lake could then read the referenced files from the .olean file, which contains the serialized environment extension.

[tydeu]

leanprover/lake#58 suggested adding an environment extension which stores the referenced files. Then include_str would add the filename to the environment extension. Lake could then read the referenced files from the .olean file, which contains the serialized environment extension.

How would this help? Lake needs to know the dependencies of files before it elaborates them to see if they have changed in order to determine whether to rebuild the dependent. I do not see what good learning about them afterwards would do.

[gebner]

Shake can do that. The standard example of compiling a C file looks like this:

    "_build//*.o" %> \out -> do
        let c = dropDirectory1 $ out -<.> "c"
        let m = out -<.> "m"
        cmd_ "gcc -c" [c] "-o" [out] "-MMD -MF" [m]
        neededMakefileDependencies m

That is, Shake only learns of the dependencies after building. Just like include_str.

[tydeu]

@gebner I'm not saying it is impossible to record such information. I am just not sure what the use of doing so is. That is, what would you like Lake to do with this information?

[gebner]

That is, what would you like Lake to do with this information?

I think the ultimate goal is clear: Base.olean should be recompiled if style.css changes. The rest is a discussion of how to make that happen.

One option, which the submitter of leanprover/lake#58 probably had in mind, is to record the referenced files while Lean is running. And then have Lake check those recorded dependencies when running lake build the next time. This option is very nice because it doesn't require any action on the part of the user, you just write include_str "my_file" and Lake does the right thing. Obviously, this doesn't neatly fit in the way Lake is implemented right now. But it is very much feasible, as it can be done easily in other systems like Shake.

There are of course also other options, like to manually list the dependencies in the lakefile.

[tydeu]

@gebner

And then have Lake check those recorded dependencies when running lake build the next time.

Ah, are you saying that if Base.lean does not change but style.css does, Lake should then perform a rebuild of Base.lean (using the information about dependencies it obtain from the prior build of Base.lean)?

I didn't realize that! I think I was mistakenly thinking that the goal was to determine the dependency chain without ever elaborating Base.lean. 🤦‍♂️

[Vtec234]

I would also find this feature very useful. We are using include_str to store widget JS code, e.g. here. Ideally we could define a build script for dist/squares.js in the lakefile.lean which is then re-ran whenever squares.tsx changes, triggering also a rebuild of CommDiag.lean. We are currently using an extraDepTarget for the JS build here. This target gets triggered on "Refresh file dependencies" and thus works for interactive use. On the command line with lake build, all the Lean files in the package are rebuilt whenever the jsTarget changes, whereas with include_str I assume we could have finer tracking that only rebuilds CommDiag.lean.

[gebner]

Ah, are you saying that if Base,lean does not change but style.css does, Lake should then perform a rebuild of Base.lean (using the information about dependencies it obtain from the prior build of Base.lean)?

Yes, this is precisely what I meant.

[Vtec234]

Btw, while it would great if the Lean file itself could declare its extra dependencies in elaborators, for widgets it would be a sufficient stopgap if we could specify in the lakefile that a particular (existing) target depends on a particular extra target. For example, in the current lakefile, I would like to specify something like CommDiag.lean depends on squares, Rubiks.lean depends on rubiks, etc. I am not seeing a way to do that currently.

[tydeu]

@Vtec234, I should note that your need and @gebner's feature request are actually different. In your example, you need to specify dependencies to build before the library's modules are elaborated. The feature request here is to specify additional dependencies after the module has been elaborated.

Both of these can be accomplished in a relatively straightforward manner in a custom target. A pre-build dependencies is done use fetch and binds and a post-build dependency is recorded by mixing traces. The problem here is what UX should be provided to do this in a library configuration. For the pre-build dependencies, a list of targets to build before building the library seems reasonable. I am, however, unsure what the proper UX for the post-build dependency would be.

[Vtec234]

@tydeu thank you for looking into this! The two feature requests you point out roughly correspond to my two messages above, which are indeed different. For widgets, specifying dependencies before elaborating the library suffices, although doing so after would be nice and convenient, since we could do it in the relevant Lean file rather than in the lakefile.lean.

I am afraid I don't understand your proposed solution though. In my example, I am not sure how to "get hold" (I mean obtain a variable) for the CommDiag.lean target and how to tell Lake that this file has an additional dependency (dist/squares.js).

[tydeu]

@Vtec234

thank you for looking into this!

And thank you for your reply!

I am afraid I don't understand your proposed solution though. In my example, I am not sure how to "get hold" (I mean obtain a variable) for the CommDiag.lean target and how to tell Lake that this file has an additional dependency (dist/squares.js).

I am sorry, but I do not understand what you are saying here at all.

[Vtec234]

I am sorry, but I do not understand what you are saying here at all.

In short, I'd like to tell Lake somehow that the target for CommDiag.lean is dependent on the target dist/squares.js. So the latter must be up-to-date before building/elaborating CommDiag.lean. I don't understand what a "pre-build" or "post-build" dependency is and how I could use them to do this.