support dune build system? (duplicate of #477)

[Matafou]

Hi, this is an early warning, not yet a real bug, about the dune build system and its support in PG.

Coq dev team is about to switch to dune build system. Since dune is sometimes presented as the recommended build system for coq package and plugins, the number of users switching to it may increase.

Problem is: dune does not generate .vo{,s,k} in the same directories than sources but in a _build_vo directory.
Edit: Morevover it actually make a complete copy of the source files in a _build directory too.

@hendriktews for the record, I think the autocompilation feature will break if .vo are not in the same directory.
@cpitclaudel maybe some feature of company-coq depend on .vo location?

I have asked details about reproducing this compilation scheme by hand, will report here. We can use this thread to gather information about this problem. We may ask @ejgallego for details.

[ejgallego]

You could query dune for locations and stuff, but I think the easiest for tools such as PG would be to use the upcoming dune coqtop file.v command, that will run coqtop on the right environment for file, building deps, options, etc...

[Matafou]

Thx @ejgallego.

IFAIU Just calling dune coqtop Foo.v when we start scripting Foo.v is not sufficient for the autocompile feature: we trigger compilation each time we reach a Require because the .vo file may have become outdated any time during development (we may be working on the require module in another ide session).

When reaching Require Foo.Bar we need to trigger compilation of dune build Foo/Bar.vo, which means to be able to link Foo.Bar to Foo/Bar.v.

[cpitclaudel]

I've been using dune for personal projects for a while. One thing that it does break is jumping to the definition of an identifier: it goes to the copy of the .v file in _build/ instead of the original file. We discussed this months ago, but I don't think there was a real solution at the time?

[ejgallego]

What tuareg does for OCaml is indeed to special case this I understand and it removes the _build/default prefix.

Dune already provides some kind of protocol and RPC to handle this stuff, and I understand OCaml emacs stuff is using it so I dunno what would be the most convenient way.

[hendriktews]

@hendriktews for the record, I think the autocompilation feature will break if .vo are not in the same directory.

auto compilation uses coqdep output to locate vo files. This should hopefully just work when using the appropriate dune equivalent of coqdep. It then uses coq-library-{src,vos,vok}-of-vo-file to compute v, vos and vok file names from that. The current version of these functions just delete or append a few letters at the end.
If I understand Pierre correctly, with dune the directory that contains a vo file does not contain the corresponding v file. In this case strange things will happen without changing these coq-library functions.
In case the v file is in the same directory, auto compilation won't recompile, because it doesn't see that the real source file has been changed.

[Matafou]

@ejgallego's remark here suggests that we should some day have an autocompilation based on (dune) build system. It would indeed make things easier from our side I suppose, but it would force our users to have such a build system from the start. I don't know if it would be good or bad.

@hendriktews I think I remember that at some point the autocompilation could rely on the makefile if present. Is it still supported? Are you aware of the coq command Locate Library (I wasn't)?

[ejgallego]

Dune does indeed place .v and .vo files in the build dir, but note that for example auto-generated .v files will exist in the build dir but not in the source build.

I guess for dune + Coq, emacs could use the upcoming RPC support in dune to ask things about the build , IIUC RPC has been designed to be used from language servers, which do provide some extra functionality in terms of workspace management.

Dune uses regular coqc / coqdep tho, and other than placing all objects and sources under _build, the compilation step is standard. Tricky parts that dune does are:

• managing OCaml deps from Coq [so you get an integrated .v + plugins build]
• managing the composition of theories, so first, libraries in the local workspace are scanned, libraries installed are scanned, a database is build; then, build rules are generated for that concrete setup of N theories in scope and M theories globally installed, in such a way that substitution of theories works.

(*) ocaml/dune#3517

[hendriktews]

autocompilation based on (dune) build system.

It's not clear yet, how to get the dependencies from dune, such that these files can be locked in Proof General.

autocompilation could rely on the makefile if present.

That was in sequential foreground compilation. There it is still supported, without ancestor locking, of course.

Are you aware of the coq command Locate Library?

Probably not, but it doesn't sound unfamiliar either. Where would it be useful? Here it doesn't seem to find libraries that have not been compiled yet.

[Matafou]

Are you aware of the coq command Locate Library?
Probably not, but it doesn't sound unfamiliar either. Where would it be useful? Here it doesn't seem to find libraries that have not been compiled yet.

True, then it is of no use for us.

[Blaisorblade]

Maybe this issue should be closed as a duplicate of #477 (comment) (with links both ways) — the latest plans are there.

[Matafou]

Indeed thanks. This is a duplicate of #477.