aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-06 14:15:19 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-06 14:15:19 +0100
commitb1d56e48b2453814a5d2898688fbc7c5d29d32fa (patch)
tree4fc10644e5db337a6d931ad1a26974a34399b97e
parent5ac5ba83b7527f29b6a00c51806d4842b2e22e44 (diff)
parentc13213ced52f8f1383d5bed9c5a826d111603318 (diff)
Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.
-rw-r--r--dev/doc/changes.md11
-rw-r--r--stm/stm.ml33
-rw-r--r--stm/stm.mli21
-rw-r--r--toplevel/coqinit.ml22
-rw-r--r--toplevel/coqinit.mli7
-rw-r--r--toplevel/coqtop.ml35
6 files changed, 97 insertions, 32 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e616bd566..aef62b009 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -58,6 +58,17 @@ Declaration of printers for arguments used only in vernac command
happen. An alternative is to register the corresponding argument as
a value, using "Geninterp.register_val0 wit None".
+### STM API
+
+The STM API has seen a general overhaul. The main change is the
+introduction of a "Coq document" type, which all operations now take
+as a parameter. This effectively functionalize the STM API and will
+allow in the future to handle several documents simultaneously.
+
+The main remarkable point is that key implicit global parameters such
+as load-paths and required modules are now arguments to the document
+creation function. This helps enforcing some key invariants.
+
### XML IDE Protocol
- Before 8.8, `Query` only executed the first command present in the
diff --git a/stm/stm.ml b/stm/stm.ml
index 1b649194d..b5848c662 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2532,16 +2532,28 @@ end (* }}} *)
(********************************* STM API ************************************)
(******************************************************************************)
+(* Main initalization routine *)
type stm_init_options = {
+ (* The STM will set some internal flags differently depending on the
+ specified [doc_type]. This distinction should dissappear at some
+ some point. *)
doc_type : stm_doc_type;
+
+ (* Initial load path in scope for the document. Usually extracted
+ from -R options / _CoqProject *)
+ iload_path : Mltop.coq_path list;
+
+ (* Require [require_libs] before the initial state is
+ ready. Parameters follow [Library], that is to say,
+ [lib,prefix,import_export] means require library [lib] from
+ optional [prefix] and [import_export] if [Some false/Some true]
+ is used. *)
require_libs : (string * string option * bool option) list;
+
+ (* STM options that apply to the current document. *)
stm_options : AsyncOpts.stm_opt;
-(*
- fb_handler : Feedback.feedback -> unit;
- iload_path : (string list * string * bool) list;
- implicit_std : bool;
-*)
}
+(* fb_handler : Feedback.feedback -> unit; *)
(*
let doc_type_module_name (std : stm_doc_type) =
@@ -2554,7 +2566,7 @@ let init_core () =
if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
State.register_root_state ()
-let new_doc { doc_type ; stm_options; require_libs } =
+let new_doc { doc_type ; iload_path; require_libs; stm_options } =
let load_objs libs =
let rq_file (dir, from, exp) =
@@ -2572,6 +2584,11 @@ let new_doc { doc_type ; stm_options; require_libs } =
let doc = VCS.init doc_type Stateid.initial in
+ (* Set load path; important, this has to happen before we declare
+ the library below as [Declaremods/Library] will infer the module
+ name by looking at the load path! *)
+ List.iter Mltop.add_coq_path iload_path;
+
begin match doc_type with
| Interactive ln ->
Safe_typing.allow_delayed_constants := true;
@@ -2588,9 +2605,11 @@ let new_doc { doc_type ; stm_options; require_libs } =
VCS.set_ldir ldir;
set_compilation_hints ln
end;
+
+ (* Import initial libraries. *)
load_objs require_libs;
- (* We record the state here! *)
+ (* We record the state at this point! *)
State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
Backtrack.record ();
Slaves.init ();
diff --git a/stm/stm.mli b/stm/stm.mli
index 8b5581979..8a4de34b4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -46,15 +46,26 @@ type stm_doc_type =
(* Main initalization routine *)
type stm_init_options = {
+ (* The STM will set some internal flags differently depending on the
+ specified [doc_type]. This distinction should dissappear at some
+ some point. *)
doc_type : stm_doc_type;
+
+ (* Initial load path in scope for the document. Usually extracted
+ from -R options / _CoqProject *)
+ iload_path : Mltop.coq_path list;
+
+ (* Require [require_libs] before the initial state is
+ ready. Parameters follow [Library], that is to say,
+ [lib,prefix,import_export] means require library [lib] from
+ optional [prefix] and [import_export] if [Some false/Some true]
+ is used. *)
require_libs : (string * string option * bool option) list;
+
+ (* STM options that apply to the current document. *)
stm_options : AsyncOpts.stm_opt;
-(*
- fb_handler : Feedback.feedback -> unit;
- iload_path : (string list * string * bool) list;
- implicit_std : bool;
-*)
}
+(* fb_handler : Feedback.feedback -> unit; *)
(** The type of a STM document *)
type doc
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b3b5375bf..10205964a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -89,22 +89,26 @@ let ml_path_if c p =
let f x = { recursive = false; path_spec = MlPath x } in
if c then List.map f p else []
-(* Initializes the LoadPath *)
-let init_load_path ~load_init =
- let open Mltop in
+(* LoadPath for toploop toplevels *)
+let toplevel_init_load_path () =
let coqlib = Envars.coqlib () in
- let user_contrib = coqlib/"user-contrib" in
- let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
- let coqpath = Envars.coqpath in
- let coq_path = Names.DirPath.make [Libnames.coq_root] in
-
(* NOTE: These directories are searched from last to first *)
(* first, developer specific directory to open *)
ml_path_if Coq_config.local [coqlib/"dev"] @
(* main loops *)
ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @
- ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @
+ ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"]
+
+(* LoadPath for Coq user libraries *)
+let libs_init_load_path ~load_init =
+
+ let open Mltop in
+ let coqlib = Envars.coqlib () in
+ let user_contrib = coqlib/"user-contrib" in
+ let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
+ let coqpath = Envars.coqpath in
+ let coq_path = Names.DirPath.make [Libnames.coq_root] in
(* then standard library and plugins *)
[build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 089847f5d..0d2da84bb 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -19,5 +19,10 @@ val push_include : string -> Names.DirPath.t -> bool -> unit
(** [push_include phys_path log_path implicit] *)
val push_ml_include : string -> unit
-val init_load_path : load_init:bool -> Mltop.coq_path list
+
val init_ocaml_path : unit -> unit
+
+(* LoadPath for toploop toplevels *)
+val toplevel_init_load_path : unit -> Mltop.coq_path list
+(* LoadPath for Coq user libraries *)
+val libs_init_load_path : load_init:bool -> Mltop.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bf090862f..400f7048d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -304,6 +304,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
|> prlist_with_sep pr_comma Names.Id.print)
++ str ".")
in
+ let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+ let require_libs = require_libs () in
+ let stm_options = !top_stm_options in
match !compilation_mode with
| BuildVo ->
Flags.record_aux_file := true;
@@ -316,8 +319,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
let doc, sid = Stm.(new_doc
{ doc_type = VoDoc long_f_dot_vo;
- require_libs = require_libs ();
- stm_options = !top_stm_options;
+ iload_path;
+ require_libs;
+ stm_options;
}) in
let doc, sid = load_init_vernaculars ~time doc sid in
@@ -352,8 +356,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
let doc, sid = Stm.(new_doc
{ doc_type = VioDoc long_f_dot_vio;
- require_libs = require_libs ();
- stm_options = !top_stm_options;
+ iload_path;
+ require_libs;
+ stm_options;
}) in
let doc, sid = load_init_vernaculars ~time doc sid in
@@ -424,7 +429,12 @@ let set_vio_checking_j opt j =
prerr_endline "setting the J variable like in 'make vio2vo J=3'";
exit 1
-let schedule_vio opts =
+let schedule_vio () =
+ (* We must add update the loadpath here as the scheduling process
+ happens outside of the STM *)
+ let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+ List.iter Mltop.add_coq_path iload_path;
+
if !vio_checking then
Vio_checking.schedule_vio_checking !vio_files_j !vio_files
else
@@ -494,7 +504,8 @@ let usage batch =
try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
with NoCoqLib -> usage_no_coqlib ()
end;
- let lp = Coqinit.init_load_path ~load_init:!load_init in
+ let lp = Coqinit.toplevel_init_load_path () in
+ (* Necessary for finding the toplevels below *)
List.iter Mltop.add_coq_path lp;
if batch then Usage.print_usage_coqc ()
else begin
@@ -808,8 +819,8 @@ let init_toplevel arglist =
if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
if !print_tags then (print_style_tags (); exit (exitcode ()));
if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
- let lp = Coqinit.init_load_path ~load_init:!load_init in
- List.iter Mltop.add_coq_path lp;
+ let top_lp = Coqinit.toplevel_init_load_path () in
+ List.iter Mltop.add_coq_path top_lp;
Option.iter Mltop.load_ml_object_raw !toploop;
let extras = !toploop_init extras in
if not (CList.is_empty extras) then begin
@@ -845,11 +856,15 @@ let init_toplevel arglist =
|| CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks))
(* Interactive *)
then begin
+ let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+ let require_libs = require_libs () in
+ let stm_options = !top_stm_options in
try
let doc, sid = Stm.(new_doc
{ doc_type = Interactive !toplevel_name;
- require_libs = require_libs ();
- stm_options = !top_stm_options;
+ iload_path;
+ require_libs;
+ stm_options;
}) in
Some (load_init_vernaculars ~time:!measure_time doc sid)
with any -> flush_all(); fatal_error any