aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-09-08 23:13:53 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-09-19 14:31:09 +0200
commit0cc07dd290eb85bbb167dae2985cd1e468df882c (patch)
tree11dce67458a4fc042fc7c5f7ac49c1fa4feddf9e /configure.ml
parentb1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (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.ml25
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";