aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml18
-rw-r--r--stm/coqworkmgrApi.ml4
-rw-r--r--stm/coqworkmgrApi.mli3
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/proofBlockDelimiter.mli4
-rw-r--r--stm/proofworkertop.ml16
-rw-r--r--stm/proofworkertop.mllib1
-rw-r--r--stm/queryworkertop.ml16
-rw-r--r--stm/queryworkertop.mllib1
-rw-r--r--stm/stm.ml38
-rw-r--r--stm/stm.mllib1
-rw-r--r--stm/tacworkertop.ml16
-rw-r--r--stm/tacworkertop.mllib1
-rw-r--r--stm/vernac_classifier.ml9
-rw-r--r--stm/vernac_classifier.mli1
-rw-r--r--stm/workerLoop.ml25
16 files changed, 53 insertions, 105 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index b3e1500ae4..768d94d305 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
type request = Request of T.request
type more_data =
- | MoreDataUnivLevel of Universes.universe_id list
+ | MoreDataUnivLevel of UnivGen.universe_id list
let slave_respond (Request r) =
let res = T.perform r in
@@ -120,12 +120,11 @@ module Make(T : Task) () = struct
let proc, ic, oc =
let rec set_slave_opt = function
| [] -> !async_proofs_flags_for_workers @
- ["-toploop"; !T.name^"top";
- "-worker-id"; name;
+ ["-worker-id"; name;
"-async-proofs-worker-priority";
- CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
- | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
- | ("-async-proofs" |"-toploop" |"-vio2vo"
+ CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+ | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+ | ("-async-proofs" |"-vio2vo"
|"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
|"-compile" |"-compile-verbose"
|"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -134,7 +133,8 @@ module Make(T : Task) () = struct
let args =
Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
let env = Array.append (T.extra_env ()) (Unix.environment ()) in
- Worker.spawn ~env Sys.argv.(0) args in
+ let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+ Worker.spawn ~env worker_name args in
name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
let manager cpanel (id, proc, ic, oc) =
@@ -171,7 +171,7 @@ module Make(T : Task) () = struct
| Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
| Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
let more_univs n =
- CList.init n (fun _ -> Universes.new_univ_id ()) in
+ CList.init n (fun _ -> UnivGen.new_univ_id ()) in
let rec kill_if () =
if not (Worker.is_alive proc) then ()
@@ -310,7 +310,7 @@ module Make(T : Task) () = struct
Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
(* We ask master to allocate universe identifiers *)
- Universes.set_remote_new_univ_id (bufferize (fun () ->
+ UnivGen.set_remote_new_univ_id (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
match unmarshal_more_data (Option.get !slave_ic) with
| MoreDataUnivLevel l -> l));
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 36b5d18ab6..841cc08c07 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -11,6 +11,10 @@
let debug = false
type priority = Low | High
+
+(* Default priority *)
+let async_proofs_worker_priority = ref Low
+
let string_of_priority = function Low -> "low" | High -> "high"
let priority_of_string = function
| "low" -> Low
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 2983b619db..be5b291776 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -14,6 +14,9 @@ type priority = Low | High
val string_of_priority : priority -> string
val priority_of_string : string -> priority
+(* Default priority *)
+val async_proofs_worker_priority : priority ref
+
(* Connects to a work manager if any. If no worker manager, then
-async-proofs-j and -async-proofs-tac-j are used *)
val init : priority -> unit
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 0af766219c..b8af2bcd56 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
static_block_declaration option
val unit_val : Stm.DynBlockData.t
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de1141..eacd3687ae 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -38,6 +38,6 @@ val crawl :
val unit_val : Stm.DynBlockData.t
(* Bullets *)
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
deleted file mode 100644
index 4b85a05ac7..0000000000
--- a/stm/proofworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
deleted file mode 100644
index f9f6c22d51..0000000000
--- a/stm/proofworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Proofworkertop
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
deleted file mode 100644
index aa00102aab..0000000000
--- a/stm/queryworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib
deleted file mode 100644
index c2f73089b3..0000000000
--- a/stm/queryworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Queryworkertop
diff --git a/stm/stm.ml b/stm/stm.ml
index cbd324f5c7..c394be22e1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1511,7 +1511,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
+ expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1661,7 +1661,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
+ expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) });
`OK proof
end
with e ->
@@ -1849,7 +1849,7 @@ end = struct (* {{{ *)
| RespError of Pp.t
| RespNoProgress
- let name = ref "tacworker"
+ let name = ref "tacticworker"
let extra_env () = [||]
type competence = unit
type worker_status = Fresh | Old of competence
@@ -2113,12 +2113,6 @@ let delegate name =
|| VCS.is_vio_doc ()
|| !cur_opt.async_proofs_full
-let warn_deprecated_nested_proofs =
- CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
- (fun () ->
- strbrk ("Nested proofs are deprecated and will "^
- "stop working in a future Coq version"))
-
let collect_proof keep cur hd brkind id =
stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
@@ -2127,7 +2121,7 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let is_defined_expr = function
- | VernacEndProof (Proved (Transparent,_)) -> true
+ | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
| _ -> false in
let is_defined = function
| _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
@@ -2200,8 +2194,7 @@ let collect_proof keep cur hd brkind id =
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
let name = name ids in
`MaybeASync (parent last, accn, name, delegate name)
- | `Sideff _ ->
- warn_deprecated_nested_proofs ();
+ | `Sideff (CherryPickEnv,_) ->
`Sync (no_name,`NestedProof)
| _ -> `Sync (no_name,`Unknown) in
let make_sync why = function
@@ -2288,7 +2281,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
- fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
@@ -2771,6 +2764,14 @@ let process_back_meta_command ~newtip ~head oid aast w =
VCS.commit id (Alias (oid,aast));
Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+let allow_nested_proofs = ref false
+let _ = Goptions.declare_bool_option
+ { Goptions.optdepr = false;
+ Goptions.optname = "Nested Proofs Allowed";
+ Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name;
+ Goptions.optread = (fun () -> !allow_nested_proofs);
+ Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
+
let process_transaction ~doc ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
@@ -2802,6 +2803,15 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
(* Proof *)
| VtStartProof (mode, guarantee, names), w ->
+
+ if not !allow_nested_proofs && VCS.proof_nesting () > 0 then
+ "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+ |> Pp.str
+ |> (fun s -> (UserError (None, s), Exninfo.null))
+ |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
+ |> Exninfo.iraise
+ else
+
let id = VCS.new_node ~id:newtip () in
let bname = VCS.mk_branch_name x in
VCS.checkout VCS.Branch.master;
@@ -2966,7 +2976,7 @@ let parse_sentence ~doc sid pa =
str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
Flags.with_option Flags.we_are_parsing (fun () ->
try
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+ match Pcoq.Gram.entry_parse Pvernac.main_entry pa with
| None -> raise End_of_input
| Some (loc, cmd) -> CAst.make ~loc cmd
with e when CErrors.noncritical e ->
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 72b5380162..4b254e8113 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,7 +5,6 @@ TQueue
WorkerPool
Vernac_classifier
CoqworkmgrApi
-WorkerLoop
AsyncTaskQueue
Stm
ProofBlockDelimiter
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
deleted file mode 100644
index 3b91df86e0..0000000000
--- a/stm/tacworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib
deleted file mode 100644
index db38fde279..0000000000
--- a/stm/tacworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Tacworkertop
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c08cc6e367..e01dcbcb6e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -54,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list =
| Names.Anonymous -> []
| Names.Name n -> [n]
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+ [ Vernacentries.universe_polymorphism_option_name;
+ stm_allow_nested_proofs_option_name ]
+
let classify_vernac e =
let static_classifier ~poly e = match e with
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
| ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
- when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+ when CList.exists (CList.equal String.equal l)
+ options_affecting_stm_scheduling ->
VtSideff [], VtNow
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index abbc04e895..45fbfb42af 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -25,3 +25,4 @@ val classify_as_query : vernac_classification
val classify_as_sideeff : vernac_classification
val classify_as_proofstep : vernac_classification
+val stm_allow_nested_proofs_option_name : string list
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
deleted file mode 100644
index 5130b019a9..0000000000
--- a/stm/workerLoop.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(* Default priority *)
-open CoqworkmgrApi
-let async_proofs_worker_priority = ref Low
-
-let rec parse = function
- | "--xml_format=Ppcmds" :: rest -> parse rest
- | x :: rest -> x :: parse rest
- | [] -> []
-
-let loop init coq_args extra_args =
- let args = parse extra_args in
- Flags.quiet := true;
- init ();
- CoqworkmgrApi.init !async_proofs_worker_priority;
- coq_args, args
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:09:05 +0000