in trustee_ot, pick log-based callbacks if we serve

src/opentheory/eval.ml

@@ -3,6 +3,8 @@
 open Common_
 module Log = Trustee_core.Log
 
+module Log_ = (val Logs.(src_log @@ Src.create "trustee.eval"))
+
 type 'a or_error = 'a Trustee_core.Error.or_error
 
 let now () = Unix.gettimeofday ()
@@ -53,6 +55,25 @@ class print_callbacks : callbacks =
         Article.pp_stats art time_s
   end
 
+class log_callbacks : callbacks =
+  object
+    method start_theory name = Log_.app (fun k -> k "checking theory `%s`" name)
+
+    method done_theory name ~ok ~time_s =
+      if ok then
+        Log_.app (fun k -> k "checked theory `%s` in %.3fs" name time_s)
+      else
+        Log_.err (fun k -> k "error theory `%s` in %.3fs" name time_s)
+
+    method start_article art_name =
+      Log_.info (fun k -> k "checking article '%s'" art_name)
+
+    method done_article art_name art ~time_s =
+      Log_.app (fun k ->
+          k "✔ checked article `%s`: %a in %.3fs" art_name Article.pp_stats art
+            time_s)
+  end
+
 (* ## main checking state ## *)
 
 type eval_info = {

src/opentheory/eval.mli

@@ -21,6 +21,8 @@ class default_callbacks : callbacks
 
 class print_callbacks : callbacks
 
+class log_callbacks : callbacks
+
 (** {2 Evaluation of theories} *)
 
 type state

src/opentheory/tool/trustee_ot.ml

@@ -65,7 +65,13 @@ let main ~dir ~serve ~port () =
   in
   let st =
     let progress_bar = !progress_ in
-    St.create ~cb:(new Eval.print_callbacks) ~progress_bar ~ctx ~idx ()
+    let cb =
+      if serve then
+        new Eval.log_callbacks
+      else
+        new Eval.print_callbacks
+    in
+    St.create ~cb ~progress_bar ~ctx ~idx ()
   in
 
   let th_serve =