Dune and coq_makefile parity · Dune devs & users

Stream: Dune devs & users

Topic: Dune and coq_makefile parity

Karl Palmskog (Feb 21 2022 at 12:13):

Ali asked me to summarize the features that Dune are lacking compared to coq_makefile, so here they are.

The most important issues for using Dune for building Coq projects are:

Backward compatibility is not guaranteed (future Dune releases may not be able to build old Coq projects). Dune-for-OCaml has guaranteed backward compatibility for some time.
You can't express project-local dependencies via(theories X) and at the same time allow those dependencies to be installed into Coq's user-contrib. So you have to choose mutually exclusively between composable local builds of projects with many dune files and installability via opam.
Still no proper support for _CoqProject+Dune+ProofGeneral (due to Dune file hygiene, ProofGeneral doesn't find .vo files built by Dune)

Karl Palmskog (Feb 21 2022 at 12:15):

other issues that are not as important:

there is to my knowledge no way to know the Coq version inside a Dune configuration file
you can't use Coq's Load command to input some other files inside a Coq file and then build a release with Dune, Dune's hygiene will remove the file you are loading
no way to support .vio/.vos/.vok compilation with Dune
no easy way to build coqdoc / Alectryon with Dune
no support for explicit extraction of multiple files (e.g., you might have to enumerate 50+ OCaml modules when extracting from Coq to OCaml)

Karl Palmskog (Feb 21 2022 at 12:16):

I can give specific examples (specific projects where this is a problem) for each of these issues. But please ask if you want that.

Ali Caglayan (Feb 21 2022 at 12:17):

cc @Rudi Grinberg

Karl Palmskog (Feb 21 2022 at 12:22):

I also don't know what the status is with Dune vs. native compilation across Coq 8.11 to Coq 8.15. For example, it seems Erik felt the need to write this script to run before Dune compilation, which looks very hacky: https://github.com/math-comp/multinomials/blob/master/configure

Karl Palmskog (Feb 21 2022 at 12:25):

see this issue for discussion of some of the issues above: https://github.com/coq-community/manifesto/issues/87

Ali Caglayan (Feb 21 2022 at 12:26):

There used to be a native-compiler option to coq IIRC, but now there is a dedicated binary coqnative and the option is deprecated. Support for the dedicated coqnative for dune seems to be stuck here: https://github.com/ocaml/dune/pull/4750

Karl Palmskog (Feb 21 2022 at 12:27):

I guess I can also mention this nice-to-have feature I already reported as a Dune issue, on running coqchk via Dune as is done with make validate via coq_makefile: https://github.com/ocaml/dune/issues/2197

Ali Caglayan (Feb 21 2022 at 12:28):

I have a solution for that using dune 3.0:

;; Rule for validation -- For dune 3.0
(rule (alias validate)
  (deps (glob_files_rec ./*.vo))
  (action (run coqchk -R . YourProjectHere %{deps} -o))
)

Ali Caglayan (Feb 21 2022 at 12:29):

glob_files_rec has nothing to do with Coq glob btw, just lets you recursively go through folders

Karl Palmskog (Feb 21 2022 at 12:31):

but that's not incremental, right?

Karl Palmskog (Feb 21 2022 at 12:32):

anyway, I think there should be an official stanza so everybody doesn't have to add it locally...

Ali Caglayan (Feb 21 2022 at 12:32):

No, coqchk would require some deeper changes unrelated to dune in order to incrementally work. At the moment, this just copies the coq_makefile validate rule and sticks all files into coqchk

Karl Palmskog (Feb 21 2022 at 12:36):

I think we have to distinguish two kinds of incremental coqchk:

the "fully incremental" approach that doesn't even check Coq's stdlib twice. This is currently out of reach.
a "partially incremental" approach that keeps track of what files in the local project have been checked so far, and hooks into Dune's checksumming of edited files.

In the second approach, you could for example add file.v.coqchk to keep track of that it has been checked by coqchk, and each partially incremental build will update these files.

Ali Caglayan (Feb 21 2022 at 12:36):

But then our documentation says that coqchk A B can be done as coqchk A && coqchk B -admit so perhaps an incremental build is possible. The only issue is that coqchk doesn't actually build anything.

Rodolphe Lepigre (Feb 21 2022 at 13:22):

FYI I'm currently looking into proper editor support for dune (see https://github.com/ocaml/dune/pull/5457).

Karl Palmskog (Feb 21 2022 at 13:38):

here is some discussion on Dune in ProofGeneral: https://github.com/ProofGeneral/PG/issues/573

Karl Palmskog (Feb 21 2022 at 13:39):

also, I have no idea about Dune in VsCoq or Coqtail/Vim or CoqIDE

Paolo Giarrusso (Feb 21 2022 at 13:48):

We’d need to use dune coqtop in vscoq etc as well, but I hope that’s easier.

Paolo Giarrusso (Feb 21 2022 at 13:53):

Re “incremental coqchk”, last I tried it seemed that running it on one file vs many files takes more or less the same since dependencies take long to check, so “always rerun from scratch on everything” is much faster than running separately on each file. Either way, “feature parity” seems more urgent than optimizations here…

Karl Palmskog (Feb 21 2022 at 14:02):

well, the problem for vo production vs. coqchk is more or less the same as for vio production vs. vio checking. Checking of an existing .vio doesn't produce anything, it just terminates with an error or without an error. Nearly the same as with .vos and .vok.

Ali Caglayan (Feb 21 2022 at 14:44):

VSCoq and CoqIDE both use coqidetop (xml protocol)

Rodolphe Lepigre (Feb 21 2022 at 14:45):

Yeah, @Enrico Tassi suggested to generalize what I am doing to also provide a dune coq idetop command, and that should not be a problem.

Ali Caglayan (Feb 21 2022 at 14:45):

Also what is with the dune coq X seperation? I thought it would be more intuitive to have dune coqX?

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:09):

Thanks a lot @Karl Palmskog , do we have a good place to add that info?

Karl Palmskog (Feb 21 2022 at 15:12):

if you tell me where I should add it on GitHub, I can do that. For example, I could report the top issues separately, and you could create a meta-issue (in the Dune repo on GitHub)

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

Maybe that interesting comparsion could live in the wiki?

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

I think you know better than I do

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:15):

issues would be great too

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:15):

we will do a dune hacking event and there is a bit of manpower

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:15):

I don't want to talk too loud, but after two complex years it seems we are getting some momentum back in terms of development and collaboration

Karl Palmskog (Feb 21 2022 at 15:16):

maybe @Rudi Grinberg can advise how he would prefer to track the most important issues on Coq+Dune

Rodolphe Lepigre (Feb 21 2022 at 15:58):

Ali Caglayan said:

Also what is with the dune coq X seperation? I thought it would be more intuitive to have dune coqX?

See https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Dune.20internals.3A.20build.20a.20target.20.60--only-deps.60/near/272285294

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:59):

Indeed it was decided to group dune ocaml etc ... commands in subcommands

Rudi Grinberg (Feb 21 2022 at 16:18):

Karl Palmskog said:

maybe Rudi Grinberg can advise how he would prefer to track the most important issues on Coq+Dune

You guys can use the projects functionality or just stick to issues/labels/milestones. If you need any additional permissions on the dune repo to do this, just ask. It is very helpful for me to see the priorities however, as I know very little about the coq project and can only guess what is important.

Karl Palmskog (Feb 21 2022 at 16:23):

OK, then I will go ahead and create separate issues for both the important and not-so-important needed features in the Dune GitHub repo (unless there is a already a similar issue)

Karl Palmskog (Feb 21 2022 at 16:24):

then I think one could add an issue label like: coq-critical

Karl Palmskog (Feb 21 2022 at 16:26):

one could argue that the IDE support question is not strictly Dune's problem, but for tracking it may be useful nevertheless

Rudi Grinberg (Feb 21 2022 at 16:30):

Karl Palmskog said:

Ali asked me to summarize the features that Dune are lacking compared to coq_makefile, so here they are.

The most important issues for using Dune for building Coq projects are:

Backward compatibility is not guaranteed (future Dune releases may not be able to build old Coq projects). Dune-for-OCaml has guaranteed backward compatibility for some time.

You can't express project-local dependencies via(theories X) and at the same time allow those dependencies to be installed into Coq's user-contrib. So you have to choose mutually exclusively between composable local builds of projects with many dune files and installability via opam.

Still no proper support for _CoqProject+Dune+ProofGeneral (due to Dune file hygiene, ProofGeneral doesn't find .vo files built by Dune)

Thanks for starting this thread. I'll address things by point as well:

This one is the easiest to address and doesn't need an issue. Once Emilio deems things stable, we can start preserving backwards compat. Dune has all the infrastructure necessary for this already
Installing theories and reading them are actually separate issues. Do we also want dune to understand theories installed with makefiles? IMO, we should just copy dune's concepts of lazy loading & library resolution wholesale. Those things are already performant, well understood, and most importantly by far the easiest to implement.
This one is tricky and needs a little more description. How flexible is PG in changes that would make it easier to work with dune?

Karl Palmskog (Feb 21 2022 at 16:32):

Do we also want dune to understand theories installed with makefiles?

If Dune assumes everything else is installed by Dune, we can't realistically migrate piecewise to Dune. Many people will want to use non-Dune build systems for Coq forever. To have any chance to convert people to use Dune, they need the flexibility to mix Dune-installed and coq_makefile-installed Coq packages.

Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

It is not hard to support the legacy install scheme

Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

would be a bit hacky as dune would have to infer what packages are installed from the coqpath contents

Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

but that's doable IMHO

Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

having that would mean 1.0 support

Rudi Grinberg (Feb 21 2022 at 16:37):

Karl Palmskog said:

other issues that are not as important:

there is to my knowledge no way to know the Coq version inside a Dune configuration file

you can't use Coq's Load command to input some other files inside a Coq file and then build a release with Dune, Dune's hygiene will remove the file you are loading

no way to support .vio/.vos/.vok compilation with Dune

no easy way to build coqdoc / Alectryon with Dune

no support for explicit extraction of multiple files (e.g., you might have to enumerate 50+ OCaml modules when extracting from Coq to OCaml)

Is there a way to obtain the version of coq without building & running coq itself? Otherwise, we get into some nasty circular dependency issues when coq itself is in the workspace. By the way, on the whole I suggest not to use versions to signal capabilities if at all possible. IMO it's much better if coq could tell dune what features it supports. For example, whether it supports interface files or not.
Isn't this a coqdep issue? Coqdep should see Load and add an appropriate dep.
I looked into this earlier, and my conclusion was that coq's cli makes this needlessly difficult. I'd like to see good documentation for this stuff and possibly a simplified scheme from the coq side.
Since we've added directory targets, we can add such rules. But we will not be able to install all the doc artifacts yet .
This should be easy to fix now. I'll look into it.

Karl Palmskog (Feb 21 2022 at 16:40):

on the whole I suggest not to use versions to signal capabilities if at all possible.

Unfortunately, nearly everything with respect to Coq capabilities are signaled via versions. There would have to be some new signal mechanism being introduced into Coq for this to go away (not likely)

Karl Palmskog (Feb 21 2022 at 16:42):

Isn't this a coqdep issue? Coqdep should see Load and add an appropriate dep.

Emilio can confirm, but I don't think coqdep is capable of getting the file names out of a Load command (it could be a raw string like ../../stuff/foobar.txt)

Rodolphe Lepigre (Feb 21 2022 at 16:45):

Rudi Grinberg said:

Karl Palmskog said:

Still no proper support for _CoqProject+Dune+ProofGeneral (due to Dune file hygiene, ProofGeneral doesn't find .vo files built by Dune)

This one is tricky and needs a little more description. How flexible is PG in changes that would make it easier to work with dune?

For PG the adaptations are pretty simple, and I don't expect it would be too difficult to upstream changes. Basically, two things are needed:

setting the coqtop command that is running when we detect that the project uses dune to build Coq (maybe this requires a kind of user flag?),
strip _build/default from paths when using "jump to definition" or the likes.

For the first point, we cannot simply tweak PG variables since it insists on overwriting configurations (though we managed to hack something by tweaking hooks as a temporary solution). For the later, there is already a prototype here: https://github.com/cpitclaudel/company-coq/pull/257, including a link to discussions.

Ali Caglayan (Feb 21 2022 at 16:47):

Rudi Grinberg said:

Karl Palmskog said:

Still no proper support for _CoqProject+Dune+ProofGeneral (due to Dune file hygiene, ProofGeneral doesn't find .vo files built by Dune)

This one is tricky and needs a little more description. How flexible is PG in changes that would make it easier to work with dune?

I assume that the dune file will replace the _CoqProject file. It would be possible to generate a _CoqProject with dune, but I don't think it would be very useful since it would end up in _build. This means that all IDEs would have to search in _build. In which case they might as well understand dune files.

Enrico Tassi (Feb 21 2022 at 16:47):

Is there a documented way to "signal capabilities"?
Also, some of these may be enabled/disabled at configure time, how can one get these without running the binary?

Enrico Tassi (Feb 21 2022 at 16:50):

Or alternatively, is there an example to follow?

Rodolphe Lepigre (Feb 21 2022 at 16:50):

Ali Caglayan said:

I assume that the dune file will replace the _CoqProject file. It would be possible to generate a _CoqProject with dune, but I don't think it would be very useful since it would end up in _build. This means that all IDEs would have to search in _build. In which case they might as well understand dune files.

As I see things, _CoqProject would not be needed any more, and I would not be too sad about that.

Enrico Tassi (Feb 21 2022 at 16:53):

If it is dune which starts coq*top, then I don't think these is any need for generating the _CoqProject file.

Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

I think in Dune 3.0 we can indeed query coqc for capabilities

Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

the rule setup is dynamic enought, as long as the theory Database doesn't depend on it

Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

that's the main eager bit

Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

[file_contents seems fine to me and that'd be the trickiest point]

Rudi Grinberg (Feb 21 2022 at 17:27):

Enrico Tassi said:

Is there a documented way to "signal capabilities"?
Also, some of these may be enabled/disabled at configure time, how can one get these without running the binary?

If they could be written to coqc --configure that would be a good start. To do this without running the binary, dune would need to peek into some configure file.

But as Emilio said, there's no technical problem with running binaries when generating rules.

Paolo Giarrusso (Feb 21 2022 at 17:35):

BTW thanks @Karl Palmskog from me as well, we also have similar problems; I’ll just add an extra vote for vos/vok

Rudi Grinberg (Feb 21 2022 at 17:42):

Paolo Giarrusso said:

BTW thanks Karl Palmskog from me as well, we also have similar problems; I’ll just add an extra vote for vos/vok

We can look at vos/vok at the hacking session. The last time I tried to do it, it was kind of complex. At this point I don't even remember what were the problems

Paolo Giarrusso (Feb 21 2022 at 17:43):

I should check the PR; IIRC, that concluded with sth like “we need a separate output folder to stop Coq from erasing vo files”

Paolo Giarrusso (Feb 21 2022 at 17:44):

https://github.com/ocaml/dune/pull/4050

Rudi Grinberg (Feb 21 2022 at 17:44):

Emilio Jesús Gallego Arias said:

It is not hard to support the legacy install scheme

Is there a document that describes how this works?

Paolo Giarrusso (Feb 21 2022 at 17:50):

Okay, I re-read the discussion about vos/vok. What’s the easiest way, in dune, to keep vos/vok and vo in completely separate folders?

Rudi Grinberg (Feb 21 2022 at 17:52):

We could create an output folder and then run coq in it, or we could pass flags to coq that would tell it to write to an output folder?

Rudi Grinberg (Feb 21 2022 at 17:53):

But if we create our own directory structure, will the editor tools understand it?

Rodolphe Lepigre (Feb 21 2022 at 17:58):

I guess dune coq top could figure out the right paths in any case, right?

Rodolphe Lepigre (Feb 21 2022 at 17:59):

(I mean, we should have control over where the editors look for files via coqtop.)

Emilio Jesús Gallego Arias (Feb 21 2022 at 18:49):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

It is not hard to support the legacy install scheme

Is there a document that describes how this works?

Not really, but it is quite simple, Coq dumps everything into user-contrib and it is scanned recursively using the folder name, so foo/bar/goo.v is mapped to foo.bar.goo

Emilio Jesús Gallego Arias (Feb 21 2022 at 18:49):

also COQPATH is taken into account

Emilio Jesús Gallego Arias (Feb 21 2022 at 18:49):

that's all

Emilio Jesús Gallego Arias (Feb 21 2022 at 18:50):

I think the plan for (coq lang 2.0) is to install stuff in $lib/package instead of a global file

Emilio Jesús Gallego Arias (Feb 21 2022 at 18:50):

but we need to think about it as not to repeat other design mistakes

Rudi Grinberg (Feb 21 2022 at 19:38):

Sure, but we'll still need to understand theories installed with makefiles, right?

Karl Palmskog (Feb 21 2022 at 19:42):

if we assume that (coq lang 2.0) is in a far future where nearly everyone uses Dune, it may not need to understand makefile-installed theories. But more directly, Coq devs can change coq_makefile to follow a new installation regime

Karl Palmskog (Feb 21 2022 at 19:43):

everything in the previous discussion has been about what can/should be done here and now, where Dune is a still a marginally used build system (outside of Coq-community)

Paolo Giarrusso (Feb 21 2022 at 20:16):

What would be needed? Can you just skip dependencies that aren’t found, if coqdep is happy?

Paolo Giarrusso (Feb 21 2022 at 20:17):

(I assume no, but I’m not entirely sure why). Or would you need a list of installed logical prefixes?

Rudi Grinberg (Feb 21 2022 at 20:24):

Does the current installation scheme for coq work well with nix?

Enrico Tassi (Feb 21 2022 at 21:05):

There is a known bug about OCAMLPATH being empty, hence coq master has problem loading plugins via findlib. Nothing foundamental. Other than that it is ok as far as I know.

Rudi Grinberg (Feb 21 2022 at 21:31):

I see. Just making sure that different packages don't need to install to the same place. For nix support, it's quite nice if it's possible to assemble a nix environment with all your packages just by customizing an env var (like OCAMLPATH for example)

Emilio Jesús Gallego Arias (Feb 22 2022 at 12:41):

@Rudi Grinberg Nix uses COQPATH indeed, but @Vincent Laporte may want to add more

Last updated: Apr 19 2024 at 14:02 UTC