[coq] Move mode to buildable, guard with coq 0.3 lang version

src/dune_engine/stanza.ml

@@ -6,7 +6,7 @@ module Parser = struct
   type nonrec t = string * t list Dune_lang.Decoder.t
 end
 
-let latest_version = (2, 7)
+let latest_version = (2, 8)
 
 let since v = (v, `Since v)
 

src/dune_rules/coq_rules.ml

@@ -163,7 +163,7 @@ module Context = struct
           (* If the mlpack files don't exist, don't fail *)
           Build.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)) )
 
-  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~mode
+  let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps
       ~native_includes (buildable : Buildable.t) =
     let loc = buildable.loc in
     let rr = resolve_program sctx ~dir ~loc in
@@ -188,7 +188,7 @@ module Context = struct
     ; boot_type = Bootstrap.No_boot
     ; build_dir
     ; profile_flags = Super_context.coq sctx ~dir
-    ; mode
+    ; mode = snd buildable.mode
     ; native_includes
     }
 
@@ -369,12 +369,11 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
     (* Coq flags for depending libraries *)
     let theories_deps = Coq_lib.DB.requires coq_lib_db theory in
     let coqc_dir = (Super_context.context sctx).build_dir in
-    let mode = snd s.mode in
     let native_includes =
       Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string "coq.kernel")
       |> Result.map ~f:(fun lib -> Util.native_paths [ lib ])
     in
-    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~mode
+    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps
       ~native_includes s.buildable
   in
 
@@ -434,7 +433,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) =
 let install_rules ~sctx ~dir s =
   match s with
   | { Theory.package = None; _ } -> []
-  | { Theory.package = Some package; mode; _ } ->
+  | { Theory.package = Some package; buildable = { mode; _} ; _ } ->
     let loc = s.buildable.loc in
     let scope = SC.find_scope_by_dir sctx dir in
     let dir_contents = Dir_contents.get sctx ~dir in
@@ -502,8 +501,8 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
       let coq_lib_db = Scope.coq_libs scope in
       Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories
     in
-    let mode, native_includes = (Coq_mode.VoOnly, Ok Path.Set.empty) in
-    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps ~mode
+    let native_includes = Ok Path.Set.empty in
+    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
       ~native_includes s.buildable
   in
   let coq_module =

src/dune_rules/coq_stanza.ml

@@ -22,11 +22,14 @@ end
 
 let coq_syntax =
   Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)"
-    [ ((0, 1), `Since (1, 9)); ((0, 2), `Since (2, 5)) ]
+    [ ((0, 1), `Since (1, 9))
+    ; ((0, 2), `Since (2, 5))
+    ; ((0, 3), `Since (2, 8))]
 
 module Buildable = struct
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Coq_mode.t
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t
@@ -35,14 +38,17 @@ module Buildable = struct
   let decode =
     let+ loc = loc
     and+ flags = Ordered_set_lang.Unexpanded.field "flags"
+    and+ mode =
+      (Dune_lang.Syntax.since coq_syntax (0, 3) >>>
+       located (field "mode" ~default:Coq_mode.VoOnly Coq_mode.decode))
     and+ libraries =
       field "libraries" (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
-    { flags; libraries; theories; loc }
+    { flags; mode; libraries; theories; loc }
 end
 
 module Extraction = struct
@@ -79,7 +85,6 @@ module Theory = struct
     ; modules : Ordered_set_lang.t
     ; boot : bool
     ; enabled_if : Blang.t
-    ; mode : Loc.t * Coq_mode.t
     ; buildable : Buildable.t
     }
 
@@ -129,8 +134,6 @@ module Theory = struct
        and+ synopsis = field_o "synopsis" string
        and+ boot =
          field_b "boot" ~check:(Dune_lang.Syntax.since coq_syntax (0, 2))
-       and+ mode =
-         located (field "mode" ~default:Coq_mode.VoOnly Coq_mode.decode)
        and+ modules = modules_field "modules"
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode in
@@ -143,7 +146,6 @@ module Theory = struct
        ; boot
        ; buildable
        ; enabled_if
-       ; mode
        })
 
   type Stanza.t += T of t

src/dune_rules/coq_stanza.mli

@@ -4,6 +4,7 @@ open Import
 module Buildable : sig
   type t =
     { flags : Ordered_set_lang.Unexpanded.t
+    ; mode : Loc.t * Coq_mode.t
     ; libraries : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t
@@ -31,7 +32,6 @@ module Theory : sig
     ; modules : Ordered_set_lang.t
     ; boot : bool
     ; enabled_if : Blang.t
-    ; mode : Loc.t * Coq_mode.t
     ; buildable : Buildable.t
     }