[coq] Fix composition of boot library when it has plugins, add field to allow libraries to opt out of stdlib

src/dune_rules/coq_lib.ml

@@ -50,6 +50,8 @@ include struct
     ; boot : t option Resolve.t
     ; id : Id.t
     ; implicit : bool (* Only useful for the stdlib *)
+    ; use_stdlib : bool
+          (* whether this theory uses the stdlib, eventually set to false for all libs *)
     ; src_root : Path.Build.t
     ; obj_root : Path.Build.t
     ; theories : (Loc.t * t) list Resolve.t
@@ -183,6 +185,7 @@ module DB = struct
         let open Memo.O in
         let* boot = if s.boot then Resolve.Memo.return None else boot coq_db in
         let allow_private_deps = Option.is_none s.package in
+        let use_stdlib = s.buildable.use_stdlib in
         let+ libraries =
           Resolve.Memo.List.map s.buildable.plugins ~f:(fun (loc, lib) ->
               let open Resolve.Memo.O in
@@ -237,19 +240,27 @@ module DB = struct
                   | Some _ -> Resolve.Memo.return ()
                   | None -> Error.private_deps_not_allowed ~loc theory_name
               in
-
               (loc, theory))
         in
+        let theories =
+          let open Resolve.O in
+          let* boot = boot in
+          match boot with
+          | Some boot when use_stdlib && not s.boot ->
+            let+ theories = theories in
+            (boot.loc, boot) :: theories
+          | Some _ | None -> theories
+        in
         let map_error x =
           let human_readable_description () = Id.pp id in
           Resolve.push_stack_frame ~human_readable_description x
         in
         let theories = map_error theories in
         let libraries = map_error libraries in
-
         { loc = s.buildable.loc
         ; boot
         ; id
+        ; use_stdlib
         ; implicit = s.boot
         ; obj_root = dir
         ; src_root = dir

src/dune_rules/coq_rules.ml

@@ -55,6 +55,49 @@ let resolve_program sctx ~loc ~dir prog =
   Super_context.resolve_program ~dir sctx prog ~loc:(Some loc)
     ~hint:"opam install coq"
 
+module Coq_plugin = struct
+  (* compute include flags and mlpack rules *)
+  let setup_ml_deps libs theories =
+    (* Pair of include flags and paths to mlpack *)
+    let libs =
+      let open Resolve.Memo.O in
+      let* theories = theories in
+      let* theories =
+        Resolve.Memo.lift
+        @@ Resolve.List.concat_map ~f:Coq_lib.libraries theories
+      in
+      let libs = libs @ theories in
+      Lib.closure ~linking:false (List.map ~f:snd libs)
+    in
+    let flags =
+      Resolve.Memo.args (Resolve.Memo.map libs ~f:Util.include_flags)
+    in
+    let open Action_builder.O in
+    ( flags
+    , let* libs = Resolve.Memo.read libs in
+      (* If the mlpack files don't exist, don't fail *)
+      Action_builder.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)
+    )
+
+  let of_buildable ~lib_db ~theories_deps (buildable : Coq_stanza.Buildable.t) =
+    let res =
+      let open Resolve.Memo.O in
+      let+ libs =
+        Resolve.Memo.List.map buildable.plugins ~f:(fun (loc, name) ->
+            let+ lib = Lib.DB.resolve lib_db (loc, name) in
+            (loc, lib))
+      in
+      setup_ml_deps libs theories_deps
+    in
+    let ml_flags = Resolve.Memo.map res ~f:fst in
+    let mlpack_rule =
+      let open Action_builder.O in
+      let* _, mlpack_rule = Resolve.Memo.read res in
+      mlpack_rule
+    in
+    (ml_flags, mlpack_rule)
+end
+
 module Bootstrap = struct
   (* the internal boot flag determines if the Coq "standard library" is being
      built, in case we need to explicitly tell Coq where the build artifacts are
@@ -69,7 +112,7 @@ module Bootstrap = struct
         (** We are compiling the prelude itself
             [should be replaced with (per_file ...) flags] *)
 
-  let get ~boot_lib ~wrapper_name coq_module =
+  let get_for_module ~boot_lib ~wrapper_name coq_module =
     match boot_lib with
     | None -> No_boot
     | Some (_loc, lib) -> (
@@ -84,11 +127,15 @@ module Bootstrap = struct
       | false -> Bootstrap lib
       | true -> Bootstrap_prelude)
 
+  let get ~use_stdlib ~boot_lib ~wrapper_name coq_module =
+    if not use_stdlib then Bootstrap_prelude
+    else get_for_module ~boot_lib ~wrapper_name coq_module
+
   let boot_lib_flags ~coqdoc lib : _ Command.Args.t =
     let dir = Coq_lib.src_root lib in
     S
       (if coqdoc then [ A "--coqlib"; Path (Path.build dir) ]
-      else [ A "-boot"; Util.theory_coqc_flag lib ])
+      else [ A "-boot" ])
 
   let flags ~coqdoc t : _ Command.Args.t =
     match t with
@@ -128,6 +175,7 @@ module Context = struct
     ; ml_flags : 'a Command.Args.t Resolve.Memo.t
     ; scope : Scope.t
     ; boot_type : Bootstrap.t Resolve.Memo.t
+    ; use_stdlib : bool
     ; profile_flags : string list Action_builder.t
     ; mode : Coq_mode.t
     ; native_includes : Path.Set.t Resolve.t
@@ -218,26 +266,6 @@ module Context = struct
     ; S file_flags
     ]
 
-  (* compute include flags and mlpack rules *)
-  let setup_ml_deps libs theories =
-    (* Pair of include flags and paths to mlpack *)
-    let libs =
-      let open Resolve.Memo.O in
-      let* theories = theories in
-      let* theories =
-        Resolve.Memo.lift
-        @@ Resolve.List.concat_map ~f:Coq_lib.libraries theories
-      in
-      let libs = libs @ theories in
-      Lib.closure ~linking:false (List.map ~f:snd libs)
-    in
-    ( Resolve.Memo.args (Resolve.Memo.map libs ~f:Util.include_flags)
-    , let open Action_builder.O in
-      let* libs = Resolve.Memo.read libs in
-      (* If the mlpack files don't exist, don't fail *)
-      Action_builder.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)
-    )
-
   let directories_of_lib ~sctx lib =
     let name = Coq_lib.name lib in
     let dir = Coq_lib.src_root lib in
@@ -260,28 +288,14 @@ module Context = struct
   let create ~coqc_dir sctx ~dir ~wrapper_name ~theories_deps ~theory_dirs
       (buildable : Buildable.t) =
     let loc = buildable.loc in
+    let use_stdlib = buildable.use_stdlib in
     let rr = resolve_program sctx ~dir ~loc in
     let* expander = Super_context.expander sctx ~dir in
     let* scope = Scope.DB.find_by_dir dir in
     let lib_db = Scope.libs scope in
     (* ML-level flags for depending libraries *)
     let ml_flags, mlpack_rule =
-      let res =
-        let open Resolve.Memo.O in
-        let+ libs =
-          Resolve.Memo.List.map buildable.plugins ~f:(fun (loc, name) ->
-              let+ lib = Lib.DB.resolve lib_db (loc, name) in
-              (loc, lib))
-        in
-        setup_ml_deps libs theories_deps
-      in
-      let ml_flags = Resolve.Memo.map res ~f:fst in
-      let mlpack_rule =
-        let open Action_builder.O in
-        let* _, mlpack_rule = Resolve.Memo.read res in
-        mlpack_rule
-      in
-      (ml_flags, mlpack_rule)
+      Coq_plugin.of_buildable ~theories_deps ~lib_db buildable
     in
     let mode = select_native_mode ~sctx ~buildable in
     let* native_includes =
@@ -307,6 +321,7 @@ module Context = struct
     ; ml_flags
     ; scope
     ; boot_type = Resolve.Memo.return Bootstrap.No_boot
+    ; use_stdlib
     ; profile_flags
     ; mode
     ; native_includes
@@ -317,7 +332,8 @@ module Context = struct
     let boot_type =
       let open Resolve.Memo.O in
       let+ boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in
-      Bootstrap.get ~boot_lib ~wrapper_name:t.wrapper_name coq_module
+      Bootstrap.get ~use_stdlib:t.use_stdlib ~boot_lib
+        ~wrapper_name:t.wrapper_name coq_module
     in
     { t with boot_type }
 end

src/dune_rules/coq_stanza.ml

@@ -32,6 +32,7 @@ module Buildable = struct
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
     ; mode : Loc.t * Coq_mode.t
+    ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml libraries *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t
@@ -60,6 +61,9 @@ module Buildable = struct
       located
         (field "mode" ~default
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
+    and+ use_stdlib =
+      field ~default:true "stdlib"
+        Dune_lang.Decoder.(enum [ ("yes", true); ("no", false) ])
     and+ libraries =
       field "libraries" ~default:[]
         (Dune_sexp.Syntax.deprecated_in coq_syntax (0, 5)
@@ -73,7 +77,7 @@ module Buildable = struct
         ~default:[]
     in
     let plugins = merge_plugins_libraries ~plugins ~libraries in
-    { flags; mode; coq_lang_version; plugins; theories; loc }
+    { flags; mode; use_stdlib; coq_lang_version; plugins; theories; loc }
 end
 
 module Extraction = struct

src/dune_rules/coq_stanza.mli

@@ -5,6 +5,7 @@ module Buildable : sig
     { flags : Ordered_set_lang.Unexpanded.t
     ; coq_lang_version : Dune_sexp.Syntax.Version.t
     ; mode : Loc.t * Coq_mode.t
+    ; use_stdlib : bool
     ; plugins : (Loc.t * Lib_name.t) list  (** ocaml plugins *)
     ; theories : (Loc.t * Coq_lib_name.t) list  (** coq libraries *)
     ; loc : Loc.t

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.4)
+
+(using coq 0.5)

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/dune

@@ -0,0 +1,4 @@
+(library
+ (name boot_plugin)
+ (public_name coq-boot.boot_plugin))
+

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/main.ml

@@ -0,0 +1 @@
+let () = Format.eprintf "plugin loaded@\n%!"

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/Init/Prelude.v

@@ -0,0 +1,2 @@
+Declare ML Module "boot_plugin:coq-boot.boot_plugin".
+Inductive AnotherBegining := Of | The | Universe.

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/dune

@@ -0,0 +1,7 @@
+(coq.theory
+ (name Coq)
+ (boot)
+ (package coq-boot)
+ (plugins coq-boot.boot_plugin))
+
+(include_subdirs qualified)

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune

@@ -0,0 +1,5 @@
+(coq.theory
+ (name User)
+ (package coq-user))
+
+

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.4)
+
+(using coq 0.5)

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/user.v

@@ -0,0 +1 @@
+Definition from_boot : AnotherBegining := Universe.

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.4)

test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/run.t

@@ -0,0 +1,5 @@
+Testing composition with a boot library with plugins
+
+  $ dune build
+  plugin loaded
+  plugin loaded