aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-24 13:43:23 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:42:01 +0200
commita77734ad64fff2396b161308099923037fb5d8a1 (patch)
tree1b0dbbbfa373e9e8219214bfee054769f8a2f85a /configure.ml
parent87910d7be9bd50de4db80f70c6e287c7c7994460 (diff)
Enable more warnings, and add -warn-error configure flag
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml31
1 files changed, 30 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index befd67262..5330da7d3 100644
--- a/configure.ml
+++ b/configure.ml
@@ -270,6 +270,7 @@ module Prefs = struct
let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
let coqwebsite = ref "http://coq.inria.fr/"
let force_caml_version = ref false
+ let warn_error = ref false
end
(* TODO : earlier any option -foo was also available as --foo *)
@@ -352,6 +353,8 @@ let args_options = Arg.align [
" URL of the coq website";
"-force-caml-version", Arg.Set Prefs.force_caml_version,
" Force OCaml version";
+ "-warn-error", Arg.Set Prefs.warn_error,
+ " Make OCaml warnings into errors";
]
let parse_args () =
@@ -511,6 +514,32 @@ let camltag = match caml_version_list with
| x::y::_ -> "OCAML"^x^y
| _ -> assert false
+(** Explanation of disabled warnings:
+ 3: deprecated warning (not error for non minimum supported ocaml)
+ 4: fragile pattern matching: too common in the code and too annoying to avoid in general
+ 9: missing fields in a record pattern: too common in the code and not worth the bother
+ 27: innocuous unused variable: innocuous
+ 41: ambiguous constructor or label: too common
+ 42: disambiguated counstructor or label: too common
+ 44: "open" shadowing already defined identifier: too common, especially when some are aliases
+ 45: "open" shadowing a label or constructor: see 44
+ 48: implicit elimination of optional arguments: too common
+ 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 =
+ if !Prefs.warn_error
+ then "-warn-error +a"
+ ^ (if caml_version_nums > [4;2;3]
+ then "-3-56"
+ else "")
+ else ""
+ in
+ warnings ^ " " ^ errors
+
+
(** * CamlpX configuration *)
@@ -1103,7 +1132,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\n" coq_annotate_flag coq_safe_string;
+ pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string;
pr "# User compilation flag\n";
pr "USERFLAGS=\n\n";
pr "# Flags for GCC\n";