From 19f5b6a7d467f75b334e769ebe30cf6459c86855 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Sep 2018 00:32:04 +0200
Subject: [configure] Don't die if the build sandbox doesn't have the stdlib.

Dune calls `./configure` under the build sandbox, which, if the voboot
target has not been executed will contain only the OCaml parts of Coq.

Thus, we make configure not to die if the `plugins` directory is not
present.

This makes Dune usable without calling the `voboot` target.
---
 configure.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 1b0c592e46..d010b44e54 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1239,7 +1239,10 @@ let write_configml f =
   pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
   pr "\nlet plugins_dirs = [\n";
 
-  let plugins = Sys.readdir "plugins" in
+  let plugins =
+    try Sys.readdir "plugins"
+    with _ -> [||]
+  in
   Array.sort compare plugins;
   Array.iter
     (fun f ->
-- 
cgit v1.2.3


From 615c29be047eafac1ec1a9a853afe5a577873771 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Sep 2018 00:41:39 +0200
Subject: [configure] [dune] Don't force the Dune user to set envars.

In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.

However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.

While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
---
 Makefile.dune |  3 ---
 config/dune   |  2 +-
 configure.ml  | 17 ++++++++++++++---
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/Makefile.dune b/Makefile.dune
index cac1bdd6a1..81afa5bb91 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -7,9 +7,6 @@
 # DUNEOPT=--display=short
 
 BUILD_CONTEXT=_build/default
-COQ_CONFIGURE_PREFIX?=_build/install/default
-
-export COQ_CONFIGURE_PREFIX
 
 help:
 	@echo "Welcome to Coq's Dune-based build system. Targets are:"
diff --git a/config/dune b/config/dune
index cf2bc71363..ce87a7816d 100644
--- a/config/dune
+++ b/config/dune
@@ -10,4 +10,4 @@
  (targets coq_config.ml)
  (mode fallback)
  (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
- (action (chdir %{project_root} (run %{ocaml} configure.ml -native-compiler no))))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
diff --git a/configure.ml b/configure.ml
index d010b44e54..da6a6f8cbf 100644
--- a/configure.ml
+++ b/configure.ml
@@ -242,6 +242,7 @@ type ide = Opt | Byte | No
 type preferences = {
   prefix : string option;
   local : bool;
+  interactive : bool;
   vmbyteflags : string option;
   custom : bool option;
   bindir : string option;
@@ -279,6 +280,7 @@ module Profiles = struct
 let default = {
   prefix = None;
   local = false;
+  interactive = true;
   vmbyteflags = None;
   custom = None;
   bindir = None;
@@ -331,6 +333,11 @@ end
 
 let prefs = ref Profiles.default
 
+(* Support don't ask *)
+let cprintf x =
+  if !prefs.interactive
+  then cprintf x
+  else Printf.ifprintf stdout x
 
 let get_bool = function
   | "true" | "yes" | "y" | "all" -> true
@@ -366,6 +373,8 @@ let args_options = Arg.align [
     "<dir> Set installation directory to <dir>";
   "-local", arg_set (fun p local -> { p with local }),
     " Set installation directory to the current source tree";
+  "-no-ask", arg_clear (fun p interactive -> { p with interactive }),
+    " Don't ask questions / print variables during configure [questions will be filled with defaults]";
   "-vmbyteflags", arg_string_option (fun p vmbyteflags -> { p with vmbyteflags }),
     "<flags> Comma-separated link flags for the VM of coqtop.byte";
   "-custom", arg_set_option (fun p custom -> { p with custom }),
@@ -1043,7 +1052,9 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout
       | None ->
         begin
           try Some (Sys.getenv "COQ_CONFIGURE_PREFIX")
-          with Not_found -> None
+          with
+          | Not_found when !prefs.interactive -> None
+          | Not_found -> Some "_build/default/install"
         end
       | p -> p
     in match uservalue, env_prefix with
@@ -1144,8 +1155,8 @@ let print_summary () =
   pr "*Warning* To compile the system for a new architecture\n";
   pr "          don't forget to do a 'make clean' before './configure'.\n"
 
-let _ = print_summary ()
-
+let _ =
+  if !prefs.interactive then print_summary ()
 
 (** * Build the dev/ocamldebug-coq file *)
 
-- 
cgit v1.2.3