[nit] Make output to be identical to Lean's, and to stdout.

tools/checkdecls/driver.ml

@@ -5,8 +5,22 @@
 (* Written by: Andrej Bauaer, Emilio J. Gallego Arias                   *)
 (************************************************************************)
 
+(* Notes:
+
+   - we could at some point use LSP, workspace/symbols seems like the closest
+   call, then we could filter client-side *)
+
+module Config = struct
+  type t =
+    { error_debug : bool
+          (* Print extra information when a constant is not found *)
+    }
+end
+
+let config : Config.t = { error_debug = false }
 let err_fmt = Format.err_formatter
 let pf fmt = Format.kfprintf (fun fmt -> Format.pp_print_flush fmt ()) fmt
+let out = pf Format.std_formatter
 
 let coq_init ~debug =
   let load_module = Dynlink.loadfile in
@@ -63,7 +77,9 @@ let do_decl decl =
     (* pf err "decl found! %s" decl; *)
     0
   | Error err ->
-    pf err_fmt "Error when processing input %s [%s]@\n" decl err;
+    out "%s is missing.@\n" decl;
+    if config.error_debug then
+      pf err_fmt "Error when processing input %s [%s]@\n" decl err;
     1
 
 let do_decls file =

tools/checkdecls/tests/run.t

@@ -21,16 +21,12 @@ Simple test with one file, succeed
   $ echo Coq.Init.Nat.add > clist
   $ echo Coq.Init.Peano.plus_n_O >> clist
   $ checkdecls clist
-  $ echo $?
-  0
 
 Simple test with one file, fail
 
   $ echo Coq.Init.Peano.not_a_constant >> clist
   $ echo Coq.Init.Nat.not_a_theorem >> clist
   $ checkdecls clist
-  Error when processing input Coq.Init.Peano.not_a_constant [Coq.Init.Peano.not_a_constant not found in name table]
-  Error when processing input Coq.Init.Nat.not_a_theorem [Coq.Init.Nat.not_a_theorem not found in name table]
+  Coq.Init.Peano.not_a_constant is missing.
+  Coq.Init.Nat.not_a_theorem is missing.
   [1]
-  $ echo $?
-  0