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.

view this post on Zulip Enrico Tassi (Nov 05 2021 at 10:19):

@Emilio Jesús Gallego Arias I'm on dune 2.9.0 and Coq master and I still see this behavior (I touch theories/ssr/ssrbool.v) and it rebuilds all .d files. Wasn't 2.9 expected to solve this problem?

view this post on Zulip Gaëtan Gilbert (Nov 05 2021 at 10:54):

https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/too.20much.20coqdep

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:31):

Didn't have time to push the optimization to 2.9 such that a single coqdep call is done, sorry

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:52):

I am not sure how to document best known issues / todo with dune + ccoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:54):

one is related to coqdep indeed:

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:54):

This requires adding a bit of the loadpath logic to Dune, not a big deal IMHO, but that's the reason the work we are trying to do to make loadpath self-contained is important, so we can just vendor it in Dune and be in sync

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:55):

Part 3 requires a lot of manpower, so I don't see myself solving it alone

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:55):

For now only workaround is to user make for the vo files, I wonder how sound the rule is

view this post on Zulip Enrico Tassi (Nov 05 2021 at 12:22):

I don't follow. The problem is not that it is called once per file, but rather that it is called for all files, even if only one was modified (in the sources, even if all sources are copied to _build). This seems to be the bug. Then of course things can be optimized other ways...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 13:14):

This is because coqdep needs all files to be present, so the rule for calling coqdep is all_source_files >> coqdep file

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 13:14):

all_source_files depends on the _hash_ of all source files, not on its existance

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 13:14):

IIUC Dune doesn't have a notion to depend only on the existance of a file, we could add that, but it seems better to just try to implement -modules which is superior

view this post on Zulip Gaëtan Gilbert (Nov 05 2021 at 13:30):

https://github.com/ocaml/dune/issues/5100

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 13:32):

Merci @Gaëtan Gilbert

view this post on Zulip Guillaume Melquiond (Nov 05 2021 at 14:30):

I don't understand how -module will help with non-existent files. If coqdep parses From Foo Require Bar and dune did not put the file Qux/Baz/Bar.v into scope, how is coqdep supposed to guess that the module is Foo.Qux.Baz.Bar?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:32):

@Guillaume Melquiond coqdep won't guess anything, that is resolved by dune who knows all modules including generated ones

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:33):

coqdep in this case just outputs (dep (from Foo) (Bar))

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:33):

that's the whole point of -modules

view this post on Zulip Karl Palmskog (Nov 05 2021 at 14:33):

so you will have knowledge of all Coq modules, even generated fromModule declarations, and their relations to files?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:36):

Require only deals with vo files

view this post on Zulip Guillaume Melquiond (Nov 05 2021 at 14:37):

At this point, why do you even need coqdep? It seems like a simple sed script would work just fine, if coqdep is meant to output Require lines almost verbatim.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:38):

Indeed, it just deals with the syntax

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 14:38):

already today it is basically a lex script + the resolution code which will soon live into its own lib

view this post on Zulip Paolo Giarrusso (Nov 05 2021 at 19:26):

But to be sure, none of this is a blocker for doing the single coqdep call, right?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):

Nope @Paolo Giarrusso

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):

indeed this should be the default until we have -modules

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):

I have a branch which was already working

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):

mentioning it so people don't spend time

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):

I'm just too busy to get some time to polish it , write the tests and merge

view this post on Zulip Paolo Giarrusso (Nov 05 2021 at 19:41):

I can’t OCaml, but any way somebody else can finish it up?


Last updated: Jun 09 2023 at 08:01 UTC