From 406717ce786a70e64b9043db45dd5a2add68f817 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 27 Jun 2016 23:49:09 +0200 Subject: [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" ``` --- configure.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'configure.ml') 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), " Specifies where is the Camlp5 library and tells to use it"; + "-flambda-opts", + Arg.String (fun s -> Prefs.flambda_flags := string_split ' ' s), + " Specifies additional flags to be passed to the flambda optimizing compiler"; "-arch", arg_string_option Prefs.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"; -- cgit v1.2.3 From 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Oct 2017 16:12:26 +0200 Subject: [flambda] [native] Pass `-Oclassic` to the native compiler. This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired. --- INSTALL | 12 +++++++----- config/coq_config.mli | 1 + configure.ml | 5 +++-- kernel/nativelib.ml | 15 +++++++++++++-- 4 files changed, 24 insertions(+), 9 deletions(-) (limited to 'configure.ml') diff --git a/INSTALL b/INSTALL index 808e76882..faac79f18 100644 --- a/INSTALL +++ b/INSTALL @@ -139,12 +139,14 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). 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 + 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. - Meanwhile, users with less powerful machines are recommended - to disable native compilation with `-native-compiler no`. + 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 diff --git a/config/coq_config.mli b/config/coq_config.mli index 885b3ef4c..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 diff --git a/configure.ml b/configure.ml index 3ba1986c0..ca7979fa1 100644 --- a/configure.ml +++ b/configure.ml @@ -1028,8 +1028,8 @@ let write_configml f = 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 - let pr_l n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) - 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)); @@ -1059,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; 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" -- cgit v1.2.3