From ad378471403767f5ecb75df25cf36194d89b1f23 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 27 Sep 2022 20:19:08 +0200
Subject: [PATCH] [coq] Generate flags correctly for `use_stdlib`

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
---
 src/dune_rules/coq_lib.ml     |  2 +-
 src/dune_rules/coq_rules.ml   | 12 ++++++++++--
 src/dune_rules/coq_stanza.ml  |  6 +++++-
 src/dune_rules/coq_stanza.mli |  1 +
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
index 03b65210752..5b14705931d 100644
--- a/src/dune_rules/coq_lib.ml
+++ b/src/dune_rules/coq_lib.ml
@@ -185,7 +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 = true 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
diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
index 842016012b3..a48f825c96a 100644
--- a/src/dune_rules/coq_rules.ml
+++ b/src/dune_rules/coq_rules.ml
@@ -112,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) -> (
@@ -127,6 +127,10 @@ 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
@@ -171,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
@@ -283,6 +288,7 @@ 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
@@ -315,6 +321,7 @@ module Context = struct
     ; ml_flags
     ; scope
     ; boot_type = Resolve.Memo.return Bootstrap.No_boot
+    ; use_stdlib
     ; profile_flags
     ; mode
     ; native_includes
@@ -325,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
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index 3d31c5c5e49..bfd006fed55 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/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
diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli
index 09a16244df7..04b1fbb0de0 100644
--- a/src/dune_rules/coq_stanza.mli
+++ b/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