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

… 0.2 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. 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 <[email protected]>
ejgallego · Nov 11, 2022 · 08c6f56 · 08c6f56
1 parent 9fe942f
commit 08c6f56
Show file tree

Hide file tree

Showing 23 changed files with 47 additions and 57 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -59,6 +59,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)
 ------------------
 

diff --git a/doc/coq.rst b/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.
@@ -243,15 +243,15 @@ 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.
 - ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)`` field.
 - ``0.6``: Support for ``(stdlib no)``.
 
+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

diff --git a/doc/hacking.rst b/doc/hacking.rst
@@ -237,7 +237,7 @@ Such languages must be enabled in the ``dune`` project file separately:
 .. code:: scheme
 
    (lang dune 3.6)
-   (using coq 0.2)
+   (using coq 0.7)
 
 If such extensions are experimental, it's recommended that they pass
 ``~experimental:true``, and that their versions are below 1.0.

diff --git a/src/dune_rules/coq_mode.ml b/src/dune_rules/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
 

diff --git a/src/dune_rules/coq_mode.mli b/src/dune_rules/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
 

diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/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 | Legacy -> []
+    | VoOnly -> []
   in
   let obj_files =
     match obj_files_mode with

diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
@@ -248,7 +248,6 @@ module Context = struct
 
   let coqc_native_flags cctx : _ Command.Args.t =
     match cctx.mode with
-    | Legacy -> As []
     | VoOnly ->
       As
         [ "-w"
@@ -307,7 +306,7 @@ module Context = struct
 
   let setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs =
     match (mode : Coq_mode.t) with
-    | VoOnly | Legacy -> Memo.return (Resolve.return Path.Build.Set.empty)
+    | VoOnly -> Memo.return (Resolve.return Path.Build.Set.empty)
     | Native ->
       Resolve.Memo.bind theories_deps ~f:(fun theories_deps ->
           let+ l =

diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
@@ -3,9 +3,7 @@ open Dune_lang.Decoder
 
 let coq_syntax =
   Dune_lang.Syntax.create ~name:"coq" ~desc:"the Coq language"
-    [ ((0, 1), `Since (1, 9))
-    ; ((0, 2), `Since (2, 5))
-    ; ((0, 3), `Since (2, 8))
+    [ ((0, 3), `Since (2, 8))
     ; ((0, 4), `Since (3, 3))
     ; ((0, 5), `Since (3, 4))
     ; ((0, 6), `Since (3, 5))
@@ -57,12 +55,8 @@ module Buildable = struct
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
     and+ mode =
-      let default =
-        if coq_lang_version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly
-      in
-      located
-        (field "mode" ~default
-           (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
+      let default = Coq_mode.VoOnly in
+      located (field "mode" ~default Coq_mode.decode)
     and+ use_stdlib =
       field ~default:true "stdlib"
         (Dune_lang.Syntax.since coq_syntax (0, 6)
@@ -74,11 +68,7 @@ module Buildable = struct
         >>> repeat (located Lib_name.decode))
     and+ plugins =
       field "plugins" (repeat (located Lib_name.decode)) ~default:[]
-    and+ theories =
-      field "theories"
-        (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode)
-        ~default:[]
-    in
+    and+ theories = field "theories" (repeat Coq_lib_name.decode) ~default:[] in
     let plugins = merge_plugins_libraries ~plugins ~libraries in
     { flags; mode; use_stdlib; coq_lang_version; plugins; theories; loc }
 end

diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project b/test/blackbox-tests/test-cases/coq/base-unsound.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.7)
+(lang dune 2.8)
 
-(using coq 0.1)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/base.t/dune b/test/blackbox-tests/test-cases/coq/base.t/dune
@@ -4,6 +4,6 @@
  (modules :standard)
  (synopsis "Test Coq library"))
 
-(alias
- (name default)
+(rule
+ (alias default)
  (action (echo "%{read:base.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/base.t/dune-project b/test/blackbox-tests/test-cases/coq/base.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 1.9)
+(lang dune 2.8)
 
-(using coq 0.1)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/A/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodups.t/B/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-plugin.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/extract.t b/test/blackbox-tests/test-cases/coq/extract.t
@@ -1,6 +1,6 @@
   $ cat >dune-project <<EOF
-  > (lang dune 2.5)
-  > (using coq 0.2)
+  > (lang dune 2.8)
+  > (using coq 0.3)
   > EOF
 
   $ cat >extract.v <<EOF

diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/dune-project b/test/blackbox-tests/test-cases/coq/ml-lib.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 1.9)
+(lang dune 2.8)
 
-(using coq 0.1)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/dune-project b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
+(lang dune 2.8)
 
-(using coq 0.2)
+(using coq 0.3)
diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/dune b/test/blackbox-tests/test-cases/coq/rec-module.t/dune
@@ -6,6 +6,6 @@
 
 (include_subdirs qualified)
 
-(alias
- (name default)
+(rule
+ (alias default)
  (action (echo "%{read:rec.install}")))
diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/dune-project b/test/blackbox-tests/test-cases/coq/rec-module.t/dune-project
@@ -1,3 +1,3 @@
-(lang dune 1.9)
+(lang dune 2.8)
 
-(using coq 0.1)
+(using coq 0.3)