diff options
| -rw-r--r-- | .travis.yml | 2 | ||||
| -rw-r--r-- | CHANGES | 12 | ||||
| -rw-r--r-- | INSTALL | 20 | ||||
| -rw-r--r-- | Makefile.build | 18 | ||||
| -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-- | doc/faq/FAQ.tex | 15 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 15 | ||||
| -rw-r--r-- | lib/minisys.ml | 14 | ||||
| -rw-r--r-- | lib/segmenttree.ml | 8 | ||||
| -rw-r--r-- | lib/segmenttree.mli | 8 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 3 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 5 |
14 files changed, 114 insertions, 28 deletions
diff --git a/.travis.yml b/.travis.yml index 656c9e1874..c380384524 100644 --- a/.travis.yml +++ b/.travis.yml @@ -146,7 +146,7 @@ matrix: - brew update --debug --verbose - brew install opam gnu-time - - if: NOT type IS pull_request + - if: NOT (type = pull_request) os: osx env: - TEST_TARGET="" @@ -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 7b2e209a25..991942bf0a 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 @@ -430,14 +430,18 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # Remember to update the dependencies below when you add files! -COQDEPBOOTSRC := lib/minisys.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ +COQDEPBOOTSRC := \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo lib/segmenttree.cmo : lib/segmenttree.cmi lib/segmenttree.cmx : lib/segmenttree.cmi -lib/unicode.cmo : lib/unicodetable.cmo lib/segmenttree.cmi lib/unicode.cmi -lib/unicode.cmx : lib/unicodetable.cmx lib/segmenttree.cmx lib/unicode.cmi +lib/unicodetable.cmo : lib/segmenttree.cmo +lib/unicodetable.cmx : lib/segmenttree.cmx +lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi +lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi +lib/minisys.cmo : lib/unicode.cmo +lib/minisys.cmx : lib/unicode.cmx tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi @@ -455,8 +459,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo lib/minisys.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ +COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ tools/coqdep.cmo diff --git a/config/coq_config.mli b/config/coq_config.mli index 429d8811bd..8bc044c3ae 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 3b6894bfcb..a7acdf5320 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 b5e19f33c3..8a2a2fffc6 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/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 213fb03137..541d39501b 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2413,15 +2413,14 @@ You can use {\tt coq\_tex}. \Question{How can I cite the {\Coq} reference manual?} -You can use this bibtex entry: +You can use this bibtex entry (to adapt to the appropriate version): \begin{verbatim} -@Manual{Coq:manual, - title = {The Coq proof assistant reference manual}, - author = {\mbox{The Coq development team}}, - organization = {LogiCal Project}, - note = {Version 8.2}, - year = {2009}, - url = "http://coq.inria.fr" +@manual{Coq:manual, + author = {{Coq} {Development} {Team}, The}, + title = {The {Coq} Proof Assistant Reference Manual, version 8.7}, + month = Oct, + year = {2017}, + url = {http://coq.inria.fr} } \end{verbatim} diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 665ddf7a65..e9c0e171ac 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/lib/minisys.ml b/lib/minisys.ml index 706f0430c3..389b18ad4e 100644 --- a/lib/minisys.ml +++ b/lib/minisys.ml @@ -36,10 +36,15 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames +(* Note: this test is possibly used for Coq module/file names but also for + OCaml filenames, whose syntax as of today is more restrictive for + module names (only initial letter then letter, digits, _ or quote), + but more permissive (though disadvised) for file names *) + let ok_dirname f = not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) + not (List.mem f !skipped_dirnames) && + match Unicode.ident_refutation f with None -> true | _ -> false (* Check directory can be opened *) @@ -55,10 +60,11 @@ let exists_dir dir = let apply_subdir f path name = (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) (* as well as skipped files like CVS, ... *) - if ok_dirname name then + let base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base then let path = if path = "." then name else path//name in match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with - | Unix.S_DIR -> f (FileDir (path,name)) + | Unix.S_DIR when name = base -> f (FileDir (path,name)) | Unix.S_REG -> f (FileRegular name) | _ -> () diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml index 9ce348a0bd..d0ded4cb59 100644 --- a/lib/segmenttree.ml +++ b/lib/segmenttree.ml @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli index 3258537b99..e274a6fdc8 100644 --- a/lib/segmenttree.mli +++ b/lib/segmenttree.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4a9d871fd3..2feaaa04cd 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -122,7 +122,8 @@ let generate_makefile oc conf_file local_file args project = Envars.coqlib () ^ template in let s = read_whole_file makefile_template in let s = List.fold_left - (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s + (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) + (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s [ "@CONF_FILE@", conf_file; "@LOCAL_FILE@", local_file; "@COQ_VERSION@", Coq_config.version; diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index c21db300ad..950ed53ccf 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 |