diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 12 | ||||
| -rw-r--r-- | stm/stm.ml | 26 | ||||
| -rw-r--r-- | stm/stm.mli | 6 |
3 files changed, 28 insertions, 16 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index be8ef24a09..73b9ef7da0 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -128,11 +128,13 @@ module Make(T : Task) () = struct | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl (* Options to discard: 1 argument *) - | ("-async-proofs" |"-vio2vo" | "-o" - |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" - |"-compile" |"-compile-verbose" - |"-async-proofs-cache" - |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> + | ( "-async-proofs" | "-vio2vo" | "-o" + | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv" + | "-compile" | "-compile-verbose" + | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j" + | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience" + | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold" + | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl -> set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" diff --git a/stm/stm.ml b/stm/stm.ml index 0165b3c029..b4f26570c6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2647,6 +2647,10 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; + (* Allow compiling modules in the Coq prefix. Irrelevant in + interactive mode. *) + allow_coq_overwrite : bool; + (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; @@ -2674,11 +2678,12 @@ let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let check_coq_overwriting p = +let check_coq_overwriting ~allow_coq_overwrite p = + if not allow_coq_overwrite then let l = DirPath.repr p in let id, l = match l with id::l -> id,l | [] -> assert false in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && Id.equal (CList.last l) Libnames.coq_root then + if not is_empty && Id.equal (CList.last l) Libnames.coq_root then user_err (str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") @@ -2695,7 +2700,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = @@ -2730,14 +2735,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = | VoDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ldir; + check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f | VioDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ldir; + check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f @@ -2885,11 +2890,12 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ldir long_f_dot_vo = +let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo + Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects + ldir long_f_dot_vo (Global.opaque_tables ()); doc @@ -3197,12 +3203,12 @@ let query ~doc ~at ~route s = let rec loop () = match parse_sentence ~doc at ~entry:Pvernac.main_entry s with | None -> () - | Some (loc, ast) -> - let indentation, strlen = compute_indentation ~loc at in + | Some {CAst.loc; v=ast} -> + let indentation, strlen = compute_indentation ?loc at in let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; - loc = Some loc; expr = ast } in + loc; expr = ast } in ignore(stm_vernac_interp ~route at st aast); loop () in diff --git a/stm/stm.mli b/stm/stm.mli index 821ab59a43..102e832d3e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -67,6 +67,10 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; + (* Allow compiling modules in the Coq prefix. Irrelevant in + interactive mode. *) + allow_coq_overwrite : bool; + (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; @@ -156,7 +160,7 @@ val join : doc:doc -> doc - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failure) *) -val snapshot_vio : doc:doc -> DirPath.t -> string -> doc +val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) |