diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-08 23:13:53 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-09-19 14:31:09 +0200 |
commit | 0cc07dd290eb85bbb167dae2985cd1e468df882c (patch) | |
tree | 11dce67458a4fc042fc7c5f7ac49c1fa4feddf9e /configure.ml | |
parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) |
coq_makefile: make sure compile flags for Coq and coq_makefile are in sync
E.g. -safe-string is set by configure.ml and made available to
both make (via config/Makefile) and coq_makefile (via
config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
Diffstat (limited to 'configure.ml')
-rw-r--r-- | configure.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/configure.ml b/configure.ml index b5e456779..fc2233f78 100644 --- a/configure.ml +++ b/configure.ml @@ -263,10 +263,6 @@ module Prefs = struct let debug = ref true let profile = ref false let annotate = ref false - (* Note, disabling this should be OK, but be careful with the - sharing invariants. - *) - let safe_string = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false @@ -376,8 +372,9 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" else "" -let coq_safe_string = - if !Prefs.safe_string then "-safe-string" else "" +(* This variable can be overriden only for debug purposes, use with + care. *) +let coq_safe_string = "-safe-string" let cflags = "-Wall -Wno-unused -g -O2" @@ -512,19 +509,22 @@ let camltag = match caml_version_list with 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 *) -let coq_warn_flags = - let warnings = "-w +a-4-9-27-41-42-44-45-48-50" in - let errors = +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" +let coq_warn_error = if !Prefs.warn_error then "-warn-error +a" ^ (if caml_version_nums > [4;2;3] then "-56" else "") else "" - in - warnings ^ " " ^ errors +(* Flags used to compile Coq and plugins (via coq_makefile) *) +let caml_flags = + Printf.sprintf "-thread -rectypes %s %s %s" coq_warnings coq_annotate_flag coq_safe_string +(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *) +let coq_caml_flags = + coq_warn_error (** * CamlpX configuration *) @@ -1050,6 +1050,7 @@ let write_configml f = pr_s "camlp4lib" camlpXlibdir; pr_s "camlp4compat" camlp4compat; pr_s "cflags" cflags; + pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; @@ -1156,7 +1157,7 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string; + pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; |