Browse files

New -no-native-compiler flag for configure, globally disabling the na…

…tive

compiler (implemented on Matthieu's request).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 0a9dd11 commit 7321065b6dc1a2bba4dbb39d0570da3c62b30cfb mdenes committed Feb 24, 2013
Showing with 14 additions and 2 deletions.
  1. +1 −0 config/coq_config.mli
  2. +12 −1 configure
  3. +1 −1 lib/flags.ml
View
1 config/coq_config.mli
@@ -69,3 +69,4 @@ val wwwrefman : string
val wwwstdlib : string
val localwwwrefman : string
+val no_native_compiler : bool
View
13 configure
@@ -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
View
2 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

0 comments on commit 7321065

Please sign in to comment.