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/system.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 7281de97c..aa964abeb 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -54,6 +54,12 @@ val where_in_path_rex : val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val trust_file_cache : bool ref +(** [trust_file_cache] indicates whether we trust the underlying + mapped file-system not to change along the execution of Coq. This + assumption greatly speds up file search, but it is often + inconvenient in interactive mode *) + val file_exists_respecting_case : string -> string -> bool (** {6 I/O functions } *) -- cgit v1.2.3