checkpoint

Author: ybertot

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

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

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 *)

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