Stream: Dune devs & users

Topic: Dune and coq_makefile parity


view this post on Zulip 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:

view this post on Zulip Karl Palmskog (Feb 21 2022 at 12:15):

other issues that are not as important:

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Feb 21 2022 at 12:17):

cc @Rudi Grinberg

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))
)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 21 2022 at 12:31):

but that's not incremental, right?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Feb 21 2022 at 12:36):

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

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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Karl Palmskog (Feb 21 2022 at 13:38):

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

view this post on Zulip Karl Palmskog (Feb 21 2022 at 13:39):

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

view this post on Zulip 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.

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Feb 21 2022 at 14:44):

VSCoq and CoqIDE both use coqidetop (xml protocol)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

Maybe that interesting comparsion could live in the wiki?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

I think you know better than I do

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:15):

issues would be great too

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:59):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Feb 21 2022 at 16:24):

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

view this post on Zulip 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

view this post on Zulip 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:

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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

It is not hard to support the legacy install scheme

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

but that's doable IMHO

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 16:36):

having that would mean 1.0 support

view this post on Zulip Rudi Grinberg (Feb 21 2022 at 16:37):

Karl Palmskog said:

other issues that are not as important:

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Rodolphe Lepigre (Feb 21 2022 at 16:45):

Rudi Grinberg said:

Karl Palmskog said:

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:

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.

view this post on Zulip Ali Caglayan (Feb 21 2022 at 16:47):

Rudi Grinberg said:

Karl Palmskog 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Feb 21 2022 at 16:50):

Or alternatively, is there an example to follow?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

that's the main eager bit

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 17:07):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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”

view this post on Zulip Paolo Giarrusso (Feb 21 2022 at 17:44):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Rudi Grinberg (Feb 21 2022 at 17:53):

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

view this post on Zulip Rodolphe Lepigre (Feb 21 2022 at 17:58):

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

view this post on Zulip Rodolphe Lepigre (Feb 21 2022 at 17:59):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 18:49):

also COQPATH is taken into account

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 18:49):

that's all

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Feb 21 2022 at 19:38):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Rudi Grinberg (Feb 21 2022 at 20:24):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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: Jan 30 2023 at 18:04 UTC