[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.

3 files changed, 12 insertions, 6 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ad622b07d..fd024b215 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -683,12 +683,15 @@ let build_module_body params restype senv =
     with one extra component and some updated fields
     (constraints, required, etc) *)
 
+let allow_delayed_constants = ref false
+
 let propagate_senv newdef newenv newresolver senv oldsenv =
   let now_cst, later_cst = List.partition Future.is_val senv.future_cst in
   (* This asserts that after Paral-ITP, standard vo compilation is behaving
    * exctly as before: the same universe constraints are added to modules *)
-  if !Flags.compilation_mode = Flags.BuildVo &&
-     !Flags.async_proofs_mode = Flags.APoff then assert(later_cst = []);
+  if not !allow_delayed_constants && later_cst <> [] then
+    CErrors.anomaly ~label:"safe_typing"
+      Pp.(str "True Future.t were created for opaque constants even if -async-proofs is off");
   { oldsenv with
     env = newenv;
     modresolver = newresolver;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 752fdd793..f0f273f35 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -158,6 +158,10 @@ val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
     Mod_subst.delta_resolver safe_transformer
 
+(** Traditional mode: check at end of module that no future was
+    created. *)
+val allow_delayed_constants : bool ref
+
 (** The optional result type is given without its functorial part *)
 
 val end_module :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3f42c348f..0c0b910e1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -428,13 +428,12 @@ let build_constant_declaration kn env result =
             let expr =
               !suggest_proof_using (Constant.to_string kn)
                 env vars ids_typ context_ids in
-            if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars expr;
+            if !Flags.record_aux_file then record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
-        if !Flags.compilation_mode = Flags.BuildVo then
+        if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
@@ -614,7 +613,7 @@ let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
-  if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
+  if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with
     | Undef _ -> ()
     | Def _ -> ()