From 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 10 Jun 2017 04:57:03 +0200 Subject: [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. --- library/library.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library/library.ml') 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,_) -> -- cgit v1.2.3