This means that from now on, Dune (>= 2.5.1) becomes mandatory for
building Coq (though Dune >= 2.8.5 is recommended).
We still have two build systems at this point: one that uses Dune only
to build OCaml code and one that uses Dune for the entire build
(including Coq files).
A major change for the legacy build system is that build outputs for
Coq files (vo and friends) are now stored into a _build_vo/ directory,
which means that the build becomes mostly hygienic. One major
consequence is that in principle, you should be able to switch between
the dev modes of the two build systems (./configure -profile devel &&
make -j4 and make -f Makefile.dune world) without having to call make
clean or git clean anymore. If you have leftover compiled files from a
previous non-hygienic compilation, it's probably a good idea to call
git clean (with the usual caution regarding the use of this command).
I also recommend activating the Dune cache, as you should notice
significant compilation speed thanks to it. To do it, just add (cache
enabled) to your dune configuration file (mine is in
~/.config/dune/config).
Please open issues if you encounter any bug. Do not hesitate to ask
for help on Zulip or by replying to this message if you need some.
How do you clean up all these messages? I clean up a bunch, re-run, then I get a new batch. A time waster. IIRC there was a cleanup utility, which needs to document exactly what it may delete. Without doc, it’s a lot like a loaded gun–someone may get injured.
Error: Multiple rules generated for _build/default/ide/coqide/coq_lex.ml:
[maybe this is not the right place to ask, tell me]
I have difficulties understanding how to reproduce the compilation
process by hand. In particular because -Q and -R options until now
were specifying simultaneously how to compile things and how to look
for already compiled things (which was simple but arguably not
flexible).
Suppose I have Foo/bar.v and Foo/foo.v, the latter depending on the former.
I see how to compile the first one:
coqc -Q Foo Foo Foo/bar.v -o _build/Foo/bar.vo
but how should I compile the second one? Like this?
No. The jump to definition feature of editors is generally provided by
merlin, which is fully compatible with Dune.
There is a small catch, which is that you need the right merlin
version for the right Dune version, because there was a change in the
way merlin uses Dune in Dune 2.8.
No, coq_makefile will keep producing makefiles and will never rely on Dune.
I was not aware of anyone ever using the proofgeneral autocompilation
feature in coq sources, but of course everyone has their own dev
setups and habits...
Ex: “Note that dune will call configure for you if needed, so no need to call ./configure in the regular development workflow.” is inconsistent with your email.
If you use the full Dune build, then dune build dev/shim/coqtop-prelude and dune build dev/shim/coqide-prelude should build the minimum to get to a working coqtop or coqide (that you can run through these shims so that the right options are set).
I believe the two were intended as meaning the same. Doc targets are excluded. I guess you would consider them part of a full Coq distribution? If yes, then it’s build-system.dune.md which should be amended.
It is not. This file documents everything about Makefile.dune. These are targets than you can use without calling ./configure first. The mention of ./configure -profile devel in my initial message was so that you can run the legacy / hybrid build.
Specifying 2 directories for logical name Foo seems strange. Maybe the
first -Q should be a -I? But then How coq does know where to find
Foo.bar?
"Hygienic" builds do indeed require as a first step to copy the sources
to the build directory; this could be lifted in the future, but as of
today both the Coq and OCaml do require this.
Using makespeak, you setup a rule like this:
$(build_dir)/%.v: %.v
cp \-a $< $@
then your coq rule looks like:
cp -a $< $@
then your coq rule looks like:
$(build_dir)/%.vo: $(build_dir)/%.v
coqc $< ...
Thus, once you have the copy under _build, your program is compiled as
Pierre Courtieu <pierre.courtieu@gmail.com> writes:
Note: proofgeneral autocompilation feature is probably broken in coq sources.
One particular tricky part is to handle plugins; if you are hacking
under the Coq tree, a change in coqc or in most plugins does indeed
require an update of all .vo files.
The plan regarding users of coqtop is to have in Dune 2.9 a
`dune coqtop file.v` command that will indeed ensure all deps of file.v
are up to date before starting coqtop.
Language servers for OCaml do also communicate with dune I think, but
I'm not familiar with the details.
Thanks for the explanation.
PG autocompilation does not deal with ocaml compilation anyway. I
guess the feature is useful only when developing coq theories.
Best regards,
Pierre
Pierre Courtieu <pierre.courtieu@gmail.com> writes:
I guess the feature is useful only when developing coq theories.
Actually for those of us using the bleeding-edge build system, Gaëtan
added some setup so when we are inside Coq sources Proof General will
not call `coqtop` but a preliminary version of `dune coqtop` (*) that
ensures that at least the regular plugins, coqc, and the prelude is up
to date.
In general, I am not sure how I feel about editors replicating build
functionality vs communicating with the build tool. Both PG and jsCoq
have some code [in jsCoq's case to build addons] that emulates the build
system, but that is gonna be pretty hard to maintain in the medium term
as we hope to take profit from some advances features in terms of
Coq library organization.