[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, 2 insertions, 1 deletions

diff --git a/library/library.ml b/library/library.ml
index 1da2c591d..e2832ecdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -683,7 +683,8 @@ let error_recursively_dependent_library dir =
 let save_library_to ?todo dir f otab =
   let except = match todo with
     | None ->
-        assert(!Flags.compilation_mode = Flags.BuildVo);
+        (* XXX *)
+        (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
         assert(Filename.check_suffix f ".vo");
         Future.UUIDSet.empty
     | Some (l,_) ->