diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | configure.ml | 4 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 4 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 10 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
12 files changed, 30 insertions, 22 deletions
diff --git a/Makefile.build b/Makefile.build index 018471b684..41220792d5 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 68fe7e1211..1916e82172 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 75a3fc4582..1f8bfc984f 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 d762a246e6..d6bd754783 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 c8e7f7afed..f87dd5c2c8 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 756d3b8515..1f68a88f3a 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 1ffa1a305c..0296d7b906 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 bd427ecd08..ac4e3b3064 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 d25f7e9150..f172bbdd1a 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 7e822dbe36..31e0a0e0ad 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 2df7c69c86..0a14a19507 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 f053839c70..94c1699c2a 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) -> |