diff options
| -rw-r--r-- | ide/fake_ide.ml | 13 | ||||
| -rw-r--r-- | stm/stm.ml | 21 | ||||
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | test-suite/ide/join-sync.fake | 20 | ||||
| -rw-r--r-- | test-suite/ide/join.fake | 20 |
5 files changed, 71 insertions, 5 deletions
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 521aff6bf6..8b0c736f50 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -11,7 +11,7 @@ (** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *) let error s = - prerr_endline ("fake_id: error: "^s); + prerr_endline ("fake_ide: error: "^s); exit 1 let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp @@ -22,7 +22,7 @@ type coqtop = { } let print_error msg = - Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg + Format.eprintf "fake_ide: error: @[%a@]\n%!" Pp.pp_with msg let base_eval_call ?(print=true) ?(fail=true) call coqtop = if print then prerr_endline (Xmlprotocol.pr_call call); @@ -257,10 +257,15 @@ let eval_print l coq = eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> eval_call (status true) coq + | [ Tok(_,"FAILJOIN") ] -> + after_fail coq (base_eval_call ~fail:false (status true) coq) | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" else prerr_endline "Good tip" + | [ Tok(_,"ABORT") ] -> + prerr_endline "Quitting fake_ide"; + exit 0 | Tok("#[^\n]*",_) :: _ -> () | _ -> error "syntax error" @@ -276,6 +281,8 @@ let grammar = ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "FAILJOIN")] + ; Seq [Item (eat_rex "ABORT")] ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] ; Item (eat_rex "#[^\n]*") ] @@ -305,6 +312,8 @@ let main = Array.of_list (def_args @ ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in + prerr_endline ("Running: "^idetop_name^" "^ + (String.concat " " (Array.to_list coqtop_args))); let coq = let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in diff --git a/stm/stm.ml b/stm/stm.ml index c9b1695407..c84721bcb5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2718,7 +2718,7 @@ let finish ~doc = ); doc let wait ~doc = - let doc = finish ~doc in + let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in Slaves.wait_all_done (); VCS.print (); doc @@ -2732,12 +2732,29 @@ let rec join_admitted_proofs id = join_admitted_proofs view.next | _ -> join_admitted_proofs view.next +(* Error resiliency may have tolerated some broken commands *) +let rec check_no_err_states ~doc visited id = + let open Stateid in + if Set.mem id visited then visited else + match state_of_id ~doc id with + | `Error e -> raise e + | _ -> + let view = VCS.visit id in + match view.step with + | `Qed(_,id) -> + let visited = check_no_err_states ~doc (Set.add id visited) id in + check_no_err_states ~doc visited view.next + | _ -> check_no_err_states ~doc (Set.add id visited) view.next + let join ~doc = let doc = wait ~doc in stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); stm_prerr_endline (fun () -> "Joining Admitted proofs"); - join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); + join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master); + stm_prerr_endline (fun () -> "Checking no error states"); + ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial) + (VCS.get_branch_pos VCS.Branch.master)); VCS.print (); doc diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d2277c37e..530671e1a1 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -569,7 +569,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake new file mode 100644 index 0000000000..236028ce46 --- /dev/null +++ b/test-suite/ide/join-sync.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency + async proofs off +# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on") +# + +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +WAIT +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT |