[eco]: add a compilation trace (messages + goals)

ECO version is now 4.

The trace field is optional. The -trace command line option triggers
the trace recording in the generated .eco file.

Author: strub

src/ec.ml

@@ -407,15 +407,36 @@ let main () =
   (* Initialize I/O + interaction module *)
   let module State = struct
     type t = {
-      prvopts     : prv_options;
-      input       : string option;
-      terminal    : T.terminal lazy_t;
-      interactive : bool;
-      eco         : bool;
-      gccompact   : int option;
-      docgen      : bool;
-      outdirp     : string option;
+      (*---*) prvopts     : prv_options;
+      (*---*) input       : string option;
+      (*---*) terminal    : T.terminal lazy_t;
+      (*---*) interactive : bool;
+      (*---*) eco         : bool;
+      (*---*) gccompact   : int option;
+      (*---*) docgen      : bool;
+      (*---*) outdirp     : string option;
+      mutable trace       : trace1 list option;
     }
+
+    and trace1 =
+      { position : int
+      ; goals    : string list option
+      ; messages : (EcGState.loglevel * string) list }
+
+    module Trace = struct
+      let trace0 : trace1 =
+        { position = 0; goals = None; messages = []; }
+
+      let push1_message (trace1 : trace1) (msg, lvl) : trace1 =
+        { trace1 with messages = (msg, lvl) :: trace1.messages }
+
+      let push_message (trace : trace1 list) msg =
+        match trace with
+        | [] ->
+          [push1_message trace0 msg] 
+        | trace1 :: trace ->
+          push1_message trace1 msg :: trace
+    end
   end in
 
   let state : State.t =
@@ -471,7 +492,8 @@ let main () =
         ; eco         = false
         ; gccompact   = None
         ; docgen      = false
-        ; outdirp     = None }
+        ; outdirp     = None
+        ; trace       = None }
 
     end
 
@@ -493,14 +515,20 @@ let main () =
           lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
         in
 
+        let trace0 =
+          if cmpopts.cmpo_trace then
+            Some [State.{ position = 0; goals = None; messages = [] }]
+          else None in
+
         { prvopts     = {cmpopts.cmpo_provers with prvo_iterate = true}
         ; input       = Some name
         ; terminal    = terminal
         ; interactive = false
         ; eco         = cmpopts.cmpo_noeco
         ; gccompact   = cmpopts.cmpo_compact
         ; docgen      = false
-        ; outdirp     = None }
+        ; outdirp     = None
+        ; trace       = trace0 }
 
       end
 
@@ -543,7 +571,8 @@ let main () =
         ; eco         = true
         ; gccompact   = None
         ; docgen      = true
-        ; outdirp     = docopts.doco_outdirp }
+        ; outdirp     = docopts.doco_outdirp
+        ; trace       = None }
       end
 
   in
@@ -571,7 +600,20 @@ let main () =
 
         assert (nameo <> input);
 
-        let eco = EcEco.{
+        let eco =
+          let mktrace (trace : State.trace1 list) : EcEco.ecotrace =
+            let mktrace1 (trace1 : State.trace1) : int * EcEco.ecotrace1 =
+              let goals = Option.value ~default:[] trace1.goals in
+              let messages =
+                let for1 (lvl, msg) =
+                  Format.sprintf "%s: %s"
+                    (EcGState.string_of_loglevel lvl)
+                    msg in
+                String.concat "\n" (List.rev_map for1 trace1.messages) in
+              (trace1.position, EcEco.{ goals; messages; })
+            in List.rev_map mktrace1 trace in 
+
+          EcEco.{
             eco_root    = EcEco.{
               eco_digest  = Digest.file input;
               eco_kind    = kind;
@@ -584,6 +626,7 @@ let main () =
                      eco_kind   = x.rqd_kind;
                    } in (x.rqd_name, (ecr, x.rqd_direct)))
                 (EcScope.Theory.required scope));
+            eco_trace = Option.map mktrace state.trace;
         } in
 
         let out = open_out nameo in
@@ -665,7 +708,10 @@ let main () =
                EcScope.hierror "invalid pragma: `%s'\n%!" x);
 
             let notifier (lvl : EcGState.loglevel) (lazy msg) =
-              T.notice ~immediate:true lvl msg terminal
+              state.trace <- state.trace |> Option.map (fun trace ->
+                State.Trace.push_message trace (lvl, msg)
+              );
+              T.notice ~immediate:true lvl msg terminal;
             in
 
             EcCommands.addnotifier notifier;
@@ -694,8 +740,25 @@ let main () =
                    let timed = p.EP.gl_debug = Some `Timed in
                    let break = p.EP.gl_debug = Some `Break in
                    let ignore_fail = ref false in
+
+                     state.trace <- state.trace |> Option.map (fun trace ->
+                      { State.Trace.trace0 with position = loc.loc_echar } :: trace
+                     );
+
                      try
                        let tdelta = EcCommands.process ~src ~timed ~break p.EP.gl_action in
+
+                       state.trace <- state.trace |> Option.map (fun trace ->
+                        match trace with
+                        | [] -> assert false
+                        | trace1 :: trace ->
+                          assert (Option.is_none trace1.State.goals);
+                          let goals = EcCommands.pp_all_goals () in
+                          let goals = if List.is_empty goals then None else Some goals in
+                          let trace1 = { trace1 with goals } in
+                          trace1 :: trace
+                       );
+
                        if p.EP.gl_fail then begin
                          ignore_fail := true;
                          raise (EcScope.HiScopeError (None, "this command is expected to fail"))
@@ -713,10 +776,10 @@ let main () =
                          raise (EcScope.toperror_of_exn ~gloc:loc e)
                        end;
                        if T.interactive terminal then begin
-                         let error =
-                           Format.asprintf
-                             "The following error has been ignored:@.@.@%a"
-                             EcPException.exn_printer e in
+                        let error =
+                          Format.asprintf
+                            "The following error has been ignored:@.@.@%a"
+                            EcPException.exn_printer e in
                          T.notice ~immediate:true `Info error terminal
                        end
                    end)

src/ecCommands.ml

@@ -912,6 +912,11 @@ let addnotifier (notifier : notifier) =
   let gstate = EcScope.gstate (oget !context).ct_root in
   ignore (EcGState.add_notifier notifier gstate)
 
+(* -------------------------------------------------------------------- *)
+let notify (level : EcGState.loglevel) fmt =
+  assert (EcUtils.is_some !context);
+  EcScope.notify (oget !context).ct_root level fmt
+
 (* -------------------------------------------------------------------- *)
 let current () =
   (oget !context).ct_current
@@ -1017,7 +1022,36 @@ let pp_current_goal ?(all = false) stream =
       end
   end
 
+(* -------------------------------------------------------------------- *)
 let pp_maybe_current_goal stream =
   match (Pragma.get ()).pm_verbose with
   | true  -> pp_current_goal ~all:(Pragma.get ()).pm_g_prall stream
   | false -> ()
+
+(* -------------------------------------------------------------------- *)
+let pp_all_goals () =
+  let scope = current () in
+
+  match S.xgoal scope with
+  | Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin
+    match EcCoreGoal.opened pf with
+    | None ->
+      []
+
+    | Some _ ->
+      let get_hc { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } =
+        (EcEnv.LDecl.tohyps g_hyps, g_concl)
+      in
+
+      let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
+      let goals = List.map get_hc (EcCoreGoal.all_opened pf) in
+
+      List.map (fun goal ->
+        let buffer = Buffer.create 0 in
+        Format.fprintf
+          (Format.formatter_of_buffer buffer)
+          "%a@?" (EcPrinting.pp_goal1 ppe) goal;
+        Buffer.contents buffer) goals
+  end
+
+  | _ -> []

src/ecCommands.mli

@@ -36,6 +36,7 @@ val initialize  :
 
 val current     : unit -> EcScope.scope
 val addnotifier : notifier -> unit
+val notify      : EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a
 
 (* -------------------------------------------------------------------- *)
 val process_internal :
@@ -60,6 +61,7 @@ val doc_comment : [`Global | `Item] * string -> unit
 (* -------------------------------------------------------------------- *)
 val pp_current_goal : ?all:bool -> Format.formatter -> unit
 val pp_maybe_current_goal : Format.formatter -> unit
+val pp_all_goals : unit -> string list
 
 (* -------------------------------------------------------------------- *)
 val pragma_verbose : bool -> unit

src/ecCorePrinting.ml

@@ -112,6 +112,8 @@ module type PrinterAPI = sig
   val pp_hyps : PPEnv.t -> EcEnv.LDecl.hyps pp
   val pp_goal : PPEnv.t -> prpo_display -> ppgoal pp
 
+  val pp_goal1 : PPEnv.t -> (EcBaseLogic.hyps * form) pp
+
   (* ------------------------------------------------------------------ *)
   val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp  
 

src/ecEco.ml

@@ -5,7 +5,7 @@ module Json = Yojson
 
 (* -------------------------------------------------------------------- *)
 module Version = struct
-  let current : int = 3
+  let current : int = 4
 end
 
 (* -------------------------------------------------------------------- *)
@@ -16,9 +16,16 @@ type ecoroot = {
   eco_digest : digest;
 }
 
+type ecorange = int
+
+type ecotrace1 = { goals: string list; messages: string; }
+
+type ecotrace = (ecorange * ecotrace1) list
+
 type eco = {
   eco_root    : ecoroot;
   eco_depends : ecodepend Mstr.t;
+  eco_trace   : ecotrace option;
 }
 
 and ecodepend =
@@ -36,6 +43,24 @@ let flag_of_json (data : Json.t) : bool =
 let flag_to_json (flag : bool) : Json.t =
   `Bool flag
 
+(* -------------------------------------------------------------------- *)
+let int_of_json (data : Json.t) : int =
+  match data with
+  | `Int i -> i
+  | _ -> raise InvalidEco
+
+(* -------------------------------------------------------------------- *)
+let string_of_json (data : Json.t) : string =
+  match data with
+  | `String s -> s
+  | _ -> raise InvalidEco
+
+(* -------------------------------------------------------------------- *)
+let list_of_json (tx : Json.t -> 'a) (data : Json.t) : 'a list =
+  match data with
+  | `List data -> List.map tx data
+  | _ -> raise InvalidEco
+
 (* -------------------------------------------------------------------- *)
 let kind_to_json (k : EcLoader.kind) =
   match k with
@@ -71,9 +96,9 @@ let ecoroot_to_map (ecor : ecoroot) : (string * Json.t) list =
     "digest", digest_to_json ecor.eco_digest ]
 
 let ecoroot_of_map (data : Json.t Mstr.t) : ecoroot =
-  let kd = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
-  let dg = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
-  { eco_kind = kd; eco_digest = dg; }
+  let eco_kind   = kind_of_json (Mstr.find_exn InvalidEco "kind" data) in
+  let eco_digest = digest_of_json (Mstr.find_exn InvalidEco "digest" data) in
+  { eco_kind; eco_digest; }
 
 (* -------------------------------------------------------------------- *)
 let ecoroot_to_json (ecor : ecoroot) : Json.t =
@@ -86,6 +111,43 @@ let ecoroot_of_json (data : Json.t) : ecoroot =
 
   | _ -> raise InvalidEco
 
+(* -------------------------------------------------------------------- *)
+let trace_to_json (trace : ecotrace option) : Json.t =
+  match trace with
+  | None ->
+    `Null
+
+  | Some trace ->
+    let for1 ((position, { goals; messages; })) =
+      `Assoc [
+        ("position", `Int position);
+        ("goals"   , `List (List.map (fun goal -> `String goal) goals));
+        ("messages", `String messages);
+      ]
+    in `List (List.map for1 trace)
+
+let trace_of_json (data : Json.t) : ecotrace option =
+  match data with
+  | `Null ->
+    None
+
+  | `List data ->
+    let for1 (data : Json.t) =
+      match data with
+      | `Assoc data ->
+        let data = Mstr.of_list data in
+        let position = Mstr.find_exn InvalidEco "position" data |> int_of_json in
+        let goals = Mstr.find_exn InvalidEco "goals" data |> list_of_json string_of_json in
+        let messages = Mstr.find_exn InvalidEco "messages" data |> string_of_json in
+        (position, { goals; messages; })
+      | _ ->
+        raise InvalidEco
+
+    in Some (List.map for1 data)
+
+  | _ ->
+    raise InvalidEco
+
 (* -------------------------------------------------------------------- *)
 let ecodepend_to_json ((ecor, direct) : ecodepend) : Json.t =
   `Assoc ([ "direct", flag_to_json direct] @ (ecoroot_to_map ecor))
@@ -119,6 +181,7 @@ let to_json (eco : eco) : Json.t =
     [ "version", `Int Version.current;
       "echash" , `String EcVersion.hash;
       "root"   , ecoroot_to_json eco.eco_root;
+      "trace"  , trace_to_json eco.eco_trace;
       "depends", `Assoc depends ]
 
 (* -------------------------------------------------------------------- *)
@@ -135,10 +198,11 @@ let of_json (data : Json.t) : eco =
       if echash <> `String EcVersion.hash then
         raise InvalidEco;
 
-      let root    = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
-      let depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
+      let eco_root    = ecoroot_of_json (Mstr.find_exn InvalidEco "root" data) in
+      let eco_depends = depends_of_json (Mstr.find_exn InvalidEco "depends" data) in
+      let eco_trace   = trace_of_json   (Mstr.find_exn InvalidEco "trace" data) in
 
-      { eco_root = root; eco_depends = depends; }
+      { eco_root; eco_depends; eco_trace; }
 
   | _ -> raise InvalidEco