Stream: Coq devs & plugin devs

Topic: dune build spending its time running coqdep


view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 09:02):

I'm wondering why, when I call dune build coq-stdlib.install after modifying a single .v file (not changing any dependency), I see a long list of coqdep calls. Is this something expected? Is it solved in one of the upcoming PRs?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 20 2021 at 11:00):

Can you write down the concrete reproduction here?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 20 2021 at 11:00):

This is not expected, coqdep should be called only on the .v file that has been changed.

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 11:21):

Well, compile coq with make -f Makefile.dune world, touch theories/Classes/CRelationClasses.v, make again

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 11:23):

Yep, it seems to entirely invalidate all the .v.d's when I touch a file

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

Thanks a lot @Matthieu Sozeau , I'm looking into it; dune version?

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

Oh I see, that is expected, I am not sure if we can do better. Let me explain: the current dune setup for coqdep is that each coqdep call does depend on all the .v files in the theory.

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:37):

2.8.5

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

This is because coqdep requires all .v files to be in place, otherwise if they are not [for example not generated], then it will complain the file is not there; this is used to resolve ambigous paths by coqdep

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

So the rule is:

{all .v files in a theory} --[coqdep]--> file.v.d

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

but actually coqdep only cares about the file being there, not about the contents.

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:38):

It is as much "there" before and after I touch it...

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:39):

But yeah I understand that to allow ambiguous Imports you need such a rule

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

I am not sure this can be expressed in dune easily, but we could tweak that; there are two other solutions to the problem:

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

By the way the example you provided doesn't trigger the rebuild

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:40):

I guess a single call would be quite fast, especially if it only does stat

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

touch is not enough, dune needs to see some actual change in the hash of the file

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:40):

Ok, sure

view this post on Zulip Matthieu Sozeau (Apr 20 2021 at 16:41):

I usually rebuild because I changed something of course :)

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

Ok, so I think the change on coqdep handling in 2.9 will solve that problem.

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

coqdep will be called but only once

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

as of now yes, unfortunately the coqdep setup is not very optimized

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

even in the regular build it is costing 10-30 seconds compared to the 2.9 solution

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

I didn't optimize it yet as even with this problem the dune build is usually faster

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

using -trace-file show how big the problem is.

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 09:25):

Yeah, I can guess on things like mathcomp, fiat or the stdlib this would be really time-consuming

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 09:27):

Another question about dune: with the new HoTT lib being installable alongside the stdlib, I'm trying to adapt Equations' build to have everything compiled only once. However that requires that I build Equations/theories/HoTT with different coq arguments (-noinit -indices-matter) than theories/Prop for example. I tried using (coq_flags ("-noinit")) in theories/HoTT/dune to override the flags in theories/dune but this didn't work. Is this scenario supported yet? (I just exclude the HoTT dir in the dune build for now)

view this post on Zulip Ali Caglayan (Apr 21 2021 at 09:30):

Does it work the other way round with having -noinit everywhere and then loading the library when you are in Prop?

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 09:33):

Hmm, possibly.

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 09:34):

But what about indices-matter? I don't want to force that in Prop and Type

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 09:35):

While you're around Ali, would you mind changing the coq-hott.dev extra-dev opam package to use the new build system?

view this post on Zulip Ali Caglayan (Apr 21 2021 at 12:30):

Matthieu Sozeau said:

While you're around Ali, would you mind changing the coq-hott.dev extra-dev opam package to use the new build system?

Is this necessary to do at the moment? Switching to dune is on my todo list but there are a few things that need to be done first. I thought that this wouldn't matter for opam?

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:05):

No I just mean using coq_makefile, I don't think the coq-hott.dev package was updated, but I might be wrong

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:07):

Indeed, right now it still installs hoqtop etc...

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

@Matthieu Sozeau what is your dune file in theories/HoTT , you likely need to add a dune file there (with (name Equations.Hott), but if you have a dune file in the parent with a recursive (include_subdirs) , then you need to tell it to stop. Not the cleanest way, maybe move it to a different directory?

view this post on Zulip Ali Caglayan (Apr 21 2021 at 13:13):

Ah I understand now. We are still working on switching to using coq_makefile for our dev builds, so it doesn't make sense to change the dev package yet.

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:13):

I tried using a dune file in theories/HoTT. Right now in theories/dune I added (dirs ("Prop" "Type")) so that the HoTT dir is ignored

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:16):

(after an (include_subdirs qualified))

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

Try first moving theories/HoTT to theories-hott/HoTT for example, and see if that works; if that works satisfactorly, then should be able to remove your (dirs ...) stanza an use instead (include_subdirs no) in the HoTT/dune file, but that maybe is not too good as it will stop the parent theory but will disable further recursion.

There are two things missing to have better control for this: a) per_file flags, so you could just do (flags Hott/* -foo) and better control of recursion for subdirectories.

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

(dirs...) will completely remove the HoTT subdir so you won't be able to see it at all

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:21):

Yep, not great

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:21):

Couldn't I have a dune in theories/ and one in each of theories/Prop, theories/Type and theories/HoTT?

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

It is still not clear to me how to handle "nested" theories, OCaml has nothing like that so no prior there.

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

Couldn't I have a dune in theories/ and one in each of theories/Prop, theories/Type and theories/HoTT?

Seems too much? Types / Prop are common right? I'd just place the HoTT stuff outside of the main tree for now so it has it's dune file and actually can declare the dep to coq-hott in the future

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:31):

Prop and Type are actually completely separate, like HoTT

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

Then you could do try that, doing (include subdirs no) in the theories/dune file indeed.

view this post on Zulip Matthieu Sozeau (Apr 21 2021 at 13:44):

Indeed, I think I managed to make it work!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2021 at 20:31):

Good to hear @Matthieu Sozeau , don't hesitate to submit suggestions for improvements to the dune issue tracker.


Last updated: Oct 16 2021 at 09:07 UTC