Commit 0016da0c authored by Sylvain Dailler's avatar Sylvain Dailler

Fix catching of NoProgress/Exit exception in controller

NoProgress is raised by apply_trans not Exit. Noprogress without
uppercase P is removed.
parent 9fb35c19
......@@ -20,16 +20,6 @@ let debug_sched = Debug.register_info_flag "scheduler"
let debug_call_prover = Debug.lookup_flag "call_prover"
let default_delay_ms = 100 (* 0.1 seconds *)
exception Noprogress
let () = Exn_printer.register
(fun fmt e ->
match e with
| Noprogress ->
Format.fprintf fmt "The transformation made no progress.\n"
| _ -> raise e)
(** State of a proof *)
type proof_attempt_status =
| Undone (** prover was never called *)
......@@ -701,9 +691,9 @@ let schedule_transformation c id name args ~callback ~notification =
let tid = graft_transf c.controller_session id name args subtasks in
callback (TSdone tid)
with
| Exit ->
| NoProgress ->
(* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, Noprogress))
callback (TSfailed (id, NoProgress))
| e when not (Debug.test_flag Debug.stack_trace) ->
(* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *)
......
......@@ -40,8 +40,6 @@ type strategy_status = STSgoto of proofNodeID * int | STShalt
val print_strategy_status : Format.formatter -> strategy_status -> unit
exception Noprogress
(** {2 Signature for asynchronous schedulers} *)
(** Default delay for the scheduler timeout *)
......
......@@ -218,7 +218,7 @@ let bypass_pretty s id =
let get_exception_message ses id e =
match e with
| Controller_itp.Noprogress ->
| Session_itp.NoProgress ->
Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans s ->
Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
......
......@@ -1362,11 +1362,18 @@ let merge_proof new_s ~goal_obsolete new_goal _ old_pa_n =
exception NoProgress
let () = Exn_printer.register
(fun fmt e ->
match e with
| NoProgress ->
Format.fprintf fmt "The transformation made no progress.\n"
| _ -> raise e)
let apply_trans_to_goal ~allow_no_effect s env name args id =
let task,table = get_task_name_table s id in
let subtasks = Trans.apply_transform_args name env args table task in
(* If any generated task is equal to the former task, then we made no
progress because we need to prove more lemmas than before *)
progress because we need to prove more lemmas than before *)
match subtasks with
| [t'] when Task.task_equal t' task && not allow_no_effect ->
Debug.dprintf debug "[apply_trans_to_goal] apply_transform made no progress@.";
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment