Add minimal Logs integration

This PR adds:
- `Logs` as a new dependency;
- Logs' sources for each debug flag;
- A reporter that prints on the appropriate output (regular or
  diagnostic) according to the source.

CHANGES.md

@@ -99,6 +99,7 @@
  - Uniformization of internal identifiers generation (#905, #918)
  - Use an efficient `String.starts_with` implementation (#912)
  - Fix the Makefile (#914)
+ - Add `Logs` dependency (#1206)
 
 ### Testing
 

rsc/extra/worker_json_example.json

@@ -10,7 +10,7 @@
     "debug": false, "debug_ac": false, "debug_adt": false,
     "debug_arith": false, "debug_arrays": false, "debug_bitv": false,
     "debug_cc": false, "debug_combine": false, "debug_constr": false,
-    "debug_explanations": false, "debug_fm": false, "debug_fpa": 0,
+    "debug_explanation": false, "debug_fm": false, "debug_fpa": 0,
     "debug_gc": false, "debug_interpretation": false, "debug_ite": false,
     "debug_matching": 0, "debug_sat": false, "debug_split": false,
     "debug_triggers": false, "debug_types": false,

src/bin/common/parse_command.ml

@@ -213,50 +213,107 @@ module Debug = struct
     | Commands -> "commands"
     | Optimize -> "optimize"
 
+  let set_level src = Logs.Src.set_level src (Some Debug)
+
   let mk ~verbosity flags =
+    let module S = Sources in
     List.concat flags
     |> List.iter (function
-        | Debug -> Options.set_debug true
-        | Ac -> Options.set_debug_ac true
-        | Adt -> Options.set_debug_adt true
-        | Arith -> Options.set_debug_arith true
-        | Arrays -> Options.set_debug_arrays true
-        | Bitv -> Options.set_debug_bitv true
+        | Debug ->
+          Options.set_debug true
+        | Ac ->
+          Options.set_debug_ac true;
+          set_level S.ac
+        | Adt ->
+          Options.set_debug_adt true;
+          set_level S.adt;
+          set_level S.adt_rel
+        | Arith ->
+          Options.set_debug_arith true;
+          set_level S.arith;
+          set_level S.interval_calculus
+        | Arrays ->
+          Options.set_debug_arrays true;
+          set_level S.arrays_rel
+        | Bitv ->
+          Options.set_debug_bitv true;
+          set_level S.bitv
         | Sum ->
           Printer.print_wrn
             "The debug flag 'sum' is deprecated and is replaced by 'adt'. \
              It has the same effect as 'adt' and will be removed in a future \
              version.";
-          Options.set_debug_adt true
-        | Ite -> Options.set_debug_ite true
-        | Cc -> Options.set_debug_cc true
-        | Combine -> Options.set_debug_combine true
-        | Constr -> Options.set_debug_constr true
-        | Explanation -> Options.set_debug_explanations true
-        | Fm -> Options.set_debug_fm true
-        | Fpa -> Options.set_debug_fpa verbosity
-        | Gc -> Options.set_debug_gc true
-        | Interpretation -> Options.set_debug_interpretation true
-        | Intervals -> Options.set_debug_intervals true
-        | Matching -> Options.set_debug_matching verbosity
-        | Sat -> Options.set_debug_sat true
-        | Split -> Options.set_debug_split true
-        | Triggers -> Options.set_debug_triggers true
-        | Types -> Options.set_debug_types true
+          Options.set_debug_adt true;
+          set_level S.adt;
+          set_level S.adt_rel
+        | Ite ->
+          Options.set_debug_ite true;
+          set_level S.ite_rel
+        | Cc ->
+          Options.set_debug_cc true;
+          set_level S.cc
+        | Combine ->
+          Options.set_debug_combine true;
+          set_level S.combine
+        | Constr ->
+          Options.set_debug_constr true;
+          set_level S.constr
+        | Explanation ->
+          Options.set_debug_explanation true;
+          set_level S.explanation
+        | Fm ->
+          Options.set_debug_fm true;
+          set_level S.fm
+        | Fpa ->
+          Options.set_debug_fpa verbosity
+        | Gc ->
+          Options.set_debug_gc true;
+          set_level S.gc_debug
+        | Interpretation ->
+          Options.set_debug_interpretation true;
+          set_level S.interpretation
+        | Intervals ->
+          Options.set_debug_intervals true;
+          set_level S.intervals
+        | Matching ->
+          Options.set_debug_matching verbosity
+        | Sat ->
+          Options.set_debug_sat true;
+          set_level S.sat
+        | Split ->
+          Options.set_debug_split true;
+          set_level S.split
+        | Triggers ->
+          Options.set_debug_triggers true;
+          set_level S.triggers
+        | Types ->
+          Options.set_debug_types true;
+          set_level S.types
         | Typing ->
           Printer.print_wrn
             "The debug flag 'typing' has no effect. It will be removed in a \
              future version."
-        | Uf -> Options.set_debug_uf true
-        | Unsat_core -> Options.set_debug_unsat_core true
-        | Use -> Options.set_debug_use true
+        | Uf ->
+          Options.set_debug_uf true;
+          set_level S.uf
+        | Unsat_core ->
+          Options.set_debug_unsat_core true;
+          set_level S.unsat_core
+        | Use ->
+          Options.set_debug_use true;
+          set_level S.use
         | Warnings ->
           Printer.print_wrn
             "The debug flag 'warning' is deprecated and will be removed in a \
              future version.";
-          Options.set_debug_warnings true
-        | Commands -> Options.set_debug_commands true
-        | Optimize -> Options.set_debug_optimize true
+          Options.set_debug_warnings true;
+          set_level S.warnings
+        | Commands ->
+          Options.set_debug_commands true;
+          set_level S.commands
+        | Optimize ->
+          Options.set_debug_optimize true;
+          set_level S.optimize
       )
 
   let light_flag_term, medium_flag_term, full_flag_term =

src/bin/js/options_interface.ml

@@ -106,7 +106,7 @@ let set_options r =
   set_options_opt Options.set_debug_cc r.debug_cc;
   set_options_opt Options.set_debug_combine r.debug_combine;
   set_options_opt Options.set_debug_constr r.debug_constr;
-  set_options_opt Options.set_debug_explanations r.debug_explanations;
+  set_options_opt Options.set_debug_explanation r.debug_explanation;
   set_options_opt Options.set_debug_fm r.debug_fm;
   set_options_opt Options.set_debug_fpa r.debug_fpa;
   set_options_opt Options.set_debug_gc r.debug_gc;

src/bin/js/worker_interface.ml

@@ -185,7 +185,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanations : bool option;
+  debug_explanation : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;
@@ -286,7 +286,7 @@ let init_options () = {
   debug_cc = None;
   debug_combine = None;
   debug_constr = None;
-  debug_explanations = None;
+  debug_explanation = None;
   debug_fm = None;
   debug_fpa = None;
   debug_gc = None;
@@ -392,7 +392,7 @@ let opt_dbg1_encoding =
        (opt "debug_cc" bool)
        (opt "debug_combine" bool)
        (opt "debug_constr" bool)
-       (opt "debug_explanations" bool)
+       (opt "debug_explanation" bool)
     )
 
 let opt_dbg2_encoding =
@@ -555,7 +555,7 @@ let options_to_json opt =
      opt.debug_cc,
      opt.debug_combine,
      opt.debug_constr,
-     opt.debug_explanations)
+     opt.debug_explanation)
   in
   let dbg_opt2 =
     (opt.debug_fm,
@@ -685,7 +685,7 @@ let options_from_json options =
          debug_cc,
          debug_combine,
          debug_constr,
-         debug_explanations) =
+         debug_explanation) =
       dbg_opt1 in
     let (debug_fm,
          debug_fpa,
@@ -771,7 +771,7 @@ let options_from_json options =
       debug_cc;
       debug_combine;
       debug_constr;
-      debug_explanations;
+      debug_explanation;
       debug_fm;
       debug_fpa;
       debug_gc;

src/bin/js/worker_interface.mli

@@ -68,7 +68,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanations : bool option;
+  debug_explanation : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;

src/bin/text/main_text.ml

@@ -43,4 +43,5 @@ let () =
   AltErgoLib.Printer.init_colors ();
   AltErgoLib.Printer.init_output_format ();
   Signals_profiling.init_signals ();
+  Logs.set_reporter (AltErgoLib.Printer.reporter);
   Solving_loop.main ()

src/lib/dune

@@ -24,6 +24,8 @@
     dune-build-info
     alt_ergo_prelude
     fmt
+    logs
+    logs.fmt
   )
   (preprocess
     (pps
@@ -60,7 +62,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_unix My_list Theories Nest Compat
+    My_zip My_unix My_list Theories Nest Compat Sources
   )
 
  (js_of_ocaml

src/lib/reasoners/adt.ml

@@ -28,7 +28,6 @@
 module Sy = Symbols
 module E  = Expr
 
-
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;

src/lib/structures/explanation.ml

@@ -106,7 +106,7 @@ let add_fresh fe s = S.add fe s
 
 let print fmt ex =
   let open Format in
-  if Options.get_debug_explanations () then begin
+  if Options.get_debug_explanation () then begin
     fprintf fmt "{";
     S.iter (function
         | Literal a -> fprintf fmt "{Literal:%a}, " Satml_types.Atom.pr_atom a

src/lib/util/options.ml

@@ -145,7 +145,7 @@ let debug_bitv = ref false
 let debug_cc = ref false
 let debug_combine = ref false
 let debug_constr = ref false
-let debug_explanations = ref false
+let debug_explanation = ref false
 let debug_fm = ref false
 let debug_intervals = ref false
 let debug_fpa = ref 0
@@ -174,7 +174,7 @@ let set_debug_bitv b = debug_bitv := b
 let set_debug_cc b = debug_cc := b
 let set_debug_combine b = debug_combine := b
 let set_debug_constr b = debug_constr := b
-let set_debug_explanations b = debug_explanations := b
+let set_debug_explanation b = debug_explanation := b
 let set_debug_fm b = debug_fm := b
 let set_debug_intervals b = debug_intervals := b
 let set_debug_fpa i = debug_fpa := i
@@ -203,7 +203,7 @@ let get_debug_bitv () = !debug_bitv
 let get_debug_cc () = !debug_cc
 let get_debug_combine () = !debug_combine
 let get_debug_constr () = !debug_constr
-let get_debug_explanations () = !debug_explanations
+let get_debug_explanation () = !debug_explanation
 let get_debug_fm () = !debug_fm
 let get_debug_intervals () = !debug_intervals
 let get_debug_fpa () = !debug_fpa

src/lib/util/options.mli

@@ -120,8 +120,8 @@ val set_debug_combine : bool -> unit
 (** Set [debug_constr] accessible with {!val:get_debug_constr} *)
 val set_debug_constr : bool -> unit
 
-(** Set [debug_explanations] accessible with {!val:get_debug_explanations} *)
-val set_debug_explanations : bool -> unit
+(** Set [debug_explanation] accessible with {!val:get_debug_explanation} *)
+val set_debug_explanation : bool -> unit
 
 (** Set [debug_fm] accessible with {!val:get_debug_fm} *)
 val set_debug_fm : bool -> unit
@@ -552,8 +552,8 @@ val get_debug_split : unit -> bool
 *)
 val get_debug_matching : unit -> int
 
-(** Get the debugging flag of explanations. *)
-val get_debug_explanations : unit -> bool
+(** Get the debugging flag of explanation. *)
+val get_debug_explanation : unit -> bool
 
 (** Get the debugging flag of triggers. *)
 val get_debug_triggers : unit -> bool

src/lib/util/printer.ml

@@ -396,3 +396,35 @@ let print_smtlib_err ?(flushed=true) s =
   in
   Format.fprintf fmt "(error \"";
   Format.kfprintf k fmt s
+
+let pp_source ppf src =
+  let name = Logs.Src.doc src in
+  Fmt.pf ppf "%s" name
+
+let pp_smtlib_header ppf level =
+  match (level : Logs.level) with
+  | App | Info -> ()
+  | Debug | Warning | Error -> Fmt.pf ppf "; "
+
+let reporter =
+  let report src level ~over k msgf =
+    let k _ = over (); k () in
+    let with_header h _tags k fmt =
+      if Logs.Src.equal src Logs.default then
+        Fmt.kpf k (Options.Output.get_fmt_regular ())
+          ("%a@[" ^^ fmt ^^ "@]@.")
+          pp_smtlib_header level
+      else if Logs.Src.equal src Sources.model then
+        Fmt.kpf k (Options.Output.get_fmt_models ())
+          ("@[" ^^ fmt ^^ "@]@.")
+      else
+        let ppf = Options.Output.get_fmt_diagnostic () in
+        if Options.get_output_with_colors () then
+          Fmt.set_style_renderer ppf `Ansi_tty;
+        Fmt.kpf k ppf ("%a[%a] @[" ^^ fmt ^^ "@]@.")
+          Logs_fmt.pp_header (level, h)
+          pp_source src
+    in
+    msgf @@ fun ?header ?tags fmt -> with_header header tags k fmt
+  in
+  { Logs.report }

src/lib/util/printer.mli

@@ -178,3 +178,12 @@ val print_status_preprocess :
 val print_smtlib_err :
   ?flushed:bool ->
   ('a, Format.formatter, unit) format -> 'a
+
+val reporter : Logs.reporter
+(** Recommended reporter used by both the library and the binary.
+
+    All the sources are printed on [Options.Output.get_fmt_diagnostic ()] but:
+    - [Sources.model] is printed on [Options.Output.get_fmt_models ()]
+    - [Sources.default] is printed on [Options.Output.get_fmt_regular ()]
+
+    The library never prints on [Sources.default] or [Sources.model]. *)