diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 41acb2b1076b..0b41cda2f150 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -48,10 +48,13 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = create_empty_file long_f_dot_vok in match mode with | BuildVo | BuildVok -> + let recovery_mode = match mode with BuildVok -> true | _ -> false in let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VoDoc long_f_dot_out; injections; } in - let state = { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } in + let state = { doc; sid; proof = None; + time = Option.map Vernac.make_time_output opts.config.time; + failed_proofs = []; in_recovery = false; recovery_mode} in let state = Load.load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file @@ -91,7 +94,9 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = Stm.{ doc_type = VosDoc long_f_dot_out; injections; } in - let state = { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } in + let state = { doc; sid; proof = None; + time = Option.map Vernac.make_time_output opts.config.time; + failed_proofs = []; in_recovery = false; recovery_mode = false } in let state = Load.load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let source = source ldir long_f_dot_in in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a21f09bfd881..140fd400b29d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -127,7 +127,11 @@ let init_document opts stm_options injections = { doc_type = Interactive opts.config.logic.toplevel_name; injections; }) in - { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } + { doc; sid; proof = None; + time = Option.map Vernac.make_time_output opts.config.time; + failed_proofs = []; + in_recovery = false; + recovery_mode = false} let init_toploop opts stm_opts injections = let state = init_document opts stm_opts injections in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 392a667170da..b7fce4f897a0 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -57,6 +57,9 @@ module State = struct sid : Stateid.t; proof : Proof.t option; time : time_output option; + failed_proofs : Names.Id.t list; + in_recovery : bool; + recovery_mode : bool; } end @@ -72,26 +75,57 @@ let emit_time state com tstart tend = let interp_vernac ~check ~state ({CAst.loc;_} as com) = let open State in + + let current_proof_name = + match state.proof with + Some prf -> Some ((Proof.data prf).name) + | None -> None in + + let admitted_com = + CAst.make { control = []; attrs = []; expr = + (VernacSynPure (VernacEndProof Admitted))}in try - let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in + + let new_recovery_status, the_com = + if state.in_recovery then + (match Vernac_classifier.classify_vernac com with + Vernacextend.VtQed _ -> false, Some admitted_com + | _ -> true, None) + else false, Some com in + + let doc, nsid, ntip = + match the_com with + | Some com -> + Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com + | None -> state.doc, state.sid, Stm.NewAddTip in (* Main STM interaction *) if ntip <> Stm.NewAddTip then anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); - + + (* Force the command *) - let () = if check then Stm.observe ~doc nsid in + let () = if check && not state.in_recovery then Stm.observe ~doc nsid in let new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in - { state with doc; sid = nsid; proof = new_proof; } - with reraise -> - let (reraise, info) = Exninfo.capture reraise in + { state with doc; sid = nsid; proof = new_proof; + in_recovery = new_recovery_status} + with potentially_catched -> + let (reraise, info) = Exninfo.capture potentially_catched in let info = (* Set the loc to the whole command if no loc *) match Loc.get_loc info, loc with | None, Some loc -> Loc.add_loc info loc - | Some _, _ | _, None -> info - in - Exninfo.iraise (reraise, info) + | Some _, _ | _, None -> info in + if state.recovery_mode then + match current_proof_name with + Some proof_name -> + if CErrors.noncritical potentially_catched then + {state with in_recovery = true; + failed_proofs = proof_name :: state.failed_proofs} + else + Exninfo.iraise (reraise, info) + | None -> Exninfo.iraise (reraise, info) + else Exninfo.iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) let load_vernac_core ~echo ~check ~state ?source file = @@ -225,6 +259,12 @@ let beautify_pass ~doc ~comments ~ids ~filename = pass. *) let load_vernac ~echo ~check ~state ?source filename = let ostate, ids, comments = load_vernac_core ~echo ~check ~state ?source filename in + if 1 <= List.length (ostate.failed_proofs) then + user_err (Pp.str "proofs failed in this file " + ++ (ostate.failed_proofs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str "."); (* Pass for beautify *) if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename; (* End pass *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index b6ea3901b12c..1d8f09e70a87 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -20,6 +20,9 @@ module State : sig sid : Stateid.t; proof : Proof.t option; time : time_output option; + failed_proofs : Names.Id.t list; + in_recovery : bool; + recovery_mode : bool } end