[build] Bump minimal dune version to 3.5

This brings mainly improvements into the directory target feature, so we can go ahead with packaging the docs properly. Note some fixes in documentation, plus now Dune enables some more warnings by default that we address in the following way: - warning 67 [unused functor parameter]: we make the arguments anonymous as OCaml seems to recommend - warning 69 [unused-field]: we disable this warning, but should be maybe enabled and handled again. It seems that most of the triggers for this warning are legit, however the situation is delicate due to some parts of the code involved using `Obj.magic` or `Marshall`. Also quite a few of these warnings are in code that is scheduled for removal at some point.
coq · Dec 1, 2023 · f2f10e1 · f2f10e1
1 parent 1788628
commit f2f10e1
Show file tree

Hide file tree

Showing 19 changed files with 27 additions and 35 deletions.
diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml
@@ -24,7 +24,7 @@ jobs:
           opam switch set ocaml-base-compiler.$COMPILER
           eval $(opam env)
           opam update
-          opam install -j "$NJOBS" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.11 dune.2.9.1
+          opam install -j "$NJOBS" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.11 dune.3.5.0
           opam list
         env:
           COMPILER: "4.12.0"

diff --git a/INSTALL.md b/INSTALL.md
@@ -18,9 +18,11 @@ Build Requirements
 To compile Coq yourself, you need:
 
 - [OCaml](https://ocaml.org/) (version >= 4.09.0)
-  (This version of Coq has been tested up to OCaml 4.14.0)
+  (This version of Coq has been tested up to OCaml 4.14.1, for the 4.x series)
 
-- The [Dune OCaml build system](https://github.com/ocaml/dune/) >= 2.9.1
+  Support for OCaml 5.x remains experimental.
+
+- The [Dune OCaml build system](https://github.com/ocaml/dune/) >= 3.5.0
 
 - The [ZArith library](https://github.com/ocaml/Zarith) >= 1.11
 
@@ -60,7 +62,7 @@ CoqIDE with:
 Opam (https://opam.ocaml.org/) is recommended to install OCaml and
 the corresponding packages.
 
-    $ opam switch create coq --packages="ocaml-variants.4.12.0+options,ocaml-option-flambda"
+    $ opam switch create coq --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
     $ eval $(opam env)
     $ opam install dune ocamlfind zarith lablgtk3-sourceview3
 
@@ -119,11 +121,3 @@ like `COQLIB="some path"`, that is a variable name followed by `=` and
 a string that follows OCaml's escaping conventions. This feature can be
 used by installers of binary package to make Coq aware of its installation
 path.
-
-Known problems
---------------
-
-- On OSX, when using Opam with sandboxing and Dune < 3.0 with caching
-  enabled, Coq may fail to install, due to Opam's sandboxing
-  restricting the permissions needed for the Dune 2.x caching
-  daemon. See https://github.com/coq/coq/issues/15138 more details.
diff --git a/clib/cSet.mli b/clib/cSet.mli
@@ -26,7 +26,7 @@ sig
   val hash : t -> int
 end
 
-module Hashcons (M : OrderedType) (H : HashedType with type t = M.t) : Hashcons.S with
+module Hashcons (M : OrderedType) (_ : HashedType with type t = M.t) : Hashcons.S with
   type t = Set.Make(M).t
   and type u = M.t -> M.t
 (** Create hash-consing for sets. The hashing function provided must be

diff --git a/clib/unionfind.mli b/clib/unionfind.mli
@@ -78,5 +78,5 @@ end
 
 module Make :
   functor (S:SetS) ->
-    functor (M:MapS with type key = S.elt) ->
+    functor (_:MapS with type key = S.elt) ->
       PartitionSig with type elt = S.elt and type set = S.t
diff --git a/coq-core.opam b/coq-core.opam
@@ -27,7 +27,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "ocaml" {>= "4.09.0"}
   "ocamlfind" {>= "1.8.1"}
   "zarith" {>= "1.11"}

diff --git a/coq-doc.opam b/coq-doc.opam
@@ -16,7 +16,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "conf-python-3" {build}
   "coq" {build & = version}
   "odoc" {with-doc}
@@ -30,11 +30,9 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/coq-stdlib.opam b/coq-stdlib.opam
@@ -23,7 +23,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "coq-core" {= version}
   "odoc" {with-doc}
 ]

diff --git a/coq.opam b/coq.opam
@@ -20,7 +20,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "coq-core" {= version}
   "coq-stdlib" {= version}
   "coqide-server" {= version}

diff --git a/coqide-server.opam b/coqide-server.opam
@@ -19,7 +19,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "coq-core" {= version}
   "odoc" {with-doc}
 ]
@@ -32,11 +32,9 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/coqide.opam b/coqide.opam
@@ -17,7 +17,7 @@ homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.5"}
   "ocamlfind" {build}
   "conf-findutils" {build}
   "conf-adwaita-icon-theme"
@@ -35,11 +35,9 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile
@@ -48,7 +48,7 @@ ENV COMPILER="4.09.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
-    BASE_ONLY_OPAM="dune.2.9.1 stdlib-shims.0.1.0 ocamlfind.1.8.1 odoc.1.5.3 yojson.1.7.0 num.1.4"
+    BASE_ONLY_OPAM="dune.3.5.0 stdlib-shims.0.1.0 ocamlfind.1.8.1 odoc.1.5.3 yojson.1.7.0 num.1.4"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.2"

diff --git a/doc/changelog/11-standard-library/18359-dune_35.rst b/doc/changelog/11-standard-library/18359-dune_35.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  Bump minimal Dune version required to build Coq to 3.5.0
+  (`#18359 <https://github.com/coq/coq/pull/18359>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/dune b/dune
@@ -1,6 +1,6 @@
 ; Default flags for all Coq libraries.
 (env
- (dev     (flags :standard -w -9-27@60@70 \ -short-paths)
+ (dev     (flags :standard -w -9-27@60-69@70 \ -short-paths)
           (coq (flags :standard -w +default)))
  (release (flags :standard)
           (ocamlopt_flags :standard -O3 -unbox-closures))

diff --git a/dune-project b/dune-project
@@ -1,6 +1,6 @@
-(lang dune 2.9)
+(lang dune 3.5)
 (name coq)
-(using coq 0.3)
+(using coq 0.6)
 
 (formatting
  (enabled_for ocaml))

diff --git a/library/goptions.mli b/library/goptions.mli
@@ -61,7 +61,7 @@ type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
 
 module MakeStringTable :
   functor
-    (A : sig
+    (_ : sig
        val key : option_name
        val title : string
        val member_message : string -> bool -> Pp.t

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
@@ -71,7 +71,7 @@ val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
 module PrintingInductiveMake :
-  functor (Test : sig
+  functor (_ : sig
     val encode : Environ.env -> Libnames.qualid -> Names.inductive
     val member_message : Pp.t -> bool -> Pp.t
     val field : string

diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
@@ -211,7 +211,7 @@ end
 
 (** Server-side functor. [MakeWorker T] creates the server task
     dispatcher. *)
-module MakeWorker(T : Task) () : sig
+module MakeWorker(_ : Task) () : sig
 
   (** [init_stdout ()] is called at [Coqtop.toploop_init] time. *)
   val init_stdout : unit -> unit

diff --git a/theories/dune.disabled b/theories/dune.disabled
@@ -6,7 +6,7 @@
  ; Uncomment this to have dune compile native files in release mode
  ; (mode native)
  (boot)
- (libraries
+ (plugins
    coq-core.plugins.ltac
    coq-core.plugins.tauto
 

diff --git a/user-contrib/Ltac2/dune.disabled b/user-contrib/Ltac2/dune.disabled
@@ -3,4 +3,4 @@
  (package coq-stdlib)
  (synopsis "Ltac2 tactic language")
  (flags -w -deprecated-native-compiler-option)
- (libraries coq-core.plugins.ltac2))
+ (plugins coq-core.plugins.ltac2))