aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-10 04:57:03 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-06 17:28:25 +0200
commit675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 (patch)
tree6007f1a5952496248c56823cba8c0b30325d2d42 /library
parentb0b9ec7c16c38dabc7c4279dbe4d578b74e91c19 (diff)
[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.
Diffstat (limited to 'library')
-rw-r--r--library/library.ml3
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,_) ->