Merge PR #6264: [kernel] Patch allowing to disable VM reduction.

12 files changed, 32 insertions, 24 deletions

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 40661f428..1666df0bd 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -76,4 +76,5 @@ val wwwbugtracker : string
 val wwwstdlib : string
 val localwwwrefman : string
 
-val no_native_compiler : bool
+val bytecode_compiler : bool
+val native_compiler : bool
diff --git a/configure.ml b/configure.ml
index 2292913d5..06aa5e766 100644
--- a/configure.ml
+++ b/configure.ml
@@ -277,6 +277,7 @@ module Prefs = struct
   let debug = ref true
   let profile = ref false
   let annotate = ref false
+  let bytecodecompiler = 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
@@ -343,6 +344,8 @@ let args_options = Arg.align [
     " Add profiling information in the Coq executables";
   "-annotate", Arg.Set Prefs.annotate,
     " Dumps ml annotation files while compiling Coq";
+  "-bytecode-compiler", arg_bool Prefs.bytecodecompiler,
+    "(yes|no) Enable Coq's bytecode reduction machine (VM)";
   "-native-compiler", arg_bool Prefs.nativecompiler,
     "(yes|no) Compilation to native code for conversion and normalization";
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
@@ -1031,9 +1034,9 @@ let print_summary () =
   pr "  Documentation               : %s\n"
     (if withdoc then "All" else "None");
   pr "  Web browser                 : %s\n" browser;
-  pr "  Coq web site                : %s\n\n" !Prefs.coqwebsite;
-  if not !Prefs.nativecompiler then
-    pr "  Native compiler for conversion and normalization disabled\n\n";
+  pr "  Coq web site                : %s\n" !Prefs.coqwebsite;
+  pr "  Bytecode VM enabled         : %B\n" !Prefs.bytecodecompiler;
+  pr "  Native Compiler enabled     : %B\n\n" !Prefs.nativecompiler;
   if !Prefs.local then
     pr "  Local build, no installation...\n"
   else
@@ -1128,7 +1131,8 @@ let write_configml f =
   pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/");
   pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
-  pr_b "no_native_compiler" (not !Prefs.nativecompiler);
+  pr_b "bytecode_compiler" !Prefs.bytecodecompiler;
+  pr_b "native_compiler" !Prefs.nativecompiler;
 
   let core_src_dirs = [ "config"; "dev"; "kernel"; "library";
                         "engine"; "pretyping"; "interp"; "parsing"; "proofs";
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index a62a079da..9f9102f7d 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -154,7 +154,7 @@ let warn_no_native_compiler =
 
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
-  if Coq_config.no_native_compiler then begin
+  if not Coq_config.native_compiler then begin
     warn_no_native_compiler ();
     vm_conv cv_pb env t1 t2
   end
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e41bfc3c..5150ad411 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -858,7 +858,7 @@ let export ?except senv dir =
     }
   in
   let ast, symbols =
-    if !Flags.native_compiler then
+    if !Flags.output_native_objects then
       Nativelibrary.dump_library mp dir senv.env str
     else [], Nativecode.empty_symbols
   in
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 578a89371..3ef297b1f 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -204,4 +204,4 @@ let vm_conv cv_pb env t1 t2 =
     let univs = (univs, checked_universes) in
     let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
 
-let _ = Reduction.set_vm_conv vm_conv
+let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv
diff --git a/lib/flags.ml b/lib/flags.ml
index fb6e48ae2..644f66d02 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -161,7 +161,7 @@ let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
 (* Native code compilation for conversion and normalization *)
-let native_compiler = ref false
+let output_native_objects = 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 58415d6f5..000862b2c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -127,8 +127,8 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(** Native code compilation for conversion and normalization *)
-val native_compiler : bool ref
+(** When producing vo objects, also compile the native-code version *)
+val output_native_objects : 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 88470d121..868e26684 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -170,7 +170,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 Coq_config.no_native_compiler then
+    if Coq_config.native_compiler then
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
@@ -738,7 +738,7 @@ 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 !Flags.native_compiler then
+    if !Flags.output_native_objects then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
 	user_err Pp.(str "Could not compile the library to native code.")
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index dafe8cb26..79e0afa72 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -436,11 +436,11 @@ let stop_profiler m_pid =
   match profiler_platform() with
     "Unix (Linux)" -> stop_profiler_linux m_pid
   | _ -> ()
-     
+
 let native_norm env sigma c ty =
   let c = EConstr.Unsafe.to_constr c in
   let ty = EConstr.Unsafe.to_constr ty in
-  if Coq_config.no_native_compiler then
+  if not Coq_config.native_compiler then
     user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
   else
   let penv = Environ.pre_env env in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b5b8987e3..e395bdbc6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -365,4 +365,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
   Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
     ~catch_incon:true ~pb env sigma t1 t2
 
-let _ = Reductionops.set_vm_infer_conv vm_infer_conv
+let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6052ba367..9a5d4e154 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -25,8 +25,11 @@ open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  Vnorm.cbv_vm env sigma c ctyp
+  if Coq_config.bytecode_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Vnorm.cbv_vm env sigma c ctyp
+  else
+    compute env sigma c
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -34,12 +37,12 @@ let warn_native_compute_disabled =
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
 let cbv_native env sigma c =
-  if Coq_config.no_native_compiler then
-    (warn_native_compute_disabled ();
-     cbv_vm env sigma c)
-  else
+  if Coq_config.native_compiler then
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
+  else
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2fa9f0ab4..437b7b0ac 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -727,9 +727,9 @@ let parse_args arglist =
     |"-noinit"|"-nois" -> load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
-      if Coq_config.no_native_compiler then
+      if not Coq_config.native_compiler then
         warning "Native compilation was disabled at configure time."
-      else Flags.native_compiler := true
+      else Flags.output_native_objects := true
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
     |"-q" -> Coqinit.no_load_rc ()