From 15ab2869ab700d21c59c5a272721b5bba1d2b8ee Mon Sep 17 00:00:00 2001 From: lduboisd Date: Fri, 10 Dec 2021 17:55:46 +0100 Subject: verit timeout --- src/Tactics.v | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/g_smtcoq.mlg | 6 +++-- src/verit/verit.ml | 14 ++++++++--- src/verit/verit.mli | 4 +-- 4 files changed, 87 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/Tactics.v b/src/Tactics.v index f79b253..e41b0f5 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -89,6 +89,31 @@ Tactic Notation "verit_bool_no_check" constr(h) := Tactic Notation "verit_bool_no_check" := get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto). +(** Tactics in bool with timeout **) + +Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances. + +Tactic Notation "verit_bool_timeout" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) + | None => verit_bool_base_auto_timeout (Some h) + end; + vauto). +Tactic Notation "verit_bool_timeout" := + get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto). + +Tactic Notation "verit_bool_no_check_timeout" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) + | None => verit_bool_no_check_base_auto_timeout (Some h) + end; + vauto). +Tactic Notation "verit_bool_no_check_timeout" := + get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; vauto). + (** Tactics in Prop **) @@ -140,6 +165,52 @@ Tactic Notation "verit_no_check" := end; vauto) ]. +Tactic Notation "verit_timeout" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) ] + | None => verit_bool_base_auto_timeout (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit_timeout" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some Hs) ] + | None => verit_bool_base_auto_timeout (@None nat) + end; vauto) + ]. +Tactic Notation "verit_no_check_timeout" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) ] + | None => verit_bool_no_check_base_auto_timeout (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit_no_check_timeout" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) ] + | None => verit_bool_no_check_base_auto_timeout (@None nat) + end; vauto) + ]. + + Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg index c8d38db..19298f4 100644 --- a/src/g_smtcoq.mlg +++ b/src/g_smtcoq.mlg @@ -113,8 +113,10 @@ END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic lpl (get_lemmas ()) } -| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check lpl (get_lemmas ()) } +| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) } +| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) } +| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) } +| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) } END TACTIC EXTEND Tactic_cvc4 diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 7f89943..b0c75a7 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -169,7 +169,7 @@ let export out_channel rt ro lsmt = exception Unknown -let call_verit _ rt ro ra_quant rf_quant first lsmt = +let call_verit timeout _ rt ro ra_quant rf_quant first lsmt = let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro lsmt; close_out outchan; @@ -177,6 +177,11 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt = let wname, woc = Filename.open_temp_file "warnings_verit" ".log" in close_out woc; let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename ^ " 2> " ^ wname in + let command = + match timeout with + | Some i -> "timeout "^(string_of_int i)^" "^command + | None -> command + in Format.eprintf "%s@." command; let t0 = Sys.time () in let exit_code = Sys.command command in @@ -202,7 +207,7 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt = CoqInterface.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in - + if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = failwith "veriT timed out" in ()); try if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); @@ -217,7 +222,7 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt = let verit_logic = SL.of_list [LUF; LLia] -let tactic_gen vm_cast lcpl lcepl = +let tactic_gen vm_cast timeout lcpl lcepl = (* Transform the tuple of lemmas given by the user into a list *) let lcpl = let lcpl = EConstr.Unsafe.to_constr lcpl in @@ -235,6 +240,7 @@ let tactic_gen vm_cast lcpl lcepl = let rf = VeritSyntax.rf in let ra_quant = VeritSyntax.ra_quant in let rf_quant = VeritSyntax.rf_quant in - SmtCommands.tactic call_verit verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl + SmtCommands.tactic (call_verit timeout) verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl let tactic = tactic_gen vm_cast_true let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check) + diff --git a/src/verit/verit.mli b/src/verit/verit.mli index f0acd0c..654de07 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -19,5 +19,5 @@ val parse_certif : val checker : string -> string -> unit val checker_debug : string -> string -> unit val theorem : CoqInterface.id -> string -> string -> unit -val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic -val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic +val tactic : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic +val tactic_no_check : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic -- cgit From 59be27207e4527661d219991728a1372335ceede Mon Sep 17 00:00:00 2001 From: lduboisd Date: Fri, 8 Apr 2022 17:11:50 +0200 Subject: use of anomaly for timeout --- src/PropToBool.v | 10 +++++----- src/Tactics.v | 2 +- src/verit/verit.ml | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/PropToBool.v b/src/PropToBool.v index bbe1967..e06b336 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -164,10 +164,10 @@ Ltac prop2bool_hyp H := destruct HFalse | ]; clear H'; - match (eval compute in prop2bool_comp) with + lazymatch (eval compute in prop2bool_comp) with | true => let A := eval cbv in prop2bool_t in - match goal with + lazymatch goal with | [ _ : CompDec A |- _ ] => idtac | _ => let Hcompdec := fresh "Hcompdec" in @@ -195,7 +195,7 @@ Ltac prop2bool_hyp H := | _ => prop2bool end in tac_rec; - match goal with + lazymatch goal with | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g end; destruct HFalse @@ -213,9 +213,9 @@ Ltac prop2bool_hyp H := Ltac remove_compdec_hyp H := let TH := type of H in - match TH with + lazymatch TH with | forall p : CompDec ?A, _ => - match goal with + lazymatch goal with | [ p' : CompDec A |- _ ] => let H1 := fresh in assert (H1 := H p'); clear H; assert (H := H1); clear H1; diff --git a/src/Tactics.v b/src/Tactics.v index e41b0f5..c44af14 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -29,7 +29,7 @@ Ltac get_hyps_acc acc k := | id _ => fail | _ => change P with (id P) in H; - match acc with + lazymatch acc with | Some ?t => get_hyps_acc (Some (H, t)) k | None => get_hyps_acc (Some H) k end diff --git a/src/verit/verit.ml b/src/verit/verit.ml index b0c75a7..12efcc9 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -207,7 +207,7 @@ let call_verit timeout _ rt ro ra_quant rf_quant first lsmt = CoqInterface.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in - if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = failwith "veriT timed out" in ()); + if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = CErrors.anomaly (Pp.str "veriT timed out") in ()) ; try if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); -- cgit From e61a54d7581b42259d726389250e1cb63682d8d8 Mon Sep 17 00:00:00 2001 From: lduboisd Date: Mon, 11 Apr 2022 11:29:23 +0200 Subject: verit_timeout takes an integer as parameter --- src/Tactics.v | 48 ++++++++++++++++++++++++------------------------ src/g_smtcoq.mlg | 4 ++-- 2 files changed, 26 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/Tactics.v b/src/Tactics.v index c44af14..316fcc1 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -91,28 +91,28 @@ Tactic Notation "verit_bool_no_check" := (** Tactics in bool with timeout **) -Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances. -Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances. +Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances. -Tactic Notation "verit_bool_timeout" constr(h) := +Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) - | None => verit_bool_base_auto_timeout (Some h) + | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_base_auto_timeout (Some h) timeout end; vauto). -Tactic Notation "verit_bool_timeout" := - get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto). +Tactic Notation "verit_bool_timeout" int_or_var(timeout) := + get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto). -Tactic Notation "verit_bool_no_check_timeout" constr(h) := +Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) - | None => verit_bool_no_check_base_auto_timeout (Some h) + | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout end; vauto). -Tactic Notation "verit_bool_no_check_timeout" := - get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; vauto). +Tactic Notation "verit_bool_no_check_timeout" int_or_var(timeout) := + get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto). (** Tactics in Prop **) @@ -165,48 +165,48 @@ Tactic Notation "verit_no_check" := end; vauto) ]. -Tactic Notation "verit_timeout" constr(h) := +Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) := prop2bool; [ .. | prop2bool_hyps h; [ .. | get_hyps ltac:(fun Hs => match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) ] - | None => verit_bool_base_auto_timeout (Some h) + [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout] + | None => verit_bool_base_auto_timeout (Some h) timeout end; vauto) ] ]. -Tactic Notation "verit_timeout" := +Tactic Notation "verit_timeout" int_or_var(timeout) := prop2bool; [ .. | get_hyps ltac:(fun Hs => match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base_auto_timeout (Some Hs) ] - | None => verit_bool_base_auto_timeout (@None nat) + [ .. | verit_bool_base_auto_timeout (Some Hs) timeout] + | None => verit_bool_base_auto_timeout (@None nat) timeout end; vauto) ]. -Tactic Notation "verit_no_check_timeout" constr(h) := +Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) := prop2bool; [ .. | prop2bool_hyps h; [ .. | get_hyps ltac:(fun Hs => match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) ] - | None => verit_bool_no_check_base_auto_timeout (Some h) + [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ] + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout end; vauto) ] ]. -Tactic Notation "verit_no_check_timeout" := +Tactic Notation "verit_no_check_timeout" int_or_var(timeout) := prop2bool; [ .. | get_hyps ltac:(fun Hs => match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) ] - | None => verit_bool_no_check_base_auto_timeout (@None nat) + [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout] + | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout end; vauto) ]. diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg index 19298f4..1d8f146 100644 --- a/src/g_smtcoq.mlg +++ b/src/g_smtcoq.mlg @@ -115,8 +115,8 @@ END TACTIC EXTEND Tactic_verit | [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) } | [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) } -| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) } -| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) } +| [ "verit_bool_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic (Some timeout) lpl (get_lemmas ()) } +| [ "verit_bool_no_check_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic_no_check (Some timeout) lpl (get_lemmas ()) } END TACTIC EXTEND Tactic_cvc4 -- cgit From deb9927455bcb3b506d17a63a9b7b5ec11fe9027 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 14 Apr 2022 18:01:03 +0200 Subject: Port --- src/Tactics.v | 87 ++++++++++++++++++++++++++++++----------------------------- 1 file changed, 45 insertions(+), 42 deletions(-) (limited to 'src') diff --git a/src/Tactics.v b/src/Tactics.v index 727e0b7..6f2c7b1 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -94,30 +94,33 @@ Tactic Notation "verit_bool_no_check" := let Hs := get_hyps in fun Hs => verit_bool_no_check_base_auto Hs; vauto. + (** Tactics in bool with timeout **) Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances. Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances. Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) := - get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout - | None => verit_bool_base_auto_timeout (Some h) timeout - end; - vauto). + let Hs := get_hyps in + match Hs with + | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_base_auto_timeout (Some h) timeout + end; + vauto. Tactic Notation "verit_bool_timeout" int_or_var(timeout) := - get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto). + let Hs := get_hyps in + verit_bool_base_auto_timeout Hs timeout; vauto. Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) := - get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout - | None => verit_bool_no_check_base_auto_timeout (Some h) timeout - end; - vauto). + let Hs := get_hyps in + match Hs with + | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout + end; + vauto. Tactic Notation "verit_bool_no_check_timeout" int_or_var(timeout) := - get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto). + let Hs := get_hyps in + verit_bool_no_check_base_auto_timeout Hs timeout; vauto. (** Tactics in Prop **) @@ -173,46 +176,46 @@ Tactic Notation "verit_no_check" := Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) := prop2bool; [ .. | prop2bool_hyps h; - [ .. | get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout] - | None => verit_bool_base_auto_timeout (Some h) timeout - end; vauto) + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout ] + | None => verit_bool_base_auto_timeout (Some h) timeout + end; vauto ] ]. Tactic Notation "verit_timeout" int_or_var(timeout) := prop2bool; - [ .. | get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_base_auto_timeout (Some Hs) timeout] - | None => verit_bool_base_auto_timeout (@None nat) timeout - end; vauto) + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some Hs) timeout ] + | None => verit_bool_base_auto_timeout (@None nat) timeout + end; vauto ]. Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) := prop2bool; [ .. | prop2bool_hyps h; - [ .. | get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ] - | None => verit_bool_no_check_base_auto_timeout (Some h) timeout - end; vauto) + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ] + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout + end; vauto ] ]. Tactic Notation "verit_no_check_timeout" int_or_var(timeout) := prop2bool; - [ .. | get_hyps ltac:(fun Hs => - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout] - | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout - end; vauto) + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout ] + | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout + end; vauto ]. -- cgit From 65c185275f8c78908c1496c6665bc7fd50a4607b Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 14 Apr 2022 18:01:15 +0200 Subject: Clean-up --- src/trace/coqInterface.ml | 1 + src/trace/coqInterface.mli | 1 + src/verit/verit.ml | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index a8af566..8b91225 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -150,6 +150,7 @@ let set_evars_tac noc = (* Other differences between the two versions of Coq *) type constr_expr = Constrexpr.constr_expr let error s = CErrors.user_err (Pp.str s) +let anomaly s = CErrors.anomaly (Pp.str s) let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 86fdd95..453bce1 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -98,6 +98,7 @@ val set_evars_tac : constr -> tactic (* Other differences between the two versions of Coq *) type constr_expr = Constrexpr.constr_expr val error : string -> 'a +val anomaly : string -> 'a val warning : string -> string -> unit val extern_constr : constr -> constr_expr val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types diff --git a/src/verit/verit.ml b/src/verit/verit.ml index eb8c5cc..33f9b4c 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -207,7 +207,7 @@ let call_verit timeout _ rt ro ra_quant rf_quant first lsmt = CoqInterface.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in - if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = CErrors.anomaly (Pp.str "veriT timed out") in ()) ; + if exit_code = 124 (*code for timeout*) then (close_in win; Sys.remove wname; let _ = CoqInterface.anomaly "veriT timed out" in ()); try if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); -- cgit