aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES12
-rw-r--r--INSTALL18
-rw-r--r--Makefile.build2
-rw-r--r--config/coq_config.mli2
-rw-r--r--configure.ml13
-rw-r--r--dev/doc/changes.md3
-rw-r--r--tools/coqmktop.ml5
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