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:
(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._CoqProject
+Dune+ProofGeneral (due to Dune file hygiene, ProofGeneral doesn't find .vo
files built by Dune)other issues that are not as important:
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.vio
/.vos
/.vok
compilation with DuneI can give specific examples (specific projects where this is a problem) for each of these issues. But please ask if you want that.
cc @Rudi Grinberg
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
see this issue for discussion of some of the issues above: https://github.com/coq-community/manifesto/issues/87
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
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
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))
)
glob_files_rec
has nothing to do with Coq glob btw, just lets you recursively go through folders
but that's not incremental, right?
anyway, I think there should be an official stanza so everybody doesn't have to add it locally...
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
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.
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.
FYI I'm currently looking into proper editor support for dune (see https://github.com/ocaml/dune/pull/5457).
here is some discussion on Dune in ProofGeneral: https://github.com/ProofGeneral/PG/issues/573
also, I have no idea about Dune in VsCoq or Coqtail/Vim or CoqIDE
We’d need to use dune coqtop in vscoq etc as well, but I hope that’s easier.
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…
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
.
VSCoq and CoqIDE both use coqidetop (xml protocol)
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.
Also what is with the dune coq X
seperation? I thought it would be more intuitive to have dune coqX
?
Thanks a lot @Karl Palmskog , do we have a good place to add that info?
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)
Maybe that interesting comparsion could live in the wiki?
I think you know better than I do
issues would be great too
we will do a dune hacking event and there is a bit of manpower
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
maybe @Rudi Grinberg can advise how he would prefer to track the most important issues on Coq+Dune
Ali Caglayan said:
Also what is with the
dune coq X
seperation? I thought it would be more intuitive to havedune coqX
?
Indeed it was decided to group dune ocaml
etc ... commands in subcommands
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.
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)
then I think one could add an issue label like: coq-critical
one could argue that the IDE support question is not strictly Dune's problem, but for tracking it may be useful nevertheless
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'suser-contrib
. So you have to choose mutually exclusively between composable local builds of projects with manydune
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:
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.
It is not hard to support the legacy install scheme
would be a bit hacky as dune would have to infer what packages are installed from the coqpath contents
but that's doable IMHO
having that would mean 1.0 support
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)
Load
and add an appropriate dep.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)
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
)
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:
coqtop
command that is running when we detect that the project uses dune to build Coq (maybe this requires a kind of user flag?),_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.
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.
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?
Or alternatively, is there an example to follow?
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.
If it is dune which starts coq*top
, then I don't think these is any need for generating the _CoqProject file.
I think in Dune 3.0 we can indeed query coqc
for capabilities
the rule setup is dynamic enought, as long as the theory Database doesn't depend on it
that's the main eager bit
[file_contents seems fine to me and that'd be the trickiest point]
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.
BTW thanks @Karl Palmskog from me as well, we also have similar problems; I’ll just add an extra vote for vos/vok
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
I should check the PR; IIRC, that concluded with sth like “we need a separate output folder to stop Coq from erasing vo files”
https://github.com/ocaml/dune/pull/4050
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?
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?
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?
But if we create our own directory structure, will the editor tools understand it?
I guess dune coq top
could figure out the right paths in any case, right?
(I mean, we should have control over where the editors look for files via coqtop
.)
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
also COQPATH is taken into account
that's all
I think the plan for (coq lang 2.0)
is to install stuff in $lib/package
instead of a global file
but we need to think about it as not to repeat other design mistakes
Sure, but we'll still need to understand theories installed with makefiles, right?
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
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)
What would be needed? Can you just skip dependencies that aren’t found, if coqdep is happy?
(I assume no, but I’m not entirely sure why). Or would you need a list of installed logical prefixes?
Does the current installation scheme for coq work well with nix?
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.
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)
@Rudi Grinberg Nix uses COQPATH indeed, but @Vincent Laporte may want to add more
Last updated: Oct 13 2024 at 01:02 UTC