[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>
ejgallego · Apr 21, 2023 · 9304bc5 · 9304bc5
1 parent 57bdb68
commit 9304bc5
Show file tree

Hide file tree

Showing 21 changed files with 44 additions and 51 deletions.
diff --git a/CHANGES.md b/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)
 ------------------
 

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

diff --git a/doc/hacking.rst b/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.

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

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

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

diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml
@@ -13,16 +13,12 @@ let coq_syntax =
     ; ((0, 8), `Since (3, 8))
     ]
 
-let already_warned = ref false
-
 let get_coq_syntax () =
   let* version = Dune_lang.Syntax.get_exn coq_syntax in
-  if version < (0, 8) && not !already_warned then (
-    already_warned := true;
-    User_warning.emit
+  if version < (0, 8) then (
+    User_error.raise
       [ Pp.text
-          "Coq Language Versions lower than 0.8 have been deprecated in Dune \
-           3.8 and will be removed in Dune 3.9"
+          "Coq Language Versions lower than 0.8 have been removed in Dune 3.8, please upgrade to (coq lang 0.8) or later if available"
       ]);
   return version
 
@@ -85,11 +81,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/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)