From 1596cdbb2e97f2353236e35fb07be05efe6d1a84 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 11 Nov 2020 17:07:14 +0100
Subject: Configure default value of -native-compiler

This an implementation of point 2 of CEP coq/ceps#48
https://github.com/coq/ceps/pull/48

Option -native-compiler of the configure script now impacts the
default value of the option -native-compiler of coqc. The
-native-compiler option of the configure script is added an ondemand
value, which becomes the default, thus preserving the previous default
behavior.

The stdlib is still precompiled when configuring with -native-compiler
yes. It is not precompiled otherwise.
---
 toplevel/coqargs.ml  | 10 ++++------
 toplevel/coqargs.mli |  3 ++-
 2 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index c6ccf2a427..ec339c69c6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -36,7 +36,8 @@ let set_type_in_type () =
 
 type color = [`ON | `AUTO | `EMACS | `OFF]
 
-type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+type native_compiler = Coq_config.native_compiler =
+  NativeOff | NativeOn of { ondemand : bool }
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
@@ -96,10 +97,7 @@ type t = {
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
-let default_native =
-  if Coq_config.native_compiler
-  then NativeOn {ondemand=true}
-  else NativeOff
+let default_native = Coq_config.native_compiler
 
 let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
@@ -301,7 +299,7 @@ let get_native_compiler s =
     | ("no" | "off") -> NativeOff
     | _ ->
        error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
-  if not Coq_config.native_compiler && n <> NativeOff then
+  if Coq_config.native_compiler = NativeOff && n <> NativeOff then
     let () = warn_no_native_compiler s in
     NativeOff
   else
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c8634b7847..f6222e4ec4 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,7 +12,8 @@ type color = [`ON | `AUTO | `EMACS | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
-type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+type native_compiler = Coq_config.native_compiler =
+  NativeOff | NativeOn of { ondemand : bool }
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
-- 
cgit v1.2.3