[coq] Remove support for Coq < 8.10 , and coq build languages 0.1 -- 0.7

Since ocaml#6409 we automatically infer rules for coq-native, and in
general this requires at least Coq 8.10 due to the need of
command-line option flags added in that version for native.

Also, since ocaml#7047 and `(coq lang 0.8)` we detect installed theories,
correcting a longstanding problem, we require all users to migrate.

The recommended path for most projects is just to upgrade their dune
file and Coq version file. Coq 8.10 will likely be the base we support
in `(lang coq 1.0)`.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

CHANGES.md

@@ -370,6 +370,9 @@ Unreleased
   diff` command can be used to just display the promotion without applying it.
   (#6160, fixes #5368, @emillon)
 
+- Coq versions < 8.10 are not supported anymore; Coq build language
+  versions 0.1 and 0.2 have been removed in consequence (# , @ejgallego)
+
 3.5.0 (2022-10-19)
 ------------------
 

bin/coq/coqtop.ml

@@ -85,7 +85,7 @@ let term =
           let stanza =
             Dune_rules.Coq_sources.lookup_module coq_src coq_module
           in
-          let args, use_stdlib, coq_lang_version, wrapper_name, mode =
+          let args, use_stdlib, wrapper_name, mode =
             match stanza with
             | None ->
               User_error.raise
@@ -96,14 +96,12 @@ let term =
               ( Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir
                   ~dir_contents:dc theory coq_module
               , theory.buildable.use_stdlib
-              , theory.buildable.coq_lang_version
               , Dune_rules.Coq_lib_name.wrapper (snd theory.name)
               , theory.buildable.mode )
             | Some (`Extraction extr) ->
               ( Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir extr
                   coq_module
               , extr.buildable.use_stdlib
-              , extr.buildable.coq_lang_version
               , "DuneExtraction"
               , extr.buildable.mode )
           in
@@ -118,7 +116,7 @@ let term =
                   | Some mode -> mode
                 in
                 Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name
-                  ~mode ~coq_lang_version coq_module
+                  ~mode coq_module
             in
             Action_builder.(run deps_of) Eager
           in

doc/coq.rst

@@ -134,10 +134,10 @@ The semantics of the fields are:
   Interproject composition has been available since :ref:`Coq lang
   0.4<coq-lang>`.
 
-  As of today, Dune cannot depend on installed Coq theories. This restriction
-  will be lifted in the future. Note that composition with the Coq standard
-  library is supported, but in this case the ``Coq`` prefix has been made
-  available in a qualified way, since :ref:`Coq lang 0.2<coq-lang>`.
+  As of today, Dune cannot depend on installed Coq theories. This
+  restriction will be lifted in the future. Note that composition with
+  the Coq standard library is supported, but in this case the ``Coq``
+  prefix is available in a qualified way.
 
   You may still use installed libraries in your Coq project, but there is
   currently no way for Dune to know about it.
@@ -254,9 +254,6 @@ file:
 
 The supported Coq language versions (not the version of Coq) are:
 
-- ``0.1``: Basic Coq theory support.
-- ``0.2``: Support for the ``theories`` field and composition of theories in the
-  same scope.
 - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9
   for Coq >= 8.14).
 - ``0.4``: Support for interproject composition of theories.
@@ -267,6 +264,9 @@ The supported Coq language versions (not the version of Coq) are:
   and ``(mode native)`` is deprecated. The ``dev`` profile also no longer
   disables native compilation.
 
+Coq language versions ``0.1`` and ``0.2`` have been deprecated in
+Dune 3.6, and removed in Dune 3.7.
+
 .. _coq-lang-1.0:
 
 Coq Language Version 1.0

doc/hacking.rst

@@ -252,7 +252,7 @@ Such languages must be enabled in the ``dune`` project file separately:
 .. code:: dune
 
    (lang dune 3.8)
-   (using coq 0.7)
+   (using coq 0.8)
 
 If such extensions are experimental, it's recommended that they pass
 ``~experimental:true``, and that their versions are below 1.0.

src/dune_rules/coq/coq_lib.ml

@@ -242,29 +242,6 @@ module Error = struct
     @@ User_message.make ~annots ~loc ?hints
          [ Pp.textf "Theory %S has not been found." name ]
 
-  module Hidden_reason = struct
-    type t =
-      | LackOfTheoryComposition
-      | LackOfInstalledComposition
-  end
-
-  let hidden_without_composition ~loc ~reason name =
-    let name = Coq_lib_name.to_string name in
-    let reason =
-      match reason with
-      | Hidden_reason.LackOfTheoryComposition ->
-        Pp.textf
-          "Upgrade coq lang to 0.4 to enable composition with theories in a \
-           different scope."
-      | LackOfInstalledComposition ->
-        Pp.textf
-          "Upgrade coq lang to 0.8 to enable composition with installed \
-           theories."
-    in
-    Resolve.Memo.fail
-    @@ User_message.make ~annots ~loc
-         [ Pp.textf "Theory %s not found in the current scope." name; reason ]
-
   let private_deps_not_allowed ~loc name =
     let name = Coq_lib_name.to_string name in
     Resolve.Memo.fail
@@ -352,16 +329,9 @@ module DB = struct
       | Some parent -> boot_library_id parent)
 
   module rec R : sig
-    val resolve_boot :
-         t
-      -> coq_lang_version:Dune_sexp.Syntax.Version.t
-      -> (Loc.t * lib) option Resolve.Memo.t
-
-    val resolve :
-         t
-      -> coq_lang_version:Dune_sexp.Syntax.Version.t
-      -> Loc.t * Coq_lib_name.t
-      -> lib Resolve.Memo.t
+    val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t
+
+    val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t
   end = struct
     open R
 
@@ -408,20 +378,17 @@ module DB = struct
         Option.to_list boot @ theories
       else theories
 
-    let resolve_boot ~coq_lang_version ~coq_db (boot_id : Id.t option) =
+    let resolve_boot ~coq_db (boot_id : Id.t option) =
       match boot_id with
       | Some boot_id ->
         let open Resolve.Memo.O in
-        let+ lib =
-          resolve ~coq_lang_version coq_db (boot_id.loc, boot_id.name)
-        in
+        let+ lib = resolve coq_db (boot_id.loc, boot_id.name) in
         Some (boot_id.loc, lib)
       | None -> Resolve.Memo.return None
 
-    let resolve_theory ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id
-        (loc, theory_name) =
+    let resolve_theory ~allow_private_deps ~coq_db ~boot_id (loc, theory_name) =
       let open Resolve.Memo.O in
-      let* theory = resolve ~coq_lang_version coq_db (loc, theory_name) in
+      let* theory = resolve coq_db (loc, theory_name) in
       let* () = Resolve.Memo.lift @@ check_boot ~boot_id theory in
       let+ () =
         if allow_private_deps then Resolve.Memo.return ()
@@ -433,17 +400,13 @@ module DB = struct
       in
       (loc, theory)
 
-    let resolve_theories ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id
-        theories =
-      let f =
-        resolve_theory ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id
-      in
+    let resolve_theories ~allow_private_deps ~coq_db ~boot_id theories =
+      let f = resolve_theory ~allow_private_deps ~coq_db ~boot_id in
       Resolve.Memo.List.map theories ~f
 
     let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) =
       let name = s.name in
       let id = Id.create ~path:(Path.build dir) ~name in
-      let coq_lang_version = s.buildable.coq_lang_version in
       let open Memo.O in
       let boot_id = if s.boot then None else boot_library_id coq_db in
       let allow_private_deps = Option.is_none s.package in
@@ -452,9 +415,9 @@ module DB = struct
         resolve_plugins ~db ~allow_private_deps ~name:(snd name)
           s.buildable.plugins
       and+ theories =
-        resolve_theories ~coq_db ~coq_lang_version ~allow_private_deps ~boot_id
+        resolve_theories ~coq_db ~allow_private_deps ~boot_id
           s.buildable.theories
-      and+ boot = resolve_boot ~coq_lang_version ~coq_db boot_id in
+      and+ boot = resolve_boot ~coq_db boot_id in
       let theories =
         maybe_add_boot ~boot ~use_stdlib ~is_boot:s.boot theories
       in
@@ -538,30 +501,20 @@ module DB = struct
       type t =
         | Found_stanza of Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t
         | Found_path of Coq_path.t
-        | Hidden of Error.Hidden_reason.t
         | Not_found
     end
 
-    let find coq_db ~coq_lang_version name : Resolve_final_result.t =
+    let find coq_db name : Resolve_final_result.t =
       match find coq_db name with
       | Not_found -> Not_found
-      | Theory (mldb, dir, stanza) when coq_lang_version >= (0, 4) ->
-        Found_stanza (mldb, dir, stanza)
-      | Legacy_theory cp when coq_lang_version >= (0, 8) -> Found_path cp
-      | Legacy_theory cp when Coq_path.stdlib cp -> Found_path cp
-      | Legacy_theory _ -> Hidden LackOfInstalledComposition
-      | Theory (mldb, dir, stanza) -> (
-        match coq_db.resolve name with
-        | Not_found -> Hidden LackOfTheoryComposition
-        | Theory _ | Redirect _ | Legacy_theory _ ->
-          Found_stanza (mldb, dir, stanza))
+      | Theory (mldb, dir, stanza) -> Found_stanza (mldb, dir, stanza)
+      | Legacy_theory cp -> Found_path cp
 
     (** Our final final resolve is used externally, and should return the
         library data found from the previous iterations. *)
-    let resolve coq_db ~coq_lang_version (loc, name) =
-      match find coq_db ~coq_lang_version name with
+    let resolve coq_db (loc, name) =
+      match find coq_db name with
       | Not_found -> Error.theory_not_found ~loc name
-      | Hidden reason -> Error.hidden_without_composition ~loc ~reason name
       | Found_stanza (db, dir, stanza) ->
         let open Memo.O in
         let+ theory = create_from_stanza coq_db db dir stanza in
@@ -575,9 +528,9 @@ module DB = struct
         let+ theory = create_from_coqpath ~boot_id cp in
         Legacy theory
 
-    let resolve_boot coq_db ~coq_lang_version =
+    let resolve_boot coq_db =
       let boot_id = boot_library_id coq_db in
-      resolve_boot ~coq_lang_version ~coq_db boot_id
+      resolve_boot ~coq_db boot_id
   end
 
   include R
@@ -664,8 +617,7 @@ module DB = struct
     { parent; resolve; boot_id }
 
   (* Resolve helpers *)
-  let find_many t theories ~coq_lang_version =
-    Resolve.Memo.List.map theories ~f:(resolve ~coq_lang_version t)
+  let find_many t theories = Resolve.Memo.List.map theories ~f:(resolve t)
 end
 
 let theories_closure = function

src/dune_rules/coq/coq_lib.mli

@@ -65,20 +65,9 @@ module DB : sig
       libraries are installed, we would infer the right amount of information. *)
   val create_from_coqpaths : Coq_path.t list -> t
 
-  val find_many :
-       t
-    -> (Loc.t * Coq_lib_name.t) list
-    -> coq_lang_version:Dune_sexp.Syntax.Version.t
-    -> lib list Resolve.Memo.t
-
-  val resolve_boot :
-       t
-    -> coq_lang_version:Dune_sexp.Syntax.Version.t
-    -> (Loc.t * lib) option Resolve.Memo.t
-
-  val resolve :
-       t
-    -> coq_lang_version:Dune_sexp.Syntax.Version.t
-    -> Loc.t * Coq_lib_name.t
-    -> lib Resolve.Memo.t
+  val find_many : t -> (Loc.t * Coq_lib_name.t) list -> lib list Resolve.Memo.t
+
+  val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t
+
+  val resolve : t -> Loc.t * Coq_lib_name.t -> lib Resolve.Memo.t
 end

src/dune_rules/coq/coq_mode.ml

@@ -7,7 +7,6 @@
    where mode was not supported, this allows us support older Coq compiler
    versions with coq-lang < 0.3 *)
 type t =
-  | Legacy
   | VoOnly
   | Native
   | VosOnly

src/dune_rules/coq/coq_mode.mli

@@ -7,7 +7,6 @@
    where mode was not supported, this allows us support older Coq compiler
    versions with coq-lang < 0.3 *)
 type t =
-  | Legacy
   | VoOnly
   | Native
   | VosOnly

src/dune_rules/coq/coq_module.ml

@@ -88,7 +88,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
           ( Path.Build.relative vo_dir x
           , Filename.(concat (concat install_vo_dir ".coq-native") x) ))
         cmxs_obj
-    | VoOnly | VosOnly | Legacy -> []
+    | VoOnly | VosOnly -> []
   in
   let obj_files =
     match obj_files_mode with