Stream: Dune devs & users

Topic: Should COQPATH invalidate caches


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:16):

okay — but compose is for 3.0 I assume?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

for 2.9, scheduled mid-may

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

in fact we are only doing 2.9 to finish Coq stuff

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:16):

uuuuuuuh cool!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:16):

3.0 will arrive in september with way deeper changes

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

as "installed libs"

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 21:17):

so what is the best policy for that, I dunno

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:17):

especially if mid-may is a more reliable timeline

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:18):

sympathies :-)

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:19):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 30 2021 at 21:22):

I'd better slap those packages together and be done

view this post on Zulip 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

view this post on Zulip 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 16 2021 at 09:07 UTC