[dune] Move to Dune 1.10, use coq.pp directive.

We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.

Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.

Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.

I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.

coq.opam

@@ -20,7 +20,7 @@ license: "LGPL-2.1"
 
 depends: [
   "ocaml"     {         >= "4.05.0" }
-  "dune"      { build & >= "1.6.0"  }
+  "dune"      { build & >= "1.10.0"  }
   "ocamlfind" { build }
   "num"
 ]

coqide-server.opam

@@ -19,7 +19,7 @@ dev-repo: "git+https://github.com/coq/coq.git"
 license: "LGPL-2.1"
 
 depends: [
-  "dune"      { build & >= "1.6.0" }
+  "dune"      { build & >= "1.10.0" }
   "coq"       {          = version }
 ]
 

coqide.opam

@@ -17,7 +17,7 @@ dev-repo: "git+https://github.com/coq/coq.git"
 license: "LGPL-2.1"
 
 depends: [
-  "dune"                 { build & >= "1.6.0" }
+  "dune"                 { build & >= "1.10.0" }
   "coqide-server"        {          = version }
   "lablgtk3"             {         >= "3.0.beta5" }
   "lablgtk3-sourceview3" {         >= "3.0.beta5" }

dev/build/windows/makecoq_mingw.sh

@@ -1132,7 +1132,7 @@ function make_findlib {
 function make_dune {
   make_ocaml
 
-  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then
+  if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
 
     log2 make release
     log2 make install

dev/doc/build-system.dune.md

@@ -52,7 +52,7 @@ order to use them, do:
 
 ```
 $ make -f Makefile.dune voboot                # Only once per session
-$ dune exec dev/shim/coqtop-prelude
+$ dune exec -- dev/shim/coqtop-prelude
 ```
 
 or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
@@ -108,14 +108,14 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg /path/to/foo.v
 (ocd) source dune_db
 ```
 
 or
 
 ```
-dune exec dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker Foo
 (ocd) source dune_db
 ```
 
@@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
 ```
-dune exec dev/shim/coqbyte-prelude
+dune exec -- dev/shim/coqbyte-prelude
 > Drop.
 # #directory "dev";;
 # #use "include_dune";;

dev/nixpkgs.nix

@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz";
-  sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1";
+  url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz";
+  sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw";
 })

dune-project

@@ -1,2 +1,8 @@
-(lang dune 1.6)
+(lang dune 1.10)
 (name coq)
+(using coq 0.1)
+
+; We cannot set this to true until as long as the build is not
+; properly bootstrapped [that is, we remove the voboot target]
+;
+; (generate_opam_files true)

tools/coq_dune.ml

@@ -193,9 +193,7 @@ let pp_vo_dep dir fmt vo =
   pp_rule fmt all_targets deps action
 
 let pp_mlg_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
-  let mlg_rule = "(run coqpp %{pp-file})" in
-  pp_rule fmt [target] [ml] mlg_rule
+  fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml)
 
 let pp_dep dir fmt oo = match oo with
   | VO vo -> pp_vo_dep dir fmt vo