Compositional Coq builds depend on the current root

[Blaisorblade]

Expected Behavior

Build Coq dune project inner (stdpp) with caching enabled. Then place it inside project outer (iris), then build using outer as root. The code should not be rebuilt.

EDIT: this is important when sharing caches between builds of stdpp and compositional builds of stdpp + iris.

Actual Behavior

When using composition, and the root is outer, the code is built using paths relative to outer, not to outer/inner. That changes the command line and defeats caching.

Here's an example. Running from iris/stdpp with --root .:

Running[2]: (cd _build/default && /Users/pgiarrusso1/.opam/4.14.0+trunk/bin/coqc -q -w -deprecated-hint-rewrite-without-locality -w -deprecated-typeclasses-transparency-without-locality -w -deprecated-syntactic-definition -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R theories stdpp theories/options.v)
cache store success [442fc78b0dbcffaf142efd215cc5a689]

Running from iris with --root .

Running[2]: (cd _build/default && /Users/pgiarrusso1/.opam/4.14.0+trunk/bin/coqc -q -w -deprecated-hint-rewrite-without-locality -w -deprecated-typeclasses-transparency-without-locality -w -deprecated-syntactic-definition -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R theories stdpp theories/options.v)
cache store success [574d71dfc706ac57a5cf8f1f619fd297]

Changing current directory before the build step would fix this cache miss.

Workaround

Create a dummy folder for the outer project even to build only the inner project.

Reproduction

• PR with a reproducing test:

1. 1. 1.

Specifications

• Version of dune (output of dune --version): dune 3.4.0
• Version of ocaml (output of ocamlc --version)
• Operating system (distribution and version):

[rgrinberg]

Unfortunately this PR breaks the locations printed by coqc as we can see in the tests.

[Blaisorblade]

TLDR: IIUC, proper caching compositional builds require changes to reported locations — and those might not be trivial.

But we shouldn't confuse the issue with my fix.

1. Do we agree there's an issue? AFAICT, this seems a serious problem with compositional builds; I can elaborate.

2. If we accept this issue is valid, the current directory when running coqc must be a fixed location inside the project, not the workspace; the project root would be a better choice. That still leaves some ambiguity, but we shouldn't fix that by running coqc from the project root or by passing info that would invalidate the cache.

For human readers, we could have dune add messages with the missing info. If IDEs decode Coq locations today (not sure!), that might not be enough, but I'm not sure what protocol they assume; regardless, for now we could have coqc could print absolute paths (at least optionally). Long-term, LSP might enable other options.

[Blaisorblade]

For discussion on the long-term solution I've opened https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/Error.20messages.2C.20locations.20and.20paths.

[Alizter]

Part of the problem is that we run coqc at the root rather than relative to the file. We could experiment with running coqc relative to the file. I did some experimentation with this when porting the Coq test-suite to Dune, and it seems to work OK. It would probably screw up extraction however.

This would however make the reported locations unhelpful, so I guess we could go down the route of OCaml and lex the error messages and correct the locations.

[Blaisorblade]

@Alizter that's what I tried in #6006; my attempt is naive, but it doesn't seem enough yet.

[Alizter]

@Blaisorblade ah ok! IIANM OCaml does something similar and lexes and modifies the messages. We could set up something similar for Coq, it shouldn't be too difficult, just tedious. @rgrinberg could confirm if this is worth doing.

[Blaisorblade]

@Alizter What I meant is that the MR doesn't fix caching yet — I don't see how to fix this while still using Command.run as-is. I'd worry about that before dealing with locations.

BTW, instead of running relative to the file, it might make more sense to run relative to the project...

=== There's also a separate problem: if library B depends on library A, using different locations for library A will still defeat caching if the cache key includes the command line. Concretely, if the cache includes the command line, dune will consider coqc -R path1 A and coqc -R path2 A as different commands that cannot share cache entries, EDIT: which is too conservative.

[ejgallego]

After discussing a bit more with @Alizter , I think that is pretty tricky, not sure even if possible with the current API constraints Dune - Coq communication has.

Actually I think a better solution with the current tech we have is to actually make all developers use a workspace that does imitate a mono repos, as for example what we are tying to do with coq-universe.

I am developing some scripts to make that easier. So indeed, you create particular workspaces (for example, when I want to work on coq-lsp, I checkout coq, coq-lsp, serlib, maybe yojson, maybe some Coq libs for testing), all under stable paths.

[Blaisorblade]

not sure even if possible with the current API constraints Dune - Coq communication has.

FWIW: I'm not sure there's anything Coq-specific here — the problem is that when building root/foo/bar from foo, the hash changes if you start from root or from root/.. even if it does not need to — while dune already understands the path to the workspace doesn't matter. No idea how hard it'd be to enhance dune's engine for this; @rlepigre any idea?

[Blaisorblade]

hash changes if you start from root or from root/.. even if it does not need to — while dune already understands the path to the workspace doesn't matter.

I will note the hash must change if an input moves from ../baz to ../../baz (as highlighted in
https://github.com/coq/coq/issues/16571#issuecomment-1462573900), but this is not an exception to the rule: all that matters are the paths relative to foo, the build command's working directory — not paths relative to the workspace. (So the scenario in the link would still defeat caching as needed for soundness, and improving that might require additional thinking).