Disable precompilation for native_compute by default.

Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.

Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.

If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.

Failure to precompile is a hard error, since it is now explicitly required
by the user.

12 files changed, 30 insertions, 22 deletions

diff --git a/Makefile.build b/Makefile.build
index 018471b68..41220792d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -81,7 +81,7 @@ TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
 STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
-COQOPTS=$(COQ_XML) $(VM)
+COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
diff --git a/configure.ml b/configure.ml
index 68fe7e121..1916e8217 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1199,7 +1199,9 @@ let write_makefile f =
   pr "# Defining REVISION\n";
   pr "CHECKEDOUT=%s\n\n" vcs;
   pr "# Option to control compilation and installation of the documentation\n";
-  pr "WITHDOC=%s\n" (if withdoc then "all" else "no");
+  pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no");
+  pr "# Option to produce precompiled files for native_compute\n";
+  pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else "");
   close_out o;
   Unix.chmod f 0o444
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 75a3fc458..1f8bfc984 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -121,9 +121,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   aux 0
 
 let native_conv pb sigma env t1 t2 =
-  if !Flags.no_native_compiler then begin
-    let msg = "Native compiler is disabled, "^
-    "falling back to VM conversion test." in
+  if Coq_config.no_native_compiler then begin
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
     Pp.msg_warning (Pp.str msg);
     vm_conv pb env t1 t2
   end
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d762a246e..d6bd75478 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -772,9 +772,9 @@ let export ?except senv dir =
     }
   in
   let ast, values =
-    if !Flags.no_native_compiler then [], [||]
-    else
+    if !Flags.native_compiler then
       Nativelibrary.dump_library mp dir senv.env str
+    else [], [||]
   in
   let lib = {
     comp_name = dir;
diff --git a/lib/flags.ml b/lib/flags.ml
index c8e7f7afe..f87dd5c2c 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -206,8 +206,8 @@ let inline_level = ref default_inline_level
 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 Coq_config.no_native_compiler
+(* Native code compilation for conversion and normalization *)
+let native_compiler = ref false
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 let print_mod_uid = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 756d3b851..1f68a88f3 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -128,8 +128,8 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(* Disabling native code compilation for conversion and normalization *)
-val no_native_compiler : bool ref
+(* Native code compilation for conversion and normalization *)
+val native_compiler : bool ref
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 val print_mod_uid : bool ref
diff --git a/library/library.ml b/library/library.ml
index 1ffa1a305..0296d7b90 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -166,7 +166,7 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    if not !Flags.no_native_compiler then
+    if !Flags.native_compiler then
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
@@ -788,10 +788,10 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if not !Flags.no_native_compiler then
+    if !Flags.native_compiler then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
-        msg_error (str"Could not compile the library to native code. Skipping.")
+	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
     let () = msg_warning (str "Removed file " ++ str f') in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index bd427ecd0..ac4e3b306 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -378,8 +378,8 @@ and  nf_predicate env ind mip params v pT =
   | _, _ -> false, nf_type env v
 
 let native_norm env sigma c ty =  
-  if !Flags.no_native_compiler then
-    error "Native_compute reduction has been disabled"
+  if Coq_config.no_native_compiler then
+    error "Native_compute reduction has been disabled at configure time."
   else
   let penv = Environ.pre_env env in 
   (*
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d25f7e915..f172bbdd1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -30,9 +30,13 @@ let cbv_vm env sigma c =
   Vnorm.cbv_vm env c ctyp
 
 let cbv_native env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  let evars = Nativenorm.evars_of_evar_map sigma in
-  Nativenorm.native_norm env evars c ctyp
+  if Coq_config.no_native_compiler then
+    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    cbv_vm env sigma c
+  else
+    let ctyp = Retyping.get_type_of env sigma c in
+    let evars = Nativenorm.evars_of_evar_map sigma in
+    Nativenorm.native_norm env evars c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 7e822dbe3..31e0a0e0a 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -109,7 +109,7 @@ let parse_args () =
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-verbose-compat-notations"|"-no-compat-notations"
       |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2df7c69c8..0a14a1950 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -498,7 +498,10 @@ let parse_args arglist =
     |"-noinit"|"-nois" -> load_init := false
     |"-no-compat-notations" -> no_compat_ntn := true
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
-    |"-no-native-compiler" -> no_native_compiler := true
+    |"-native-compiler" ->
+      if Coq_config.no_native_compiler then
+	warning "Native compilation was disabled at configure time."
+      else native_compiler := true
     |"-notop" -> unset_toplevel_name ()
     |"-output-context" -> output_context := true
     |"-q" -> no_load_rc ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f053839c7..94c1699c2 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -71,7 +71,7 @@ let print_usage_channel co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
-\n  -no-native-compiler    disable the native_compute reduction machinery\
+\n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help              print this list of options\
 \n";
   List.iter (fun (name, text) ->