Static facets and Export.Parse not built

[xhalo32]

Currently, when building comparator with an already built/distributed lean4export, it tries to build Export.Parse leading to a permission denied issue when the artifacts of lean4export are distributed in a read-only state (as is the case with nix e.g.).

To fix this, lean4export should also build Export.Parse which can be fixed by adding globs = ["Export.*"] to lakefile.toml under the Export library configuration (otherwise, when building comparator for example, lake tries to build these in the immutable location /path/to/lean4export/.lake).

This would be sufficient to build comparator's oleans, but as it also contains an exe which import Export.Parse, it needs the static library facets (including the .c.o.export files that are found under .lake/build/ir/Export/) which again, when missing, lake tries to build in the immutable location. To build static facets as part of lean4export we should add defaultFacets = ["static"] to the Export library configuration.

I can submit a PR for this if it's okay?

[nomeata]

This sounds like we are using lake here in a way that works with "normal" use of lake, but breaks assumptions by a separate tool (you mention nix)? Or can you demonstrate the issue using just lake?

[xhalo32]

I agree my use is outside the "normal" use of lake and to demonstrate this issue without nix I came up with the following contrived setup:

1. Clone comparator and run lake update inside. This populates .lake/packages/{lean4export,lean4checker}.
2. Build lean4export in a "standalone" way (noting that comparator's and lean4export's lean-toolchain is the same leanprover/lean4:v4.32.0-rc1): cd .lake/packages/lean4export && lake build
3. Change back to comparator's directory and remove write permissions to lean4export: chmod -R a-w .lake/packages/lean4export/
4. Run lake build still in comparator's directory and observe the permission denied error

✖ [2/9] Building Export.Parse
error: permission denied (error code: 13)
  file: /home/niklash/Projects/comparator/.lake/packages/lean4export/.lake/build/lib/lean/Export
Some required targets logged failures:
- Export.Parse
error: build failed

Now if we repeat step 1, and then replace lakefile.toml in .lake/packages/lean4export with the following:

name = "lean4export"
defaultTargets = ["lean4export", "Export"]
testDriver = "Test"

[[lean_lib]]
name = "Export"
globs = ["Export.*"]
defaultFacets = ["static"]

[[lean_lib]]
name = "Test"

[[lean_exe]]
name = "lean4export"
root = "Main"
supportInterpreter = true

where I have added "Export" to defaultTargets, globs = ["Export.*"], and defaultFacets = ["static"].

continuing with steps 2-4 we manage to compile comparator:

$ lake build
warning: lean4export: repository '/home/niklash/Projects/comparator/.lake/packages/lean4export' has local changes
Build completed successfully (18 jobs).

As Lake supports (to some extent) having dependencies distributed in a system-wide/read-only manner, I think the question here is: do we want to force the downstream users to have a writable copy of lean4export or should we try to support distributing lean4export in a way that is useful to more downstream users?

I have run into this problem with other libraries (like md4lean, verso) before but this is the first time I thought I should start a discussion in an issue. I totally respect a decision to close this as a non-issue -- as this is right now only an issue that I seem to be facing.

Hopefully I haven't wasted your time and apologize if I have!

[xhalo32]

A less contrived example to use a prebuilt lean4export, which avoids having to manipulate lean4export under .lake/packages, would be to provide it to comparator via lake's --packages option (this is what the nix build uses internally) or through package-overrides.json. This is what I was referring to with "lake supports to some extent having dependencies distributed in a system-wide/read-only manner."

I don't know if this feature of lake is used by any other project than nixpkgs at the moment. A quick GitHub search didn't result in any hits.

[nomeata]

Thats helpful. Note that a package can have multiple targets, and just running lake build builds only the default target. So it's not at all surprising that that does not pre build “everything”, and some rebuilding has to happen downstream.

So the question should more likely be: is there a way (conceptually and actually) to do lake build everything for reliable rebuilding? But I assume not, as downstream packages can add more facets.

So I'd conclude that read only directories in .lake are simply wrong.

Maybe packaging that tries to provide pre built artifacts should rather use lake's new local artifict cache functionality?

In any case, @tydeu may have more insight.

[xhalo32]

Thanks for the reply! You raise a good point with multiple targets, so my suggestion to add Export to defaultTargets is probably not the way to go. I investigated if comparator's lakefile could specify the target of lean4export instead and noticed that providing defaultTargets = ["Export"] in the [[require]] section is one way to do this.

I definitely making dependencies in .lake read-only is wrong, but lake treats dependencies provided through --packages pretty much the same way as those in .lake, and these might be installed into a read-only location. I hope dependency injection with lake would not have to rely on write access to the provided dependency, but right now adding the globs and defaultFacets seems like the best-effort alternative to me.

I wasn't aware of the new local artifact cache, thanks for mentioning it!

[tydeu]

@nomeata is generally right here. However, I am a little confused by the module structure of this project. Is it intentional that lake build only builds Export and not Export.Parse? Given Lean's usual module naming conventions, I would have expected the code in Export to be a module named something like Export.Dump and the root Export to import both Export.Dump and Export.Parse. If that were the case, a lake build Export:static would do everything @xhalo32 wanted.