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?
Can you write down the concrete reproduction here?
This is not expected, coqdep should be called only on the .v
file that has been changed.
Well, compile coq with make -f Makefile.dune world
, touch theories/Classes/CRelationClasses.v
, make
again
Yep, it seems to entirely invalidate all the .v.d's when I touch a file
Thanks a lot @Matthieu Sozeau , I'm looking into it; dune version?
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.
2.8.5
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
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.
It is as much "there" before and after I touch it...
But yeah I understand that to allow ambiguous Imports you need such a rule
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.By the way the example you provided doesn't trigger the rebuild
I guess a single call would be quite fast, especially if it only does stat
touch is not enough, dune needs to see some actual change in the hash of the file
Ok, sure
I usually rebuild because I changed something of course :)
Ok, so I think the change on coqdep handling in 2.9 will solve that problem.
coqdep will be called but only once
as of now yes, unfortunately the coqdep setup is not very optimized
even in the regular build it is costing 10-30 seconds compared to the 2.9 solution
I didn't optimize it yet as even with this problem the dune build is usually faster
using -trace-file
show how big the problem is.
Yeah, I can guess on things like mathcomp, fiat or the stdlib this would be really time-consuming
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)
Does it work the other way round with having -noinit
everywhere and then loading the library when you are in Prop
?
Hmm, possibly.
But what about indices-matter
? I don't want to force that in Prop
and Type
While you're around Ali, would you mind changing the coq-hott.dev
extra-dev opam package to use the new build system?
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?
No I just mean using coq_makefile
, I don't think the coq-hott.dev
package was updated, but I might be wrong
Indeed, right now it still installs hoqtop etc...
@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?
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.
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
(after an (include_subdirs qualified)
)
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.
(dirs...)
will completely remove the HoTT
subdir so you won't be able to see it at all
Yep, not great
Couldn't I have a dune in theories/ and one in each of theories/Prop, theories/Type and theories/HoTT?
It is still not clear to me how to handle "nested" theories, OCaml has nothing like that so no prior there.
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
Prop and Type are actually completely separate, like HoTT
Then you could do try that, doing (include subdirs no)
in the theories/dune
file indeed.
Indeed, I think I managed to make it work!
Good to hear @Matthieu Sozeau , don't hesitate to submit suggestions for improvements to the dune issue tracker.
@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?
https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/too.20much.20coqdep
Didn't have time to push the optimization to 2.9 such that a single coqdep call is done, sorry
I am not sure how to document best known issues / todo with dune + ccoq
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 modulesThis 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
Part 3 requires a lot of manpower, so I don't see myself solving it alone
For now only workaround is to user make for the vo files, I wonder how sound the rule is
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...
This is because coqdep needs all files to be present, so the rule for calling coqdep is all_source_files >> coqdep file
all_source_files
depends on the _hash_ of all source files, not on its existance
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
https://github.com/ocaml/dune/issues/5100
Merci @Gaëtan Gilbert
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
?
@Guillaume Melquiond coqdep won't guess anything, that is resolved by dune who knows all modules including generated ones
coqdep in this case just outputs (dep (from Foo) (Bar))
that's the whole point of -modules
so you will have knowledge of all Coq modules, even generated fromModule
declarations, and their relations to files?
Require only deals with vo files
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.
Indeed, it just deals with the syntax
already today it is basically a lex script + the resolution code which will soon live into its own lib
But to be sure, none of this is a blocker for doing the single coqdep call, right?
Nope @Paolo Giarrusso
indeed this should be the default until we have -modules
I have a branch which was already working
mentioning it so people don't spend time
I'm just too busy to get some time to polish it , write the tests and merge
I can’t OCaml, but any way somebody else can finish it up?
Last updated: Jun 09 2023 at 08:01 UTC