diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 15:54:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 15:54:38 +0200 |
commit | f790c6ac8b16f71aae4868cbcad87a39f50727e3 (patch) | |
tree | 026665b355bf3c2712c3148b8e459e85ee10199a | |
parent | 16f169b3c756aa3c5cbc38eb13412ba23ae2937d (diff) | |
parent | 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (diff) |
Merge PR #540: [configure] Support for flambda flags.
-rw-r--r-- | CHANGES | 12 | ||||
-rw-r--r-- | INSTALL | 20 | ||||
-rw-r--r-- | Makefile.build | 2 | ||||
-rw-r--r-- | config/coq_config.mli | 3 | ||||
-rw-r--r-- | configure.ml | 16 | ||||
-rw-r--r-- | dev/doc/changes.md | 3 | ||||
-rw-r--r-- | kernel/nativelib.ml | 15 | ||||
-rw-r--r-- | tools/coqmktop.ml | 5 |
8 files changed, 68 insertions, 8 deletions
@@ -22,6 +22,18 @@ Tactics Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. +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,26 @@ 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 + + There is a known problem with certain OCaml versions and + `native_compute`, that will make compilation to require + a large amount of RAM (>= 10GiB) in some particular files. + + We recommend disabling native compilation (`-native-compiler no`) + with flambda unless you use a modern (>= 4.06.0) OCaml. + + c.f. https://caml.inria.fr/mantis/view.php?id=7630 + 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..8bc044c3a 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -49,6 +49,7 @@ val vmbyteflags : string list (* -custom/-dllib -lcoqrun *) val version : string (* version number of Coq *) val caml_version : string (* OCaml version used to compile Coq *) +val caml_version_nums : int list (* OCaml version used to compile Coq by components *) val date : string (* release date *) val compile_date : string (* compile date *) val vo_magic_number : int @@ -72,6 +73,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 3b6894bfc..a7acdf532 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,8 +1027,9 @@ 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) - in + (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 + let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); @@ -1055,6 +1059,7 @@ let write_configml f = pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; pr_s "caml_version" caml_version; + pr_li "caml_version_nums" caml_version_nums; pr_s "date" short_date; pr_s "compile_date" full_date; pr_s "arch" arch; @@ -1065,6 +1070,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 +1166,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/kernel/nativelib.ml b/kernel/nativelib.ml index 665ddf7a6..e9c0e171a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -74,7 +74,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); - let initial_args = + let initial_args = if Dynlink.is_native then ["opt"; "-shared"] else @@ -86,9 +86,20 @@ let call_compiler ?profile:(profile=false) ml_filename = else [] in + let flambda_args = + if Coq_config.caml_version_nums >= [4;3;0] then + (* We play safe for now, and use the native compiler + with -Oclassic, however it is likely that `native_compute` + users can benefit from tweaking here. + *) + ["-Oclassic"] + else + [] + in let args = initial_args @ - profile_args @ + profile_args @ + flambda_args @ ("-o"::link_filename ::"-rectypes" ::"-w"::"a" 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 |