coq · coqbot-app · Dec 13, 2023 · Dec 1, 2023 · JasonGross · Dec 22, 2023
@@ -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.6.1
           opam list
         env:
           COMPILER: "4.12.0"

@@ -36,7 +36,7 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2023-06-30-8ca33f9dfd"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2023-11-30-7323af070e"
   EDGE_CACHEKEY: "edge_ubuntu-V2023-11-30-ba911a5fa6"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"

@@ -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.6.1
 
 - 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.
@@ -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

@@ -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
@@ -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.6" & >= "3.6.1"}
   "ocaml" {>= "4.09.0"}
   "ocamlfind" {>= "1.8.1"}
   "zarith" {>= "1.11"}

@@ -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.6"}
   "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"
@@ -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.6"}
   "coq-core" {= version}
   "odoc" {with-doc}
 ]

@@ -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.6"}
   "coq-core" {= version}
   "coq-stdlib" {= version}
   "coqide-server" {= version}

@@ -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.6"}
   "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"
@@ -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.6"}
   "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"
@@ -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.6.1 stdlib-shims.0.1.0 ocamlfind.1.8.1 odoc.2.0.2 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"

@@ -0,0 +1,4 @@
+- **Changed:**
+  Bump minimal Dune version required to build Coq to 3.6.1
+  (`#18359 <https://github.com/coq/coq/pull/18359>`_,
+  by Emilio Jesus Gallego Arias).
@@ -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))

@@ -1,7 +1,6 @@
-(lang dune 2.9)
+(lang dune 3.6)
 (name coq)
 (using coq 0.3)
-(cram enable)
 
 (formatting
  (enabled_for ocaml))
@@ -18,10 +17,14 @@
 (version dev)
 
 ; Note that we use coq.opam.template to have dune add the correct opam
-; prefix for configure
+; prefix for configure; also note that we manually add the dune >= 3.6.1
+; dependency due a dune bug preventing Coq to build in
+; 3.6.0. Dune adds `dune >= 3.6` automatically, based on `(lang dune 3.6)`
+; above, but that's not enough.
 (package
  (name coq-core)
  (depends
+  (dune (>= 3.6.1))
   (ocaml (>= 4.09.0))
   (ocamlfind (>= 1.8.1))
   (zarith (>= 1.11)))

@@ -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

@@ -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

@@ -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

@@ -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
 

@@ -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))