A minimal working example modifying the -vok option of coqc/rocqc such that

compilation does not fail on the first error inside proof, but discards all
commands to the end of that proof, which is admitted.  Subsequent lemmas can
then be proved, and they can raise more errors.  This makes it possible to have
several errors in the same file, but not in the same proof.

At the end of compilation, a report is generated, indicating how many proofs
failed, the name of each proof, and the error message.  In the current
version, no location information is provided.

This version is a request for comments.  One big unsatisfaction is the need
to change a line in stm.ml, because we need to use a command that is usually
reserved for interactive mode, while the compiler is a batch process.

An alternative choice would be to execute all commands, so that there could
be more than one error for each lemma and focusing information could be used
to guide the recovery process, but this would require more heavyweight
programming.

The example file on which this has been tested is:

Lemma L1 : False.
Proof.
exact I.
fail "any failure".
Qed.

Lemma L2 : True.
Proof.
exact I.
Qed.

Lemma L3 : True /\ False.
Proof.
split.
  exact L2.
exact L1.
Qed.

Lemma L4 : True /\ False.
Proof.
split.
  exact L2.
exact L2.
Qed.

Lemma L5 : False.
Proof.
Admitted.

Lemma L6 : False.
Proof.
exact L5.
Qed.

====
For this file, compilation with -vok reports 2 errors.

Error:
proofs failed in file ./trials/toto.v, number of failures: 2
L1
The term "I" has type "True" while it is expected to have type "False".
L4
The term "L2" has type "True" while it is expected to have type "False".

Author: ybertot

stm/stm.ml

@@ -2670,7 +2670,7 @@ let query ~doc ~at ~route s =
   s
 
 let edit_at ~doc id =
-  assert (VCS.is_interactive());
+  (* assert (VCS.is_interactive()); Needed for recovery mode in coqc -vok *)
   !Hooks.document_edit id;
   if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
   let vcs = VCS.backup () in

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

@@ -128,7 +128,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 * Pp.t) list;
+    in_recovery : bool;
+    recovery_mode : bool;
   }
 
 end
@@ -70,28 +73,62 @@ let emit_time state com tstart tend =
     | ToFeedback -> Feedback.msg_notice pp
     | ToChannel ch -> Pp.pp_with ch (pp ++ fnl())
 
+
+let admitted_com =
+  CAst.make { control = []; attrs = []; expr =
+    VernacSynPure (VernacEndProof Admitted)}
+
+let noop_com =
+  CAst.make {control = []; attrs = []; expr =
+    VernacSynPure (VernacProof (None, None))}
+
 let interp_vernac ~check ~state ({CAst.loc;_} as com) =
   let open State in
+
     try
+      let new_recovery_status, com =
+        if state.in_recovery then
+          (match Vernac_classifier.classify_vernac com with
+            Vernacextend.VtQed _ -> false, admitted_com
+            | _ -> true, noop_com)
+          else false, com in
+
       let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com 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 new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in
-      { state with doc; sid = nsid; proof = new_proof; }
+      (try
+        let () = if check && not new_recovery_status 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;
+          in_recovery = new_recovery_status}
+      with potentially_catched when
+        state.recovery_mode && noncritical potentially_catched ->
+        match state.proof with
+        | Some prf ->
+          (* If we want the compilation to proceed, we need the faulty error
+             to be removed from the STM, otherwise "Admitted" will dig it
+             out later. *)
+          let _, _ = Stm.edit_at ~doc state.sid in
+          let doc, nsid, ntip =
+            Stm.add ~doc:state.doc ~ontop:state.sid
+              (not !Flags.quiet) noop_com in
+          {state with doc; sid = nsid; in_recovery = true;
+          failed_proofs = ((Proof.data prf).name, print potentially_catched) ::
+            state.failed_proofs}
+        | None -> raise potentially_catched)
     with reraise ->
       let (reraise, info) = Exninfo.capture reraise 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)
+       in 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 +262,15 @@ 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 file " ++ Pp.str filename
+      ++ str ", number of failures: "
+      ++ int (List.length ostate.failed_proofs) ++ fnl()
+      ++ (ostate.failed_proofs
+                        |> List.rev
+                        |> prlist_with_sep fnl
+                          (fun (x, y) -> Names.Id.print x ++ Pp.fnl() ++
+                            y)));
   (* 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 * Pp.t) list;
+    in_recovery : bool;
+    recovery_mode : bool
   }
 
 end