From 4554a860ffdcb30bf5711bd52f443484f9f950d9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Nov 2017 01:49:52 +0100 Subject: [kernel] Patch allowing to disable VM reduction. The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607]. --- config/coq_config.mli | 3 ++- configure.ml | 12 ++++++++---- kernel/nativeconv.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/vconv.ml | 2 +- lib/flags.ml | 2 +- lib/flags.mli | 4 ++-- library/library.ml | 4 ++-- pretyping/nativenorm.ml | 4 ++-- pretyping/vnorm.ml | 2 +- proofs/redexpr.ml | 15 +++++++++------ toplevel/coqtop.ml | 4 ++-- 12 files changed, 32 insertions(+), 24 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index 6a834a304..4a89794a5 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -80,4 +80,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 1ccb69106..490954eba 100644 --- a/configure.ml +++ b/configure.ml @@ -263,6 +263,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 @@ -329,6 +330,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, @@ -1003,9 +1006,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 @@ -1101,7 +1104,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 ddc8f8482..23b25756e 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -195,7 +195,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 c4afb8318..9f322db46 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -154,8 +154,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 553da2dc0..5d9dc4180 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 () -- cgit v1.2.3