diff options
| author |  mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-24 11:56:32 +0000 |
|---|---|---|
| committer | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-24 11:56:32 +0000 |
| commit | 7321065b6dc1a2bba4dbb39d0570da3c62b30cfb (patch) | |
| tree | d1f274f6e417820754cf656f03ca37081e725dda | |
| parent | 0a9dd11b1500455bdc98ad5769e3a572a5705d8f (diff) | |
New -no-native-compiler flag for configure, globally disabling the native
compiler (implemented on Matthieu's request).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 13 | ||||
| -rw-r--r-- | lib/flags.ml | 2 |
3 files changed, 14 insertions, 2 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index f2861f12a..f16ffbe51 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -69,3 +69,4 @@ val wwwrefman : string val wwwstdlib : string val localwwwrefman : string +val no_native_compiler : bool @@ -89,7 +89,9 @@ usage () { echo "-typerex" printf "\tCompiles Coq using typerex wrapper\n" echo "-makecmd <command>" - printf "\tName of GNU Make command.\n" + printf "\tName of GNU Make command\n" + echo "-no-native-compiler" + printf "\tDisables compilation to native code for conversion and normalization\n" } @@ -142,6 +144,7 @@ with_doc_spec=no force_caml_version=no force_caml_version_spec=no usecamlp5=yes +no_native_compiler=false # Parse command-line arguments @@ -249,6 +252,7 @@ while : ; do -profile|--profile) coq_profile_flag=-p;; -annotate|--annotate) coq_annotate_flag=-dtypes;; -typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;; + -no-native-compiler|--no-native-compiler) no_native_compiler=true;; -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) force_caml_version_spec=yes force_caml_version=yes;; @@ -901,6 +905,11 @@ echo " Web browser : $BROWSER" echo " Coq web site : $WWWCOQ" echo "" +if test "$no_native_compiler" = "true"; then +echo " Native compiler for conversion and normalization disabled" +echo "" +fi + if test "$local" = "true"; then echo " Local build, no installation..." echo "" @@ -1051,6 +1060,8 @@ let wwwcoq = "$WWWCOQ" let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/" let localwwwrefman = "file:/" ^ docdir ^ "html/refman" +let no_native_compiler = $no_native_compiler + END_OF_COQ_CONFIG diff --git a/lib/flags.ml b/lib/flags.ml index 727e2184b..4ad929052 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -168,7 +168,7 @@ let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level (* Disabling native code compilation for conversion and normalization *) -let no_native_compiler = ref false +let no_native_compiler = ref Coq_config.no_native_compiler (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false |