diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
| commit | 16dec9697b06a7fbda0997ab0685ef24443c7d3a (patch) | |
| tree | 1f85ee8f06535198d402ef9879883f3225291e6b /toplevel/coqinit.ml | |
| parent | 35c36f80dcc1e61e3dae8bcce1da71b384904582 (diff) | |
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index bf22c16cd..c80899288 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,9 +59,9 @@ let load_rcfile doc sid = doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) -let add_stdlib_path ~unix_path ~coq_root ~with_ml = +let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml = let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in - Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init) + Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init let add_userlib_path ~unix_path = Mltop.add_rec_path Mltop.AddRecML ~unix_path @@ -75,7 +75,7 @@ let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes (* Initializes the LoadPath *) -let init_load_path () = +let init_load_path ~load_init = 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 @@ -93,9 +93,9 @@ let init_load_path () = if System.exists_dir (coqlib/"toploop") then Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) - add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; + add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) - add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; + add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; (* then user-contrib *) if Sys.file_exists user_contrib then add_userlib_path ~unix_path:user_contrib; |