From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: 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.
---
 toplevel/coqtop.ml | 5 ++++-
 toplevel/usage.ml  | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'toplevel')

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) ->
-- 
cgit v1.2.3