Adding support for a "dune coq top" command

[rlepigre]

The plan for this MR is to add support for a dune coq top FILE -- ARGS command that, given a path to a Coq source file FILE in the workspace, invokes coqtop with the appropriate arguments (derived from the relevant dune files). The main motivation for this is to avoid having to manually maintain a _CoqProject file containing duplicate information (already contained in dune files), and to easily ensure that all dependencies of the file loaded in the Coq toplevel are up-to-date. This would greatly facilitate interaction with editors like Proof General (see ProofGeneral/PG#477).

The command should basically do three things:

• Find the dependencies (.vo files) upon which the argument file depend and build them.
• Figure out what flags would be used for that file by coqc and use them for coqtop.
• Invoke the Coq toplevel (coqtop -topfile FILE ...).

Other things to do:

• Figure out what should be done for generated .v files.
• Also provide a dune coq idetop --toplevel CMD option to support vscode, coqide (via --toplevel idetop), coqtail, ... (suggested by @gares).
• Figure out if we can support absolute paths better (problem with symbolic links reported by @MackieLoeffel). One possibility would be to use realpath, but not sure if dune has something like that.
• Figure out if we can provide an option to disable the building of dependencies (requested by @MackieLoeffel). Building deps is a problem in the case where you also use dune build -w. However, one has to be careful in cases where the toplevel command itself must be built.

CC @ejgallego @Blaisorblade @MackieLoeffel

[rlepigre]

Currently, running dune coq top FILE leads to the _build directory being initialised with all the source files, but no .vo files are produced. Any clue what might be going on?

[rgrinberg]

kind of done, but does not work yet

It was just a small issue with how we were evaluating the action. I pushed a fix.

[rlepigre]

It was just a small issue with how we were evaluating the action. I pushed a fix.

Great thanks! I'll try this out when I have a minute.

[ejgallego]

@rlepigre thanks a lot for your help, this is looking great and was a much much needed feature.

Let me know when / if this is ready for review and testing.

[rlepigre]

Let me know when / if this is ready for review and testing.

@ejgallego This is not quite ready yet, since I'm still missing the part that figures out what arguments to give to coqtop based on the dune stanzas. I kind of see how to get access to that information, but what I found seems way too complicated to be the right thing. Would you have time to talk about this sometime this week?

[ejgallego]

@ejgallego This is not quite ready yet, since I'm still missing the part that figures out what arguments to give to coqtop based on the dune stanzas. I kind of see how to get access to that information, but what I found seems way too complicated to be the right thing. Would you have time to talk about this sometime this week?

Sure, the arguments are not too hard to get tho, basically they come from two pieces of info:

• -Q / -I for the libraries used, this is done in coqc_file_flags, it requires you initialize the Coq_lib.DB.
• Arguments given in the flags field, this is coming from Context.coq_flags

So the tricky part is to organize code well, but you could start just by coping and paste setup rules and remove everything that doesn't return the arguments. But indeed don't hesitate to ping me for a quick visio towards the end of the week.

[ejgallego]

[you need to add a changelog too]

[rlepigre]

I have a first working version! Not sure at all this is the right way to do things, so I'd be great if you could review @ejgallego.

[MackieLoeffel]

I've tested this MR and it looks quite good already!

Could you add a flag to disable the rebuilding of dependencies? Currently, dune coq top cannot be used with dune build --watch as the two builds conflict.

In case it is useful, I've tested dune coq top by creating a file dune-coqtop with the following contents in PATH and setting coq-prog-name in Proof General to dune-coqtop.

#!/bin/sh

set -e

if [ ! -f "dune" ]; then
    opam exec -- coqtop "$@"
    exit 0
fi

if [ "x$1" = "x-help" ]; then
    opam exec -- coqtop -help
    exit 0
fi

if [ "x$1" != "x-topfile" ]; then
    echo "Expected -topfile as first argument!"
    exit 1
fi

TARGET_FILE="$2"
REL_FILE=$(realpath --relative-to="." "$TARGET_FILE")

opam exec -- <path to dune.exe> coq top "$REL_FILE" --display=short  -- -emacs

The realpath is necessary because dune coq top currently does not support absolute arguments.

[gares]

Also provide a dune coq idetop to support vscode, coqide, coqtail, ... (suggested by @gares).

To be precise, coqidetop is one toplevel used by these UIs today, but there are others (in development, or dead) with similar names, eg pidetop or vscoqtop. So maybe a dune coq top --toplevel=myname would be more appropriate (default myname=coqtop).

[MackieLoeffel]

The hack @rlepigre just pushed to support absolute paths does not seem to work for paths that include symlinks.

I also noticed that dune coq top recomputes too much. I.e. if I modify one file and then open another that depends on the first file, the first file is rebuilt as expected. However, if I then kill the *coq* buffer after the rebuilding has finished and then open the second file again, another rebuild is triggered. Any idea what could be going on there? I was only able to reproduce this in emacs using my dune-coqtop script from above, not on the command line.

[rlepigre]

Also provide a dune coq idetop to support vscode, coqide, coqtail, ... (suggested by @gares).

To be precise, coqidetop is one toplevel used by these UIs today, but there are others (in development, or dead) with similar names, eg pidetop or vscoqtop. So maybe a dune coq top --toplevel=myname would be more appropriate (default myname=coqtop).

Is it somewhat guaranteed that they take the same command line arguments? If yes, that seems to be a great solution.

[gares]

we try to enforce that coq specific ones are understood (via a public api to parse these) then I guess each toplevel may undertsand more, so extra arguments to the dune command should probably be passed along

[rlepigre]

we try to enforce that coq specific ones are understood (via a public api to parse these) then I guess each toplevel may undertsand more, so extra arguments to the dune command should probably be passed along

OK, that's already the case that extra arguments (after --) are passed along, so that's good.

Also, you can probably already do what you want (I think) redefining coqtop to be a custom command (say, a shell script coqtop.sh with something like the following in a dune file.

(env
 (dev
  (binaries (coqtop.sh as coqtop))
  (flags :standard))
 (release
  (binaries (coqtop.sh as coqtop))
  (flags :standard)))

We've used that trick with @MackieLoeffel to run coqc with perf in CI for RefinedC (see https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/dune).

[ejgallego]

Great, fantastic work @rlepigre ; I have added this to the top of my review queue, realistically that means next Wednesday, but I hope we can get this merged before the end of next week.

[rlepigre]

There are two last things to figure out before this is ready:

• understand why recompilation is too eager when you invoke dune from a sub-directory,
• understand why the reproducing test case for the above is completely broken.

@rgrinberg I'd greatly appreciate your input on the second point, since I get really weird results. I tried echoing $TESTCASE_ROOT and it seems to be always empty: is that normal?

File "test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t", line 1, characters 0-0:
diff --git a/_build/.sandbox/5e1ba220194a4e4da3629f58d2c405e2/default/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t b/_build/.sandbox/5e1ba220194a4e4da3629f58d2c405e2/default/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t.corrected
index ffbb01e3f..f853d35ca 100644
--- a/_build/.sandbox/5e1ba220194a4e4da3629f58d2c405e2/default/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t
+++ b/_build/.sandbox/5e1ba220194a4e4da3629f58d2c405e2/default/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t.corrected
@@ -27,9 +27,28 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune clean
   $ (cd dir && echo "TESTCASE_ROOT=$TESTCASE_ROOT" && dune coq top --display verbose --toplevel echo bar.v)
-        coqdep dir/bar.v.d
-        coqdep dir/foo.v.d
-          coqc dir/.foo.aux,dir/foo.{glob,vo}
-  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
+  TESTCASE_ROOT=
+  Shared cache: disabled
+  Workspace root:
+  $TESTCASE_ROOT/dir
+  Warning: No dune-project file has been found. A default one is assumed but
+  the project might break when dune is upgraded. Please create a dune-project
+  file.
+  Hint: generate the project file with: $ dune init project <name>
+  File "dune", line 1, characters 0-26:
+  1 | (coq.theory
+  2 |  (name basic))
+  Error: 'coq.theory' is available only when coq is enabled in the dune-project
+  file. You must enable it using (using coq 0.3) in your dune-project file.
+  [1]
   $ (cd dir && dune coq top --display short --toplevel echo bar.v)
-  -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
+  Warning: No dune-project file has been found. A default one is assumed but
+  the project might break when dune is upgraded. Please create a dune-project
+  file.
+  Hint: generate the project file with: $ dune init project <name>
+  File "dune", line 1, characters 0-26:
+  1 | (coq.theory
+  2 |  (name basic))
+  Error: 'coq.theory' is available only when coq is enabled in the dune-project
+  file. You must enable it using (using coq 0.3) in your dune-project file.
+  [1]

[ejgallego]

Thanks for the fix @rlepigre . Indeed I was suspecting that you were not taking the module prefix into account.

This is something we need to clean up, as a module name in Coq is really Foo.Bar.Moo.bar for example, but Coq_module.Name.t is only a component of the name. Moreover, we have some discrepancy on what Dune considers a Coq module, and what Coq does, as in dune we don't include the prefix given by the stanza, but really modules are not relocatable.

Yup, we need some cleanup here.

Actually I'm wondering why we don't keep a reverse map for path to stanza directly? But module is also fine as it includes the path.

[ejgallego]

• understand why recompilation is too eager when you invoke dune from a sub-directory,

Is that still the case after the revmap fix? If so, I'll have a look ASAP.

[rlepigre]

• understand why recompilation is too eager when you invoke dune from a sub-directory,

Is that still the case after the revmap fix? If so, I'll have a look ASAP.

Yes, that is still the case.

[rlepigre]

Actually I'm wondering why we don't keep a reverse map for path to stanza directly? But module is also fine as it includes the path.

That's a good point, I did not think of that! I'm inclined to keep things as they are though, especially if some refactoring around what Coq module are is planed. I agree the current situation is a bit confusing (I thought Coq module names would include the full path, which is why I thought a map from module names would be enough initially).

[ejgallego]

That's a good point, I did not think of that! I'm inclined to keep things as they are though, especially if some refactoring around what Coq module are is planed.

Sounds good then. It seems to me that once we fix the test we can merge! We are close!

I agree the current situation is a bit confusing (I thought Coq module names would include the full path, which is why I thought a map from module names would be enough initially).

Indeed, we initially followed the model that OCaml uses, but they are too different so as things are, they are confusing. I'd say we should not hold back to improve things if we want / see the opportunity, for example by making the name be the actual, canonical name [but that's tricky due to the way -Q etc... binding work sometimes]

[snowleopard]

That's indeed a tricky point; dropping the deps completely is gonna result in very broken stuff, as the .vo files may not ever be there. The only reasonable thing I can come up with if is Dune would allow to depend on a file being there, instead of their contents. That would be useful in some other scenarios, but AFAIK the build engine doesn't have that capability, correct @snowleopard @rgrinberg ) ?

The build engine does have a capability for ignoring contents -- see the goal primitive:

dune/src/dune_engine/action_builder0.mli

Lines 70 to 74 in 4bc7629

	(** [goal t] ignores all facts that have been accumulated about the dependencies
	of [t]. For example, [goal (path p)] declares that a path [p] contributes to
	the "goal" of the resulting action builder, which means [p] must be built,
	but the contents of [p] is irrelevant. *)
	val goal : 'a t -> 'a t

It is used for implementing aliases, for example, and we've been also discussing to use it for supporting so-called "order-only dependencies" (#5514).

Of course, one can easily shoot oneself in the foot by ignoring the contents of dependencies. But you guys know Coq, so maybe you can prove something about the correctness :-)

[ejgallego]

Thanks a lot @snowleopard !

Coq's need for that are actually stemming from a deeper problem with coqdep that would better be solved by actually implementing -modules. That's planned, but it is gonna take a while I guess.

Meanwhile, the main use case is due to coqdep depending on the layout of the Coq theories as to implement module resolution; so indeed, we want to re-run coqdep only when the directory layout has changed, not the files themselves.ç

So a proof could be directly by construction by having a type that represents only the layout of the FS as input to coqdep.

How well goal can work for the other use case (don't rebuild if already present) I'm a bit skeptical, as Coq doesn't like that [for safety reasons it uses internal hashes to avoid .vo file injection].

[ejgallego]

@rlepigre ha indeed that's a bug in dune, in fact, if you apply #5544 the rebuild problem is fixed.

Indeed the db was not saved after exec'ing.

I did the test using:

  $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)

What do you think of doing that? Maybe dune coq top should adjust the input path to the root, so the test is:

  $ (cd dir && dune coq top --root .. --display short --toplevel echo bar.v)

[rlepigre]

Thanks @ejgallego! I think you're right about adjusting the path to the root. I don't have time to look into that right now, but I rebased and the example (and CI) should be fixed. If you want to have a look into changing that yourself feel free to do so.

[ejgallego]

Thanks @ejgallego! I think you're right about adjusting the path to the root. I don't have time to look into that right now, but I rebased and the example (and CI) should be fixed. If you want to have a look into changing that yourself feel free to do so.

Great, thanks @rlepigre ! I will have a look, but if the CI is fine we can merge this and keep improving later on.

I am not sure about the policy w.r.t. commit squashing, what do you prefer? @rgrinberg what's the dune standard here?

[ejgallego]

Looks great to me; may need a few tweaks on usability but IMHO it is merge time, these can be done later on.

[ejgallego]

After looking at the commits, I think I prefer a squash, especially as some of the commits leave the test suite broken so bisect could not work well.

Are you ok with that @rlepigre ? (I can do the squash myself from the GitHub interface)

[rlepigre]

Fine withe me, the history was indeed horrible. I squashed into a single commit.

[ejgallego]

🎉 🎉 🎉 🎉 🎉

I took the freedom to tweet about this https://twitter.com/ejgallego/status/1511782302896070669

[rgrinberg]

what's the dune standard here?

I prefer squashing unless the commits have value on their own.