diff options
| -rw-r--r-- | CHANGES | 12 | ||||
| -rw-r--r-- | INSTALL | 18 | ||||
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | config/coq_config.mli | 2 | ||||
| -rw-r--r-- | configure.ml | 13 | ||||
| -rw-r--r-- | dev/doc/changes.md | 3 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 5 |
7 files changed, 50 insertions, 5 deletions
@@ -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 =================================== @@ -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 |