I'm using make -f Makefile.dune test-suite
and I'm experiencing a weird behavior. It first did run signalling 1 test failure. I've edited the test and run the command again. It's recompiling the whole stdlib before running the tests again, and it is running all of them (but I guess this is normal since everything changed).
Actually it should not do that, unless something in (package coq)
changed
you can check the build log to see what it did happen
but usually, I can re-run the test-suite
target and things work OK
I also have a version of the test suite rules that only re-run tests that are needed, but needs a newer dune as it uses (cram
stanza in a few places
but it test-suite
rebuilt the whole stdlib it means that the hash of coqc / plugins changed
Here the log of the the second run: https://gist.github.com/gares/2c04fd921b6e4ff555e66512b0002151
What I did is:
git worktree add ../xxx xxx
cd ../xxx
codium plugins/ssr/ssrelim.v test-suite/ssr/nothing_to_inject.v
make -f Makefile.dune test-suite
codium test-suite/ssr/nothing_to_inject.v
make -f Makefile.dune test-suite
No, I did just edit the .v file
Umm, it is re-running configure
which makes a full build due to the changed timestamp [once we can use dune-build info this spurious rebuild won't happen]
Actually it seems it recompiled everything, not just the stdlib
However it is bizarre that configure
is re-run, as the deps shouldn't change
(deps
%{project_root}/configure.ml
%{project_root}/dev/ocamldebug-coq.run
%{project_root}/dev/header.c
; Needed to generate include lists for coq_makefile
(source_tree %{project_root}/plugins)
(env_var COQ_CONFIGURE_PREFIX))
Aha, it is due to your change in plugins
:(
we have this rule source_tree plugins
as configure needs to scan the plugins to create some include variables
so yes this is a pitfall of the current setup, if you edit something in plugins
configure gets called again
there are two choices to fix this:
however it is bizarre that a .v
file is in plugins ?
I've opened an issue: https://github.com/coq/coq/issues/12750
I guess I did touch the .ml (and not the .v test as I thought), but the problem is still there
I've no preference for the chosen solution. I don't even know what "some include variables" is. How does the standard makefile solve the same problem (whatever the problem is)?
Note that just touching the file won't re-trigger, you need to change the hash
The makefile setup doesn't have this problem as it never auto-calls configure
A workaround is actually you calling configure manually
if dune sees the user called configure it won't call it manually, but yeah, that's a workaround; a fix should be done
Emilio Jesús Gallego Arias said:
The makefile setup doesn't have this problem as it never auto-calls configure
You did not explain why you need to scan plugins
[that's the (mode fallback)
bit, means "only run configure if coq_config is not there"]
That's this piece of code @Enrico Tassi
let plugins =
try Sys.readdir "plugins"
with _ -> [||]
in
Array.sort compare plugins;
Array.iter
(fun f ->
let f' = "plugins/"^f in
if Sys.is_directory f' && f.[0] <> '.' then pr " %S;\n" f')
plugins;
pr "]\n";
pr "\nlet all_src_dirs = core_src_dirs @ plugins_dirs\n";
I see but that is not going to change output if you edit a file. I guess it is the date thing, which is also something you have to hack around for reproducibility. What I don't get is why the date would be different. IIRC coq prints barely the month.
Yes, that's the date, see the call to unix.time
Oh, we store a second precise date and we round it up at print time?
Maybe we should round it up at configure time and make dune happy
Oh I see, we keep both: date and full_date
It seems it is only used for meessages like coqtop -v or coqide's welcome message. I vote for ditching the full_date altogether, or at least have a configure option (used by dune) to put 0 in place of anything more precise than the month.
We could also refine the deps of the rule
so it only depends on the dirs, not on the contents
as of today I'd suggest just to do like in make and call configure manually to avoid this problem
I don't think It is a viable solution. I edit a file and I've to know if I need to call configure or no (which files did I touch exactly, and which are the offending dirs)?
in make you have to call configure only if you add a plugin, here you would need to run it whenever you touch a file in there
Enrico Tassi said:
in make you have to call configure only if you add a plugin, here you would need to run it whenever you touch a file in there
Not sure I understand, if you call configure manually dune will disable the configure rule so you are in the same exact situation as in make.
Ah ok, I have to run it only once. I did not get that. It seems a useful workaround. I'm wondering why ./configure is not invoked by Makefile.dune in the first place then.
Enrico Tassi said:
Ah ok, I have to run it only once. I did not get that. It seems a useful workaround. I'm wondering why ./configure is not invoked by Makefile.dune in the first place then.
Having dune call configure if the user didn't is useful as to make things work out of the box for tooling that uses dune. Promotion rules are designed by this exact use case "let the user override some files" Opam will call it manually for example.
But anyways we will fix this bug soon I think.
Last updated: Oct 13 2024 at 01:02 UTC