Matthieu Sozeau (Apr 20 2021 at 09:02): 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?
Emilio Jesús Gallego Arias (Apr 20 2021 at 11:00):Can you write down the concrete reproduction here?
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.
Matthieu Sozeau (Apr 20 2021 at 11:21):Well, compile coq with make -f Makefile.dune world, touch theories/Classes/CRelationClasses.v, make again
Matthieu Sozeau (Apr 20 2021 at 11:23):Yep, it seems to entirely invalidate all the .v.d's when I touch a file
Emilio Jesús Gallego Arias (Apr 20 2021 at 16:34):Thanks a lot @Matthieu Sozeau , I'm looking into it; dune version?
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.
Matthieu Sozeau (Apr 20 2021 at 16:37):2.8.5
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
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
but actually coqdep only cares about the file being there, not about the contents.
Matthieu Sozeau (Apr 20 2021 at 16:38):It is as much "there" before and after I touch it...
Matthieu Sozeau (Apr 20 2021 at 16:39):But yeah I understand that to allow ambiguous Imports you need such a rule
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:
-modules flag for coqdep that has been proposed, this way coqdep for foo.v doesn't need to have all files in place in the first place. Emilio Jesús Gallego Arias (Apr 20 2021 at 16:40):By the way the example you provided doesn't trigger the rebuild
Matthieu Sozeau (Apr 20 2021 at 16:40):I guess a single call would be quite fast, especially if it only does stat
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
Matthieu Sozeau (Apr 20 2021 at 16:40):Ok, sure
Matthieu Sozeau (Apr 20 2021 at 16:41):I usually rebuild because I changed something of course :)
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.
Emilio Jesús Gallego Arias (Apr 20 2021 at 16:41):coqdep will be called but only once
Emilio Jesús Gallego Arias (Apr 20 2021 at 16:42):as of now yes, unfortunately the coqdep setup is not very optimized
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
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
Emilio Jesús Gallego Arias (Apr 20 2021 at 16:42):using -trace-file show how big the problem is.
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
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)
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?
Matthieu Sozeau (Apr 21 2021 at 09:33):Hmm, possibly.
Matthieu Sozeau (Apr 21 2021 at 09:34):But what about indices-matter? I don't want to force that in Prop and Type
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?
Ali Caglayan (Apr 21 2021 at 12:30):Matthieu Sozeau said:
While you're around Ali, would you mind changing the
coq-hott.devextra-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?
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
Matthieu Sozeau (Apr 21 2021 at 13:07):Indeed, right now it still installs hoqtop etc...
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?
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.
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
Matthieu Sozeau (Apr 21 2021 at 13:16):(after an (include_subdirs qualified))
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.
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
Matthieu Sozeau (Apr 21 2021 at 13:21):Yep, not great
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?
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.
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
Matthieu Sozeau (Apr 21 2021 at 13:31):Prop and Type are actually completely separate, like HoTT
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.
Matthieu Sozeau (Apr 21 2021 at 13:44):Indeed, I think I managed to make it work!
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.
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?
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
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
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
Emilio Jesús Gallego Arias (Nov 05 2021 at 11:54):one is related to coqdep indeed:
coqdep -modules [see issues from other users] so that we can run coqdep without having to put all source files in place, the way it works is like in OCaml, dune reads the module information, and it resolves the deps at rule generation time as it already has a database of modules 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
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
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
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...
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
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
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
Gaëtan Gilbert (Nov 05 2021 at 13:30):https://github.com/ocaml/dune/issues/5100
Emilio Jesús Gallego Arias (Nov 05 2021 at 13:32):Merci @Gaëtan Gilbert
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?
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
Emilio Jesús Gallego Arias (Nov 05 2021 at 14:33):coqdep in this case just outputs (dep (from Foo) (Bar))
Emilio Jesús Gallego Arias (Nov 05 2021 at 14:33):that's the whole point of -modules
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?
Emilio Jesús Gallego Arias (Nov 05 2021 at 14:36):Require only deals with vo files
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.
Emilio Jesús Gallego Arias (Nov 05 2021 at 14:38):Indeed, it just deals with the syntax
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
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?
Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):Nope @Paolo Giarrusso
Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):indeed this should be the default until we have -modules
Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):I have a branch which was already working
Emilio Jesús Gallego Arias (Nov 05 2021 at 19:40):mentioning it so people don't spend time
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
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