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

1 files changed, 4 insertions, 2 deletions

diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index bccf560e1..410dcf0d4 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -17,7 +17,9 @@ val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : bool -> Stateid.t -> string -> Stateid.t
+val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
-val compile : bool -> string -> unit
+val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit