[stm] [flags] Move document mode flags to the STM.

We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.

Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.

In particular:

== Added flags ==

- `Safe_typing.allow_delayed_constants`
  Allow delayed constants in the kernel.

- `Flags.record_aux_file`
  Output `Proof using` information from the kernel.

- `System.trust_file_cache`
  Assume that the file system won't change during our run.

== Deleted flags ==

- `Flags.compilation_mode`
- `Flags.batch_mode`

Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.

The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.

4 files changed, 15 insertions, 13 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d4be81c61..a178eb755 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -43,11 +43,8 @@ let with_extra_values o l f x =
 
 let boot = ref false
 let load_init = ref true
-let batch_mode = ref false
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-let compilation_mode = ref BuildVo
-let compilation_output_name = ref None
+let record_aux_file = ref false
 
 let test_mode = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 3024c6039..8ec2a8073 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -13,12 +13,9 @@
 val boot : bool ref
 val load_init : bool ref
 
-(* Will affect STM caching *)
-val batch_mode : bool ref
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-val compilation_mode : compilation_mode ref
-val compilation_output_name : string option ref
+(** Set by coqtop to tell the kernel to output to the aux file; will
+    be eventually removed by cleanups such as PR#1103 *)
+val record_aux_file : bool ref
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
diff --git a/lib/system.ml b/lib/system.ml
index 0b64b237d..4b5066ef4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -54,6 +54,8 @@ let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
   Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
 
+let trust_file_cache = ref true
+
 let exists_in_dir_respecting_case dir bf =
   let cache_dir dir =
     let contents = make_dir_table dir in
@@ -62,10 +64,10 @@ let exists_in_dir_respecting_case dir bf =
   let contents, fresh =
     try
       (* in batch mode, assume the directory content is still fresh *)
-      StrMap.find dir !dirmap, !Flags.batch_mode
+      StrMap.find dir !dirmap, !trust_file_cache
     with Not_found ->
       (* in batch mode, we are not yet sure the directory exists *)
-      if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+      if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true
       else cache_dir dir, true in
   StrSet.mem bf contents ||
     not fresh &&
@@ -80,7 +82,7 @@ let file_exists_respecting_case path f =
     let df = Filename.dirname f in
     (String.equal df "." || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
-  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
+  in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
diff --git a/lib/system.mli b/lib/system.mli
index 7281de97c..aa964abeb 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -54,6 +54,12 @@ val where_in_path_rex :
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+val trust_file_cache : bool ref
+(** [trust_file_cache] indicates whether we trust the underlying
+    mapped file-system not to change along the execution of Coq. This
+    assumption greatly speds up file search, but it is often
+    inconvenient in interactive mode *)
+
 val file_exists_respecting_case : string -> string -> bool
 
 (** {6 I/O functions } *)