[configure] Support for flambda flags.

We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:

```
./configure -flambda-opts "-O3 -unbox-closures"
```

7 files changed, 50 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 39f119e7c..6442d7c2c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,18 @@ Tactics
   profiling, and "Set NativeCompute Profile Filename" customizes
   the profile filename.
 
+Changes from 8.7+beta2 to 8.7.0
+===============================
+
+OCaml
+
+- Users can pass specific flags to the OCaml optimizing compiler by
+  -using the flambda-opts configure-time option.
+
+  Beware that compiling Coq with a flambda-enabled compiler is
+  experimental and may require large amounts of RAM and CPU, see
+  INSTALL for more details.
+
 Changes from 8.7+beta1 to 8.7+beta2
 ===================================
 
diff --git a/INSTALL b/INSTALL
index 676a1f8ea..808e76882 100644
--- a/INSTALL
+++ b/INSTALL
@@ -128,6 +128,24 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 	Use <command> to open an URL in a browser. %s must appear in <command>,
 	and will be replaced by the URL.
 
+-flambda-opts <flags>
+         This experimental option will pass specific user flags to the
+        OCaml optimizing compiler. In most cases, this option is used
+        to tweak the flambda backend; we recommend using
+
+        -flambda-opts `-O3 -unbox-closures`
+
+        but of course you are free to try with a different combination
+        of flags. You can read more at
+        https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+        Note that a regular build with a flambda-enabled compiler
+        requires a large amount of RAM (>= 10GiB) in one particular
+        file, see: https://caml.inria.fr/mantis/view.php?id=7630
+
+        Meanwhile, users with less powerful machines are recommended
+        to disable native compilation with `-native-compiler no`.
+
 5- Still in the root directory, do
 
 	make
diff --git a/Makefile.build b/Makefile.build
index 7b2e209a2..63aa41c6c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -196,7 +196,7 @@ OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
-OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
+OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
 DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils)
 
 # On MacOS, the binaries are signed, except our private ones
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 429d8811b..885b3ef4c 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -72,6 +72,8 @@ val gtk_platform : [`QUARTZ | `WIN32 | `X11]
 val has_natdynlink : bool
 val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
 
+val flambda_flags : string list
+
 val wwwcoq : string
 val wwwrefman : string
 val wwwbugtracker : string
diff --git a/configure.ml b/configure.ml
index fc2233f78..3ba1986c0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -260,6 +260,7 @@ module Prefs = struct
   let withdoc = ref false
   let geoproof = ref false
   let byteonly = ref false
+  let flambda_flags = ref []
   let debug = ref true
   let profile = ref false
   let annotate = ref false
@@ -305,6 +306,9 @@ let args_options = Arg.align [
   "-camlp5dir",
     Arg.String (fun s -> Prefs.camlp5dir:=Some s),
     "<dir> Specifies where is the Camlp5 library and tells to use it";
+  "-flambda-opts",
+    Arg.String (fun s -> Prefs.flambda_flags := string_split ' ' s),
+    "<flags> Specifies additional flags to be passed to the flambda optimizing compiler";
   "-arch", arg_string_option Prefs.arch,
     "<arch> Specifies the architecture";
   "-natdynlink", arg_bool Prefs.natdynlink,
@@ -949,7 +953,6 @@ let config_runtime () =
 
 let vmbyteflags = config_runtime ()
 
-
 (** * Summary of the configuration *)
 
 let print_summary () =
@@ -964,6 +967,7 @@ let print_summary () =
   pr "  OCaml version               : %s\n" caml_version;
   pr "  OCaml binaries in           : %s\n" camlbin;
   pr "  OCaml library in            : %s\n" camllib;
+  pr "  OCaml flambda flags         : %s\n" (String.concat " " !Prefs.flambda_flags);
   pr "  %s version              : %s\n"     capitalized_camlpX camlpX_version;
   pr "  %s binaries in          : %s\n"     capitalized_camlpX camlpXbindir;
   pr "  %s library in           : %s\n"     capitalized_camlpX camlpXlibdir;
@@ -1013,7 +1017,6 @@ let write_dbg_wrapper f =
 
 let _ = write_dbg_wrapper "dev/ocamldebug-coq"
 
-
 (** * Build the config/coq_config.ml file *)
 
 let write_configml f =
@@ -1024,7 +1027,8 @@ let write_configml f =
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
   let pr_p s o = pr "let %s = %S\n" s
-    (match o with Relative s -> s | Absolute s -> s)
+    (match o with Relative s -> s | Absolute s -> s) in
+  let pr_l n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l))
   in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
@@ -1065,6 +1069,7 @@ let write_configml f =
   pr "let gtk_platform = `%s\n" !idearchdef;
   pr_b "has_natdynlink" hasnatdynlink;
   pr_s "natdynlinkflag" natdynlinkflag;
+  pr_l "flambda_flags" !Prefs.flambda_flags;
   pr_i "vo_magic_number" vo_magic;
   pr_i "state_magic_number" state_magic;
   pr "let with_geoproof = ref %B\n" !Prefs.geoproof;
@@ -1160,6 +1165,8 @@ let write_makefile f =
   pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
+  (* XXX make this configurable *)
+  pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !Prefs.flambda_flags);
   pr "# Flags for GCC\n";
   pr "CFLAGS=%s\n\n" cflags;
   pr "# Compilation debug flags\n";
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b5e19f33c..8a2a2fffc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -40,6 +40,9 @@ Coq is compiled with `-safe-string` enabled and requires plugins to do
 the same. This means that code using `String` in an imperative way
 will fail to compile now. They should switch to `Bytes.t`
 
+Configure supports passing flambda options, use `-flambda-opts OPTS`
+with a flambda-enabled Ocaml to tweak the compilation to your taste.
+
 ### ML API
 
 - Added two functions for declaring hooks to be executed in reduction
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index c21db300a..950ed53cc 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -32,6 +32,8 @@ let supported_suffix f = match CUnix.get_extension f with
   | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
   | _ -> false
 
+let supported_flambda_option f = List.mem f Coq_config.flambda_flags
+
 (** From bytecode extension to native
 *)
 let native_suffix f = match CUnix.get_extension f with
@@ -187,6 +189,7 @@ let parse_args () =
 	end
 
     | ("-h"|"-help"|"--help") :: _ -> usage ()
+    | f :: rem when supported_flambda_option f -> parse (op,fl) rem
     | f :: rem when supported_suffix f -> parse (op,f::fl) rem
     | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
   in
@@ -275,7 +278,7 @@ let main () =
   let prog = if !opt then "opt" else "ocamlc" in
   (* Which arguments ? *)
   if !opt && !top then failwith "no custom toplevel in native code!";
-  let flags = if !opt then [] else Coq_config.vmbyteflags in
+  let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in
   let topstart = if !top then [ "topstart.cmo" ] else [] in
   let (modules, tolink) = files_to_link userfiles in
   let main_file = create_tmp_main_file modules in