Dune support

[ejgallego]

Hi folks,

the Coq mode for Dune is getting more mature, and a big blocker now is integration with Proof General. I am unsure how to best approach this; basically PG should add the right flags to make libraries compiled in _build into scope.

A possibility is indeed to let dune handle this; so PG could call dune coqtop foo.v and indeed coqtop would be started with the right settings. WDYT?

[cpitclaudel]

A possibility is indeed to let dune handle this; so PG could call dune coqtop foo.v and indeed coqtop would be started with the right settings. WDYT?

Sounds reasonable, but we'd need to be able to determine when dune is in use.

Could dune generate a _CoqProject file for us? In my projects I just write it by hand:

-R _build/default/coq/ Xyz
-Q _build/default/tests/ Tests
-Q _build/default/examples/ Examples
-R _build/default/examples/rv RV

Also, we need some indication of where each .v file came from, so that jump-to-definition can go to the right place.

[ejgallego]

Could dune generate a _CoqProject file for us?

It could, but I'm not sure I'm willing to do this; notably the _CoqProject format will have trouble keeping with Dune features; also it pollutes the source tree. Experience with generating .merlin files in OCaml indicates that this is a path we don't want to follow.

Also, we need some indication of where each .v file came from, so that jump-to-definition can go to the right place.

What do you concretely mean? If you use dune coqtop foo.v you would be using the right file already; otherwise you could implement something like tuareg does [it understands _build]

dune provides some APIs to query projects, but I guess I'd need to see the concrete use case. I'm not sure if this index functionality is something to have in PG, or instead PG should rely on an external too such as ocp-index for OCaml.

[ejgallego]

notably the _CoqProject format will have trouble keeping with Dune features

Yeah, already we cannot generate a _CoqProject that works for a simple case with two composed libraries, and those with different flags.

[cpitclaudel]

It could, but I'm not sure I'm willing to do this; notably the _CoqProject format will have trouble keeping with Dune features; also it pollutes the source tree. Experience with generating .merlin files in OCaml indicates that this is a path we don't want to follow.

OK. Then running dune coq sounds good. How do we detect dune projects reliably? Do we just search for dune-project files?

What do you concretely mean?

When I press M-. in company-coq it issues a Locate query for the current symbol. Then it uses Locate Library to find where the library came from. For example M-. on nat yields this:

<prompt>Coq < 17 || 0 < </prompt>Timeout 1 Locate nat.
Inductive Coq.Init.Datatypes.nat
<prompt>Coq < 19 || 0 < </prompt>Timeout 1 Locate Library Coq.Init.Datatypes.
Coq.Init.Datatypes has been loaded from file
/home/clement/.opam/default/lib/coq/theories/Init/Datatypes.vo

Then it jumps to the corresponding .v file: /home/clement/.opam/default/lib/coq/theories/Init/Datatypes.v

With dune this doesn't work: instead of going to the original .v file it jumps to the copy that dune made in _build. For OCaml merlin detects this. I need to detect it too in company-coq. So the question is: how do I find which original file a .v file in _build is a copy of?

(We discussed this on gitter a while ago:

@cpitclaudel
Hey @ejgallego, we've been using dune to build our latest Coq project, and it's working very nice. Thanks again!
There's one thing I need to tweak in company-coq for it to work perfectly, though: currently jump-to-definition goes to teh .v file in _build/default because that's where the .vo and .v file are. Do you have ideas on how company-coq could learn where the original .v file was?

@SkySkimmer
remove the _build/default prefix?

@cpitclaudel
Yes, but that feels a bit ah-hod, and IIUC dune doesn't always use that prefix.

@SkySkimmer
how does merlin do it? I know dune generates some .merlin files for it but don't know how it links the B and S lines together

@cpitclaudel
I don't know either :) But you're onto something. Maybe dune could generate a _CoqProject (I think it currently doesn't?) that would include the right info
Emilio Jesús Gallego Arias

@ejgallego
Yup merlin + dune is an open problem, upstream devs are working on it, it is a bit painful as you have to call dune at every check.
What I am thinking is to provide a dune info command that editors could use, given a file foo.v, dune info foo.v would provide:

• flags
• list of dependencies
• original location
  as indeed you are correct @cpitclaudel the location of the files is highly dependent on quite a few factors
  as for merlin, it will basically do something like that in the future, likely keeping a pipe open to dune, as it is expensive sometimes, think of the whole duniverse

@cpitclaudel
Very interesting, thanks a lot. But since Dune already generates a merlin file, could it not enhance that with extra info so that it doesn't have to be called each time? (this might be naive)
And in the Coq case, couldn't we put the relevant info in the _CoqProject?
I'm thinking something like a map file that would say where each .vo file came from

Emilio Jesús Gallego Arias
@ejgallego
@cpitclaudel both .merlin and _CoqProject have quite serious problems, for example they cannot do per-file flags, etc... So indeed Dune will stop generating .merlin files pretty soon I heard.

I'm thinking something like a map file that would sya where each .vo file came from

Yup, dune info should provide that, however I'm curious why do you need to find the information about the .vo files instead of the .v file, which is what the editor uses?

@cpitclaudel
To locate a symbol I do Locate xyz.and then Locate Library A.B.C, which points me to a .vo file

@ejgallego

To locate a symbol I do Locate xyz.and then Locate Library A.B.C, which points me to a .vo file

I see, indeed that's a bit tricky, as imagine A.vo is coming from a generated A.v file which is not in the source tree, I'll have a look how merlin does handle locate, but indeed we could provide a reverse-map

[ejgallego]

OK. Then running dune coq sounds good. How do we detect dune projects reliably? Do we just search for dune-project files?

That's the standard method, we could add a variable in case the user wants to override?

We discussed this on gitter a while ago

Oh yes I remember that, I thought it had happened in an issue but I couldn't locate it.

Actually OCaml has the same problem sometimes [you use M-. but it sends you to the _build dir] but tuareg got a hack for it; I'll have a look and discuss with dune / OCaml upstream to see what the plan regarding this is.

ocp-index seems to use a hack, see https://github.com/OCamlPro/ocp-index/blob/master/libs/indexBuild.ml#L276

Actually that doesn't bother me too much; for now the large majority of users will be satisfied by that; we could add a locate-build-prefix var for projects that use a special prefix.

The medium term plan is to have something similar to the LSP protocol locate call; still the relation between the lsp-server and the build tool has not been fully determined tho.

[Matafou]

Isn't it the dune file that we want to detect here? dune-project is not necessary is it?
Be careful, we use the _CoqProject informations for other actions than just launching coqtop.
For instanceIt is used by "auto-compilation on Require" (which detects if dependencies of a file needs recompilation and preforms it), and by company-coq as already remarked. @cpitclaudel how many other of your features need the _CoqProject infos?

So if we accept dune project files we need to either parse it or be able to query dune for several things.

[cpitclaudel]

@cpitclaudel how many other of your features need the _CoqProject infos?

It's not so much that company-coq needs _CoqProject; it's that dune copies source files into a separate directory, so it adds extra work to find out where things came from.

Maybe dune could add a comment at the end of the file, or something. Or maybe it could have a command to figure out where a file came from.

[Matafou]

OK and no other feature of company-coq needs the compile-options?

[cpitclaudel]

Everything is queried through Coq, so they do need the options, but indirectly ^^

[ejgallego]

Note that dune coqtop foo.v will update the dependencies of foo.v automatically, as it does for the OCaml version. It will also set the right flags for foo.v.

[erikmd]

@ejgallego IIUC you suggest that the main place from PG codebase where coqtop is called to run the REPL, we should replace for example (if I open a file from ValidSDP library) the command:

coqtop -topfile …/validsdp/theories/validsdp.v -emacs -I …/validsdp/plugins/soswitness/src -R …/validsdp/plugins/soswitness/theories ValidSDP -R …/validsdp/plugins/soswitness/src ValidSDP -R …/validsdp/plugins/soswitness/test-suite ValidSDP -R …/validsdp/test-suite ValidSDP -R …/validsdp/theories ValidSDP

with just dune coqtop -topfile …/validsdp/theories/validsdp.v -emacs ?

If yes, would this work as well with dune coqidetop …? (to be able to use Coq's XML protocol)

[ejgallego]

Not even -topfile should be needed IMO, but indeed yes, dune knows how to compute the flags and includes for a particular file so IMO it is better not to duplicate that logic in emacs; the same could be applied to coqidetop, good suggestion indeed!

[erikmd]

BTW I have the same question as
@Matafou

Isn't it the dune file that we want to detect here? dune-project is not necessary is it?

also we may want to detect if dune itself is in the path.

anyway correct me if I'm wrong, but it seems we'll also need to keep _CoqProject support functional (say, as a fallback if the dune binary and project file is not found)

[ejgallego]

dune-project indicates the root, IMHO it is better to issue locate-dominating-file buffer-file-name for dune-project and assume that's the root of the project. dune files can appear in many subdirs but are really small pieces.

I guess it boils down to whether you want to do dune coqtop theories/foo.v or cd theories && dune coqtop foo.v

I tend to prefer working from the root; keep in mind that dune coqtop foo.v would compile foo's deps, so IMHO reported paths in case of errors would look more natural.

Keeping _CoqProject is fine, whether a project wants to support both build systems is IMHO down to them.

Regarding locate I suggest we follow fow now the "hack" approach as done in ocp-index ; the issue is being discussed upstream so it seems to me that waiting to see what happens there may be sensible vs rolling our own complex solution.

[cpitclaudel]

dune-project indicates the root, IMHO it is better to issue locate-dominating-file buffer-file-name for dune-project and assume that's the root of the project. dune files can appear in many subdirs but are really small pieces.

That sounds good, though we should use default-directory, not buffer-file-name. Also, this will break for some projects using dune, so we should be careful to add a setting to disable it (my Coq projects using dune have multiple libraries depending on each other, and these dependencies are captured in a _CoqProject but not in a dune file. Maybe the latest changes make that unnecessary?

I guess it boils down to whether you want to do dune coqtop theories/foo.v or cd theories && dune coqtop foo.v

Note that doing the former will change the way commands producing files behave, I think (not necessarily a bad thing, just pointing it out).

Keeping _CoqProject is fine, whether a project wants to support both build systems is IMHO down to them.

I think it's also that we want to support projects with just one of these systems.

[ejgallego]

the way commands producing files behave

What commands? If you mean extraction that will be fixed in Coq itself soon.

my Coq projects using dune have multiple libraries depending on each other, and these dependencies are captured in a _CoqProject but not in a dune file. Maybe the latest changes make that unnecessary?

There is limited composition support already in dune master, I'm planning to add full support soon. Do you have an example of such projects? I would be great to check the current implementation covers your use case.

[cpitclaudel]

What commands? If you mean extraction that will be fixed in Coq itself soon.

Yep, Extraction, as well as graph-dumping commands and other debugging commands that write a file. The "obvious" fix would be to make all these commands print the path of the file they just created (some of them already do). Not a big deal.

There is limited composition support already in dune master

😍

Do you have an example of such projects? I would be great to check the current implementation covers your use case.

Yes! Our PLDI20 paper :) We'll release it on Github in just a few days ^^ I can send you a tarball if you want?

[ejgallego]

Yep, Extraction, as well as graph-dumping commands and other debugging commands that write a file. The "obvious" fix would be to make all these commands print the path of the file they just created (some of them already do). Not a big deal.

Actually I'm reworking any command that produces a file so it has to go thru a standard API, that should solve these problems which indeed are annoying. LSP-Coq will forbid all these stuff [except maybe for extraction] and have commands provide output by the protocol.

Yes! Our PLDI20 paper :) We'll release it on Github in just a few days ^^ I can send you a tarball if you want?

Thanks! I can wait for the github release, no worries.

[hendriktews]

Note that dune coqtop foo.v will update the dependencies of foo.v automatically

Hi, this is very interesting to read. I have the following
questions wrt dependencies:

1. Does this also work when the user interactively adds or changes dependencies of foo.v?
2. Or when the file foo.v has not yet been created?
3. Presumably one can configure whether -vos is used for the dependencies or not. Can this also be configured without writing dune-project files?
4. Is there a mode, where it first uses -vos and, when ready, starts updating all .vo files on a subset of the available cores?

[ejgallego]

• Does this also work when the user interactively adds or changes dependencies of foo.v?

It would be easy to use watch mode so when the file is saved additional dependencies are picked up; more fine-grained interaction would require a protocol with dune which I'd rather defer to a later stage of development.

2. Or when the file foo.v has not yet been created?

What to do in this case is an open question; dune does know that foo.v belongs to a library, however coqdep will return no deps so nothing will be compiled. There are many approximations that could be interesting. I think for now an empty file should trigger no rebuild.

3. Presumably one can configure whether -vos is used for the dependencies or not. Can this also be configured without writing dune-project files?

4. Is there a mode, where it first uses -vos and, when ready, starts updating all .vo files on a subset of the available cores?

Not as of today, but we may add support for it in the future. As long as you can write reasonable build rules for that should be easy to add to dune.

Myself I'm not very interested in vos as it doesn't produce a sound build in general, and it is not properly incremental.

[ejgallego]

Not as of today, but we may add support for it in the future. As long as you can write reasonable build rules for that should be easy to add to dune.

Myself I'm not very interested in vos as it doesn't produce a sound build in general, and it is not properly incremental.

While I don't plan to work on this right now I'd strongly encourage for people interested to open an issue in ocaml/dune and try to contribute. IMHO, adding vos support would be a very nice first contribution to Dune for someone willing to learn more about it.

Basically you'd need to figure out the right build rules and write them down using Dune's OCaml-based rule language.

[hendriktews]

@ejgallego Thanks for your quick answers! From the answers I would conclude, that currently dune cannot support the auto compilation feature of Proof General. Because there, we need support for interactively adding/changing require commands.

vos [...] doesn't produce a sound build

My plan for this is to add a compilation mode to Proof General, where first -vos is used and then, with a suitable delay after -vos finished, start a normal .vo compilation in the background. This way, one can quickly proceed and sees any potential errors relatively soon. I've been using this for -quick/-vio2vo for quite a while.

it is not properly incremental.

With this you mean, that a .vos cannot be converted into a .vo?

[ejgallego]

Because there, we need support for interactively adding/changing require commands.

I guess it depends how you want to look at it, currently dune has all capabilities to indeed provide compilation support, it is more a matter of the interface to access them I think.

My plan for this is to add a compilation mode to Proof General

Note that replicating Coq's build system in PG is going to be costly in terms of work, as for example dune provides more and more features including composition.

With this you mean, that a .vos cannot be converted into a .vo?

Not only that, but .vo generated that way are not guaranteed to be sound in general.

By incremental I mean more of a true incremental compiliation, that is to say, only recheck proofs that need rechecking, not a file-based approach.

[hendriktews]

currently dune has all capabilities to indeed provide compilation support

Yes, but there are important features missing and there is the general problem, that dune cannot deduce dependencies, before the file has been saved. I am not sure, if it is desirable to save a file when Proof General processes a require command.

Note that replicating Coq's build system in PG is going to be costly in terms of work

Well, Proof General's support for compiling Coq projects exists already since 2011, so it is not that we are paying the effort now, which would indeed be questionable.

[ejgallego]

Yes, but there are important features missing and there is the general problem, that dune cannot deduce dependencies, before the file has been saved. I am not sure, if it is desirable to save a file when Proof General processes a require command.

This is due to the interface being this way, but can send the file to stdout or save in /tmp and run the dep checker; not a big issue, except if of course you want to embed coqdep in the editor and avoid the process round trip; but that has limitations as you will have to keep up.

Well, Proof General's support for compiling Coq projects exists already since 2011, so it is not that we are paying the effort now, which would indeed be questionable.

Things for simple projects will still continue to work, however quite a few of new features are being added now so the PG code will need updating if we intend to support such projects.

[lthms]

As certain of my projects grows in complexity, the need for a “dune support” in PG increases. Is there a way to help here to see this issue moving forward?

[vzaliva]

What is the status of this? If there is a workaround? We are attempting to switch a sizeable Coq project to Dune, and M-. jumping to files under _build is not going to work for us. People will end up editing files in _build by mistake, and their changes will not be pushed to git.

[cpitclaudel]

People will end up editing files in _build by mistake

I think Dune makes these files read-only now, so you realize the issue quickly. Still I agree it would be nice to have this. There's no general solution AFAIK, but we should probably just implement a hack at this point. I won't have time to work on it soon though (I'm defending my thesis in a week), so someone would have to write the (ELisp) code.

[vzaliva]

@cpitclaudel good luck with your defense! Do we have a consensus on how this "hack" should work? Maybe you can explain the general idea and we can see if somebody else can help...

[cpitclaudel]

Thanks! My guess is that the algorithm is, roughly:

1. Find file defining symbol under point — this company-coq already does.
2. Check (locate-dominating-file with a predicate) whether the file we found is in a _build directory
3. If no, return the file as before
4. If yes, search for the same file within the parent directory of _build; if it exists open that, otherwise show a warning message.

In step 2 we could also look for a dune project file. In step 4 what I mean is that …/_build/default/x/y/z.v becomes …/x/y/z.v.

[Matafou]

Let me check I understand: We don't implement dune support immediately. We just hack something so that dune does not make PG open the wrong files. Is that it? If yes then this needs a fake _coqProject in sync with dune. Right?

Let me try to sum up what we need to really support dune and check what seems solved:

• detect dune files. easy.
• compile dependencies of a file via dune. easy.
• auto-translate file "_build/anyprofile/a/b/c.v" into "./a/b/c.v". easy.
• retrieve dependencies of a file to "lock" corresponding buffers. easy?

Anything else? Do we have a solution for the last point.

[cpitclaudel]

Let me check I understand: We don't implement dune support immediately. We just hack something so that dune does not make PG open the wrong files.

Right

If yes then this needs a fake _coqProject in sync with dune. Right?

Also right.

retrieve dependencies of a file to "lock" corresponding buffers. easy?

I don't use the locking feature, and I'm not sure it's worth maintaining. I often develop generic lemmas or tactics while working on an example, and copy them as I make progress into an appropriate library file that the current file depends on. Locking just gets in the way of that.

Anything else?

I don't really use auto-compilation either, so for me the important point is really the third one; I don't have too many thoughts on the other points. I've resisted doing anything on this because it's bad to accumulate hacks in PG, but since we don't have a solution currently on the dune side, I think we should go ahead with a minimal number of hacks.

[Matafou]

I don't use the locking feature, and I'm not sure it's worth maintaining. I often develop generic lemmas or tactics while working on an example, and copy them as I make progress into an appropriate library file that the current file depends on. Locking just gets in the way of that.

I use it most of the time. It helps me maintain a consistency between files. It is sometimes a bit annoying to recompile files when I know nothing will break, but with vso mode + "don't check proof" mode I basically am happy.
Admittedly breaking this may not be to much of a problem. Still I think people are used to it.

I don't really use auto-compilation either, so for me the important point is really the third one;

auto-compilation is extremely nice. IMHO it is the best feature of PG. vos mode is definitely the

[monnier]

1. Find file defining symbol under point — this company-coq already does. 2. Check (`locate-dominating-file` with a predicate) whether the file we found is in a `_build` directory

Maybe a regexp match for "/_build/" is sufficient? Stefan

[cpitclaudel]

Admittedly breaking this may not be to much of a problem.

I'm not suggesting breaking it, just not fixing it yet (it's already broken by dune, right?)

Maybe a regexp match for "/_build/" is sufficient?

/_build/[^/]+/ really, since thre is a second layer of nesting in _build, but yes, I guess that would work.

[hendriktews]

What function does M-. runs for you? For me it is xref-find-definitions, which asks for a TAGS file. If the TAGS file is right, it would never switch into a wrong directory.

[cpitclaudel]

What function does M-. runs for you?

The M-. part of this discussion is about company-coq, which queries Coq dynamically to locate symbols.

[hendriktews]

@cpitclaudel Please only answer after your defence!
If dune copies the files around, shouldn't it have a function that translates a copied filename back to the original file name? Wouldn't it be cleaner to pipe the location you get from Coq through that dune back-translation function?

[cpitclaudel]

If dune copies the files around, shouldn't it have a function that translates a copied filename back to the original file name?

It should, and I wish it did. but AFAIK it doesn't at the moment, and the issue has been with us for long enough that I now think worth a hack ^^

Please only answer after your defence!

(Sorry, couldn't resist. Take care.)

[ejgallego]

tuareg just strips the _build part from filesnames, it is a hack but so far it has worked well [until dune rpc is more usable I guess]

[Matafou]

By the way @ejgallego does dune rename coq modules as it does for ML modules with the dune__exe__ prefix? Isn't that also a source of hacks somewhere in merlin or tuareg?

[ejgallego]

@Matafou not that I know of yet, that's mostly for object files tho so it is hard to observe.

[Matafou]

@Matafou not that I know of yet, that's mostly for object files tho so it is hard to observe.

Indeed the ML module names are correct error messages. Does it mean dune performs on-the-fly translation of names on error messages?

[MackieLoeffel]

Based on the suggestions above, I am currently using the following hack to make M-. in company-coq go to the correct file:

  (defun company-coq-library-path-strip-build-advice (res)
    ;; (message "company-coq-library-path returned %S" res)
    (let ((filtered (replace-regexp-in-string "_build/default" "" res nil 'literal)))
      (if (file-exists-p filtered)
          filtered
        res
        )))
  (advice-add 'company-coq-library-path :filter-return #'company-coq-library-path-strip-build-advice)

This simple heuristic seems to work so far for my use cases but I don't know how robust it is.

[Matafou]

Thanks! We will try something similar.

[cpitclaudel]

@MackieLoeffel LGTM, do you want to make it into a PR in company-coq?

[MackieLoeffel]

Done in cpitclaudel/company-coq#257

[rlepigre]

Now that support for coqtop is available in dune (since version 3.1.0), I'm wondering how we should move forward on the PG side. I'm definitely not the right person for the job, since I'm hopeless with Emacs.

Roughly, what needs to be done to have reasonable support is (I think) the following:

1. Detect the presence of a dune workspace (its root contains a dune-project file), fallback to normal behaviour if there is none.
2. Decide whether we want to run coqtop via dune, not sure how. Maybe only do it if there is no _CoqProject file?
3. Running the Coq toplevel with command dune coq top <file> -- -emacs, where file is a path to the Coq source file. Ideally, the command would be run from the root of the dune workspace, with a relative path to the file. (There are some issues with absolute paths and symbolic links in dune, so using an absolute path is not ideal even if it works in most cases.)
4. Enable some hacks to improve usability, like what @MackieLoeffel proposed here to enable jump-to-definition in the original source file (not its copy under dune's _build directory).

[ejgallego]

Thanks for all the work @rlepigre , a few comments:

1 and 2: Indeed there are some heuristics to guess that, usually locate-dominating-file helps. Also, dune has several commands that may help, and a RPC protocol which is more fancy and can provide config à la merlin.

I guess a good start would be to find a project root (using locate-dominating-file) and start from there.

For 3. we have a bug in dune, once we fix it, it should work to run dune coq top from any point, but indeed I guess PG may enjoy knowing the root.

For 4. I'd just copy what tuareg does, a very simple but effective hack: if the file starts with _build, strip the prefix 😆