Create (stdlib) syntax for Coq stanza

Fixes #6163

Author: LasseBlaauwbroek

src/dune_rules/coq_rules.ml

@@ -376,6 +376,7 @@ let setup_coqdep_rule ~sctx ~loc (cctx : _ Context.t) ~source_rule coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
     let file_flags = Context.coqc_file_flags cctx in
+    (if cctx.buildable.stdlib then [] else [Command.Args.A "-boot"]) @
     [ Command.Args.S file_flags
     ; As [ "-dyndep"; "opt" ]
     ; Dep (Path.build source)
@@ -399,6 +400,8 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
       |> List.map ~f:fst
     in
     let native_flags = Context.coqc_native_flags cctx in
+    (if cctx.buildable.stdlib then [] else
+       [Command.Args.A "-boot"; A "-noinit"]) @
     [ Command.Args.Hidden_targets objects_to
     ; native_flags
     ; S file_flags

src/dune_rules/coq_stanza.ml

@@ -25,6 +25,7 @@ let coq_syntax =
     ; ((0, 3), `Since (2, 8))
     ; ((0, 4), `Since (3, 3))
     ; ((0, 5), `Since (3, 4))
+    ; ((0, 6), `Since (3, 5))
     ]
 
 module Buildable = struct
@@ -34,6 +35,7 @@ module Buildable = struct
     ; mode : Loc.t * Coq_mode.t
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
+    ; stdlib : bool
     ; loc : Loc.t
     }
 
@@ -71,9 +73,13 @@ module Buildable = struct
       field "theories"
         (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode)
         ~default:[]
+    and+ stdlib =
+      field "stdlib"
+        (Dune_lang.Syntax.since coq_syntax (0, 6) >>> enum ["yes", true; "no", false])
+        ~default:true
     in
     let plugins = merge_plugins_libraries ~plugins ~libraries in
-    { flags; mode; coq_lang_version; plugins; theories; loc }
+    { flags; mode; coq_lang_version; plugins; theories; stdlib; loc }
 end
 
 module Extraction = struct

src/dune_rules/coq_stanza.mli

@@ -7,6 +7,7 @@ module Buildable : sig
     ; mode : Loc.t * Coq_mode.t
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml plugins *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
+    ; stdlib : bool
     ; loc : Loc.t
     }
 end