Merge PR #11174: [dune] Update to dune language version 2.0

Reviewed-by: Zimmi48

12 files changed, 42 insertions, 22 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 49e1361407..6344b51702 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2019-11-25-V01"
+  CACHEKEY: "bionic_coq-V2019-12-03-V81"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/coq.opam b/coq.opam
index 4399dafe7c..6aec0132be 100644
--- a/coq.opam
+++ b/coq.opam
@@ -21,8 +21,8 @@ license: "LGPL-2.1"
 version: "dev"
 
 depends: [
-  "ocaml"     {         >= "4.05.0" }
-  "dune"      { build & >= "1.10.0"  }
+  "ocaml"     { >= "4.05.0" }
+  "dune"      { >= "2.0.0"  }
   "ocamlfind" { build }
   "num"
 ]
diff --git a/coqide-server.opam b/coqide-server.opam
index 5da533ea6b..4cec409f78 100644
--- a/coqide-server.opam
+++ b/coqide-server.opam
@@ -21,8 +21,8 @@ license: "LGPL-2.1"
 version: "dev"
 
 depends: [
-  "dune"      { build & >= "1.10.0" }
-  "coq"       {          = version }
+  "dune"      { >= "2.0.0" }
+  "coq"       {  = version }
 ]
 
 build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
diff --git a/coqide.opam b/coqide.opam
index 3e588ed0cf..54b8dca98b 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -19,10 +19,10 @@ license: "LGPL-2.1"
 version: "dev"
 
 depends: [
-  "dune"                 { build & >= "1.10.0" }
-  "coqide-server"        {          = version }
-  "lablgtk3"             {         >= "3.0.beta5" }
-  "lablgtk3-sourceview3" {         >= "3.0.beta5" }
+  "dune"                 { >= "2.0.0" }
+  "coqide-server"        {  = version }
+  "lablgtk3"             { >= "3.0.beta5" }
+  "lablgtk3-sourceview3" { >= "3.0.beta5" }
 ]
 
 build-env: [
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 78c0b4b2c7..82cc7a7117 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1132,11 +1132,22 @@ function make_findlib {
 function make_dune {
   make_ocaml
 
-  if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
+  if build_prep https://github.com/ocaml/dune/archive/ 2.0.0 tar.gz 1 dune-2.0.0 ; then
 
     log2 make release
     log2 make install
 
+    # Dune support libs, we don't install glob and action-plugin as
+    # they are not needed by Coq
+    logn dune-private-build dune build -p dune-private-libs @install
+    logn dune-private-install dune install dune-private-libs
+
+    logn dune-configurator-build dune build -p dune-configurator @install
+    logn dune-configurator-install dune install dune-configurator
+
+    logn dune-build-info dune build -p dune-build-info @install
+    logn dune-build-info dune install dune-build-info
+
     build_post
   fi
 }
@@ -1191,7 +1202,8 @@ function make_ocaml_cairo2 {
 
     log2 dune build cairo2.install
     log2 dune install cairo2
-    log2 dune clean
+    # See https://github.com/ocaml/dune/issues/2921
+    # log2 dune clean
     build_post
 
   fi
@@ -1216,7 +1228,8 @@ function make_lablgtk {
     log2 dune build -p lablgtk3-sourceview3
     log2 dune install lablgtk3-sourceview3
 
-    log2 dune clean
+    # See https://github.com/ocaml/dune/issues/2921
+    # log2 dune clean
     build_post
   fi
 }
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e80f96362b..8907843b12 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-11-25-V01"
+# CACHEKEY: "bionic_coq-V2019-12-03-V81"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.8.0"
 
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.09.0" \
     COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.2"
+    BASE_OPAM_EDGE="dune-release.1.3.3"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 28e8773e25..49e338d0a5 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,4 +1,4 @@
-(lang dune 1.10)
+(lang dune 2.0)
 
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index 353d58c676..b788fbbeed 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1,8 +1,10 @@
 (dirs :standard _static)
 
-(rule (targets README.gen.rst)
+(rule
+ (targets README.gen.rst)
  (deps (source_tree ../tools/coqrst) README.template.rst)
  (action (run ../tools/coqrst/regen_readme.py %{targets})))
 
-(alias (name refman-html)
-  (action (diff README.rst README.gen.rst)))
+(rule
+ (alias refman-html)
+ (action (diff README.rst README.gen.rst)))
diff --git a/dune-project b/dune-project
index 45d9d06314..1249c4af9f 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 1.10)
+(lang dune 2.0)
 (name coq)
 (using coq 0.1)
 
diff --git a/ide/dune b/ide/dune
index 7200915593..a599be9351 100644
--- a/ide/dune
+++ b/ide/dune
@@ -21,6 +21,7 @@
  (package coqide-server)
  (modules idetop)
  (libraries coq.toplevel coqide-server.protocol)
+ (modes native byte)
  (link_flags -linkall))
 
 (install
@@ -45,6 +46,7 @@
  (name coqide_main)
  (public_name coqide)
  (package coqide)
+ (optional)
  (modules coqide_main)
  (libraries coqide_gui))
 
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 8d8374a603..2998178be2 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -2,8 +2,10 @@
  (name byterun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
  (public_name coq.vm)
- (c_flags (:include %{project_root}/config/dune.c_flags))
- (c_names coq_fix_code coq_memory coq_values coq_interp))
+ (foreign_stubs
+  (language c)
+  (names coq_fix_code coq_memory coq_values coq_interp)
+  (flags (:include %{project_root}/config/dune.c_flags))))
 
 (rule
  (targets coq_instruct.h)
diff --git a/topbin/dune b/topbin/dune
index 7b77826216..46052c81e5 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -26,6 +26,7 @@
  (package coq)
  (modules coqc_bin)
  (libraries coq.toplevel)
+ (modes native byte)
  ; Adding -ccopt -flto to links options could be interesting, however,
  ; it doesn't work on Windows
  (link_flags -linkall))