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. --- lib/flags.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'lib/flags.ml') 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 -- cgit v1.2.3