Stream: Coq devs & plugin devs

Topic: dune and test-suite


view this post on Zulip Enrico Tassi (Jul 24 2020 at 13:54):

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).

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:00):

Actually it should not do that, unless something in (package coq) changed

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:00):

you can check the build log to see what it did happen

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:00):

but usually, I can re-run the test-suite target and things work OK

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:01):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:02):

but it test-suite rebuilt the whole stdlib it means that the hash of coqc / plugins changed

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:07):

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

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:08):

No, I did just edit the .v file

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:09):

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]

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:09):

Actually it seems it recompiled everything, not just the stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:09):

However it is bizarre that configure is re-run, as the deps shouldn't change

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:09):

(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))

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:10):

Aha, it is due to your change in plugins

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:10):

:(

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:10):

we have this rule source_tree plugins

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:10):

as configure needs to scan the plugins to create some include variables

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:11):

so yes this is a pitfall of the current setup, if you edit something in plugins configure gets called again

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:11):

there are two choices to fix this:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:12):

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:12):

however it is bizarre that a .v file is in plugins ?

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:14):

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

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:15):

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)?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:16):

Note that just touching the file won't re-trigger, you need to change the hash

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:16):

The makefile setup doesn't have this problem as it never auto-calls configure

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:16):

A workaround is actually you calling configure manually

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:17):

if dune sees the user called configure it won't call it manually, but yeah, that's a workaround; a fix should be done

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:18):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:18):

[that's the (mode fallback) bit, means "only run configure if coq_config is not there"]

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:18):

That's this piece of code @Enrico Tassi

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:18):


view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:18):

  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";

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:22):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:23):

Yes, that's the date, see the call to unix.time

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:24):

Oh, we store a second precise date and we round it up at print time?

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:24):

Maybe we should round it up at configure time and make dune happy

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:26):

Oh I see, we keep both: date and full_date

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:29):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:36):

We could also refine the deps of the rule

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:37):

so it only depends on the dirs, not on the contents

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 14:37):

as of today I'd suggest just to do like in make and call configure manually to avoid this problem

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:45):

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)?

view this post on Zulip Enrico Tassi (Jul 24 2020 at 14:46):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 17:14):

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.

view this post on Zulip Enrico Tassi (Jul 24 2020 at 17:17):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 17:19):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 17:20):

But anyways we will fix this bug soon I think.


Last updated: Oct 21 2021 at 21:03 UTC