Stream: Dune devs & users

Topic: Should COQPATH invalidate caches

Paolo Giarrusso (Apr 30 2021 at 21:10):

As per subject... I've done some quick testing and it doesn't seem to. My testing was about building packages in CI, so I tried to install package 1 into a special folder, and build package 2 with COQPATH, but I seemed to notice that package 1 wasn't rebuilt after setting the COQPATH, installs and uninstalls... and I'm not sure what should have happened and if this was unsound

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:14):

Yes, Dune's Coq mode doesn't know about things installed publicily yet, and that includes coqpath; this is fixed in the compose branch tho so no need to report a bug

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:15):

generally tho, I feel that COQPATH will only affect the set of libraries that are detected, but not sure how strict we should be here

Paolo Giarrusso (Apr 30 2021 at 21:16):

okay — but compose is for 3.0 I assume?

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

we lack any metadata for now to detect what should be done on a COQPATH change; same for libs that are installed publicly

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

for 2.9, scheduled mid-may

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

in fact we are only doing 2.9 to finish Coq stuff

Paolo Giarrusso (Apr 30 2021 at 21:16):

uuuuuuuh cool!

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

3.0 will arrive in september with way deeper changes

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

but the compose thing has proven tricky indeed due to the fact that currently we throw at dune user-contrib + whatever is in COQPATH

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

as "installed libs"

Paolo Giarrusso (Apr 30 2021 at 21:17):

if it's coming I won't waste your time with the challenges (I know a bit)

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

but there is close to zero metadata here, and even worse coqdep won't behave the same

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

so what is the best policy for that, I dunno

Paolo Giarrusso (Apr 30 2021 at 21:17):

especially if mid-may is a more reliable timeline

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:18):

I'm hoping, last thing I have to do before going on much needed holidays

Paolo Giarrusso (Apr 30 2021 at 21:18):

sympathies :-)

Paolo Giarrusso (Apr 30 2021 at 21:19):

but since I was working on dunifying our build, I might take that into account

Paolo Giarrusso (Apr 30 2021 at 21:20):

I guess I can focus on a compositional build, and delay any hacks to split the builds

Paolo Giarrusso (Apr 30 2021 at 21:21):

on your questions, I guess it might be hard for dune to detect changes to what's global (COQPATH/installed libs)

Paolo Giarrusso (Apr 30 2021 at 21:22):

so if I want to build in CI package P1, then dependent package P2, and do caching, I shouldn't install P1 yet

Paolo Giarrusso (Apr 30 2021 at 21:22):

I'd better slap those packages together and be done

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:25):

Yeah, tho we could track the hashes of the stuff in the global path the same way we do for ocaml

Emilio Jesús Gallego Arias (Apr 30 2021 at 21:26):

I just need to massage coqdep a bit more which is challenging as this is the trickiest part of the rules ; moreover Coq will by default import _all_ of user-contrib into scope; we could not do this but it would break compat with every project

Last updated: Oct 12 2024 at 13:01 UTC