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]. --- configure.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'configure.ml') 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"; -- cgit v1.2.3