diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-06 03:06:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-07 17:30:37 +0200 |
| commit | b6ea08b66f874de1ed787cdea68d058dad5ac9ad (patch) | |
| tree | 9f199d5bd84c545954ec692430f8b2501e481aba /toplevel | |
| parent | e9c6d4cbc9973e0c46b8022fcc5a794f363d1e86 (diff) | |
[toplevel] Fix path initialization before vio processing (closes #7044)
The toplevel refactoring made path initialization per document,
however vio-checking and vio-tasks are not documents, so loadpath must
be initialized individually.
Patch by @gares, refactoring to avoid double-initialization by me.
Co-authored-by: <Enrico.Tassi@inria.fr>
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a08cfa9f4..0dabed6b7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -315,16 +315,24 @@ let check_vio_tasks opts = (* vio files *) let schedule_vio opts = - (* We must add update the loadpath here as the scheduling process - happens outside of the STM *) - let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; - if opts.vio_checking then Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files +let do_vio opts = + (* We must initialize the loadpath here as the vio scheduling + process happens outside of the STM *) + if opts.vio_files <> [] || opts.vio_tasks <> [] then + let iload_path = build_load_path opts in + List.iter Mltop.add_coq_path iload_path; + + (* Vio compile pass *) + if opts.vio_files <> [] then schedule_vio opts; + (* Vio task pass *) + if opts.vio_tasks <> [] then check_vio_tasks opts + + (******************************************************************************) (* Color Options *) (******************************************************************************) @@ -483,10 +491,9 @@ let init_toplevel arglist = end else begin try compile_files opts; - (* Vio compile pass *) - if opts.vio_files <> [] then schedule_vio opts; - (* Vio task pass *) - check_vio_tasks opts; + (* Careful this will modify the load-path and state so after + this point some stuff may not be safe anymore. *) + do_vio opts; (* Allow the user to output an arbitrary state *) outputstate opts; None, opts |