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. --- stm/stm.mli | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 3f01fca01..ea8aecaed 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -10,6 +10,26 @@ open Names (** state-transaction-machine interface *) +(** The STM doc type determines some properties such as what + uncompleted proofs are allowed and recording of aux files. *) +type stm_doc_type = + | VoDoc of DirPath.t + | VioDoc of DirPath.t + | Interactive of DirPath.t + +(* Main initalization routine *) +type stm_init_options = { + doc_type : stm_doc_type; +(* + fb_handler : Feedback.feedback -> unit; + iload_path : (string list * string * bool) list; + require_libs : (Names.DirPath.t * string * bool option) list; + implicit_std : bool; +*) +} + +val init : stm_init_options -> unit + (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable -> @@ -83,9 +103,6 @@ val finish_tasks : string -> (* Id of the tip of the current branch *) val get_current_state : unit -> Stateid.t -(* Misc *) -val init : unit -> unit - (* This returns the node at that position *) val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option -- cgit v1.2.3