[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3

CHANGES.md

@@ -30,6 +30,10 @@ Unreleased
 
 - Auto-detect `dune-project` files as `dune` files in Emacs (#4222, @shonfeder)
 
+- Restore compatibility with Coq < 8.10 for coq-lang < 0.3 , document
+  that `(using coq 0.3)` does require Coq 8.10 at least (#4224, fixes
+  #4142, @ejgallego)
+
 2.8.2 (21/01/2021)
 ------------------
 

doc/dune-files.rst

@@ -1642,9 +1642,10 @@ language version is absent, dune will automatically add this line with the
 latest Coq version to the project file once a ``(coq.theory ...)`` stanza is used anywhere.
 
 The supported Coq language versions 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)``.
+- ``0.3``: support for ``(mode native)``, requires Coq >= 8.10.
 
 Guarantees with respect to stability are not provided yet,
 however, as implementation of features progresses, we hope to reach

src/dune_rules/coq_mode.ml

@@ -3,7 +3,11 @@
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
+(* Legacy is used to signal that we are in a mode prior to Coq syntax 0.3 ,
+   where mode was not supported, this allows us support older Coq compiler
+   versions with coq-lang < 0.3 *)
 type t =
+  | Legacy
   | VoOnly
   | Native
 

src/dune_rules/coq_mode.mli

@@ -3,7 +3,11 @@
 (* (c) INRIA 2020                              *)
 (* Written by: Emilio Jesús Gallego Arias *)
 
+(* Legacy is used to signal that we are in a mode prior to Coq syntax 0.3 ,
+   where mode was not supported, this allows us support older Coq compiler
+   versions with coq-lang < 0.3 *)
 type t =
+  | Legacy
   | VoOnly
   | Native
 

src/dune_rules/coq_module.ml

@@ -68,7 +68,9 @@ 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 -> []
+    | VoOnly
+    | Legacy ->
+      []
   in
   let obj_files =
     match obj_files_mode with

src/dune_rules/coq_rules.ml

@@ -157,6 +157,7 @@ module Context = struct
 
   let coqc_native_flags cctx : _ Command.Args.t =
     match cctx.mode with
+    | Coq_mode.Legacy -> Command.Args.As []
     | Coq_mode.VoOnly ->
       Command.Args.As
         [ "-w"; "-native-compiler-disabled"; "-native-compiler"; "ondemand" ]
@@ -214,7 +215,9 @@ module Context = struct
           List.fold_left theories_deps ~init:theory_dirs ~f:(fun acc lib ->
               let theory_dirs = directories_of_lib ~sctx lib in
               Path.Build.Set.(union acc (of_list theory_dirs))))
-    | Coq_mode.VoOnly -> Or_exn.return Path.Build.Set.empty
+    | Coq_mode.VoOnly
+    | Coq_mode.Legacy ->
+      Or_exn.return Path.Build.Set.empty
 
   let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~theory_dirs
       (buildable : Buildable.t) =

src/dune_rules/coq_stanza.ml

@@ -39,8 +39,15 @@ module Buildable = struct
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
     and+ mode =
+      let* version = Dune_lang.Syntax.get_exn coq_syntax in
+      let default =
+        if version < (0, 3) then
+          Coq_mode.Legacy
+        else
+          Coq_mode.VoOnly
+      in
       located
-        (field "mode" ~default:Coq_mode.VoOnly
+        (field "mode" ~default
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ libraries =
       field "libraries" (repeat (located Lib_name.decode)) ~default:[]