aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-06-20 15:18:40 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-06-20 15:49:44 +0200
commit2e99ed199cde9495bd0f7e3c1209986bcaf77947 (patch)
tree509d927c4cd2716494d3e6d123ed50496fd4f0b5 /stm
parentc68afe0da68a2653a47ac3ed2818886c1c338dda (diff)
STM: par: report no error to UIs in non-solve mode
Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve")
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml19
1 files changed, 8 insertions, 11 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 8ca50e2d5..90f977ddb 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1672,7 +1672,7 @@ end (* }}} *)
and TacTask : sig
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
@@ -1681,13 +1681,12 @@ and TacTask : sig
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
- exception NoProgress
include AsyncTaskQueue.Task with type task := task
end = struct (* {{{ *)
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -1709,10 +1708,9 @@ end = struct (* {{{ *)
r_name : string }
type response =
- | RespBuiltSubProof of output
+ | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
| RespError of Pp.std_ppcmds
| RespNoProgress
- exception NoProgress
let name = ref "tacworker"
let extra_env () = [||]
@@ -1734,10 +1732,9 @@ end = struct (* {{{ *)
let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
match resp with
- | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+ | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
| RespNoProgress ->
- let e = (NoProgress, Exninfo.null) in
- t_assign (`Exn e);
+ t_assign (`Val None);
t_kill ();
`Stay ((),[])
| RespError msg ->
@@ -1848,8 +1845,8 @@ end = struct (* {{{ *)
else tclUNIT ()
else
let open Notations in
- try
- let pt, uc = Future.join f in
+ match Future.join f with
+ | Some (pt, uc) ->
stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
@@ -1857,7 +1854,7 @@ end = struct (* {{{ *)
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
Tactics.exact_no_check (EConstr.of_constr pt))
- with TacTask.NoProgress ->
+ | None ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
end)
in