Add progress bars

.github/workflows/build.yml

@@ -56,9 +56,11 @@ jobs:
     # Build/test steps
     # ----------------
     steps:
-    # checkout the repo (full clone, necessary for push later)
+    # checkout the repo
     - name: Checkout the repo
       uses: actions/checkout@v3
+      with:
+        submodules: recursive
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2

.github/workflows/install.yml

@@ -70,6 +70,8 @@ jobs:
     # checkout the repo (full clone, necessary for push later)
     - name: Checkout the repo
       uses: actions/checkout@v3
+      with:
+        submodules: recursive
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2

.github/workflows/release.yml

@@ -58,6 +58,8 @@ jobs:
     # checkout the repo
     - name: Checkout the repo
       uses: actions/checkout@v3
+      with:
+        submodules: recursive
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2

.github/workflows/test.yml

@@ -49,9 +49,11 @@ jobs:
     # Build/test steps
     # ----------------
     steps:
-    # checkout the repo (full clone, necessary for push later)
+    # checkout the repo
     - name: Checkout the repo
       uses: actions/checkout@v3
+      with:
+        submodules: recursive
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "vendor/progress"]
+	path = vendor/progress
+	url = https://github.com/Gbury/progress.git

dolmen_bin.opam

@@ -14,10 +14,23 @@ depends: [
   "dolmen_type" {= version }
   "dolmen_loop" {= version }
   "dolmen_model" {= version }
+  "odoc" { with-doc }
   "dune" { >= "3.0" }
   "fmt"
   "cmdliner" { >= "1.1.0" }
-  "odoc" { with-doc }
+  "pp_loc" { >= "2.0.0" }
+  "mtime" {>= "1.1.0" & < "2.0.0" }
+# These two are currently vendored
+#  "progress"
+#  "terminal"
+# thus we need their deps
+  "stdlib-shims"
+  "fmt" {>= "0.8.5"}
+  "logs" {>= "0.7.0"}
+  "uucp" {>= "2.0.0"}
+  "uutf" {>= "1.0.0"}
+  "vector"
+  "optint" {>= "0.1.0"}
 ]
 depopts: [
   "memtrace"

dolmen_loop.opam

@@ -15,7 +15,6 @@ depends: [
   "dune" { >= "3.0" }
   "gen"
   "odoc" { with-doc }
-  "pp_loc" { >= "2.0.0" }
 ]
 tags: [ "logic" "computation" "automated theorem prover" ]
 homepage: "https://github.com/Gbury/dolmen"

dune

@@ -1,3 +1,6 @@
+; directory for vendored libs
+(vendored_dirs vendor)
+
 (env
   ; Ensure no inlinging takes place in dev mode to have more accurate backtraces
   (dev (ocamlopt_flags :standard -inline 0))

src/bin/dune

@@ -6,6 +6,8 @@
   (libraries
     ; external deps
     cmdliner fmt gen
+    pp_loc progress terminal
+    mtime mtime.clock.os
     ; dolmen deps
     dolmen dolmen.intf dolmen.std
     dolmen_type dolmen_loop dolmen_model

src/bin/errors.ml

@@ -14,35 +14,35 @@ let exn st = function
   | Dolmen_loop.Pipeline.Sigint ->
     Format.pp_print_flush Format.std_formatter ();
     Format.pp_print_flush Format.err_formatter ();
-    Loop.State.error st Dolmen_loop.Report.Error.user_interrupt ()
+    State.error st Dolmen_loop.Report.Error.user_interrupt ()
 
   (* Timeout, potentially wrapped by the typechecker *)
   | Dolmen_loop.Alarm.Out_of_time ->
     Format.pp_print_flush Format.std_formatter ();
-    Loop.State.error st Dolmen_loop.Report.Error.timeout ()
+    State.error st Dolmen_loop.Report.Error.timeout ()
 
   | Dolmen_loop.Alarm.Out_of_space ->
     Format.pp_print_flush Format.std_formatter ();
     Format.pp_print_flush Format.err_formatter ();
-    Loop.State.error st Dolmen_loop.Report.Error.spaceout ()
+    State.error st Dolmen_loop.Report.Error.spaceout ()
 
   (* Internal Dolmen Expr errors *)
   | Dolmen.Std.Expr.Ty.Bad_arity (c, l) ->
     let pp_sep fmt () = Format.fprintf fmt ";@ " in
-    Loop.State.error st Dolmen_loop.Report.Error.internal_error
+    State.error st Dolmen_loop.Report.Error.internal_error
       (Format.dprintf
          "@[<hv>Internal error: Bad arity for type constant '%a',\
           @ which was provided arguments:@ [@[<hv>%a@]]@]"
          Dolmen.Std.Expr.Print.ty_cst c
          (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) l)
   | Dolmen.Std.Expr.Type_already_defined c ->
-    Loop.State.error st Dolmen_loop.Report.Error.internal_error
+    State.error st Dolmen_loop.Report.Error.internal_error
       (Format.dprintf
          "@[<hv>Internal error: Type constant '%a' was already defined earlier,\
           @ cannot re-define it.@]"
          Dolmen.Std.Expr.Print.id c)
   | Dolmen.Std.Expr.Term.Wrong_type (t, ty) ->
-    Loop.State.error st Dolmen_loop.Report.Error.internal_error
+    State.error st Dolmen_loop.Report.Error.internal_error
       (Format.dprintf
          "@[<hv>Internal error: A term of type@ %a@ was expected \
           but instead got a term of type@ %a@]"
@@ -52,5 +52,5 @@ let exn st = function
   (* Generic catch-all *)
   | exn ->
     let bt = Printexc.get_raw_backtrace () in
-    Loop.State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)
+    State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt)
 

src/bin/loop.ml

@@ -1,12 +1,9 @@
 
 (* This file is free software, part of dolmen. See file "LICENSE" for more information *)
 
-module State = Dolmen_loop.State
 module Pipeline = Dolmen_loop.Pipeline.Make(State)
-
-module Parser = Dolmen_loop.Parser.Make(State)
+module Parser = Dolmen_loop.Parser.Make(State)(Stats)
 module Header = Dolmen_loop.Headers.Make(State)
 module Typer = Dolmen_loop.Typer.Typer(State)
-module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Typer)
-module Check = Dolmen_model.Loop.Make(State)(Parser)(Typer)(Typer_Pipe)
-
+module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Stats)(Typer)
+module Check = Dolmen_model.Loop.Make(State)(Stats)(Parser)(Typer)(Typer_Pipe)

src/bin/main.ml

@@ -1,19 +1,18 @@
 
 (* This file is free software, part of dolmen. See file "LICENSE" for more information *)
 
-
 (* Debug printing *)
 (* ************** *)
 
 let debug_parsed_pipe st c =
-  if Loop.State.get Loop.State.debug st then
+  if State.get State.debug st then
     Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
       Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc
       Dolmen.Std.Statement.print c;
   st, c
 
 let debug_typed_pipe st stmt =
-  if Loop.State.get Loop.State.debug st then
+  if State.get State.debug st then
     Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
       Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc
       Loop.Typer_Pipe.print stmt;
@@ -24,6 +23,7 @@ let debug_typed_pipe st stmt =
 (* ************************ *)
 
 let handle_exn st exn =
+  let () = Tui.finalise_display () in
   let _st = Errors.exn st exn in
   exit 125
 
@@ -32,20 +32,21 @@ let finally st e =
   | None -> st
   | Some (bt,exn) ->
     (* Print the backtrace if requested *)
-    if Loop.State.(get bt) st then (
-      Format.eprintf "foo ?!@.";
-      Printexc.print_raw_backtrace stdout bt);
+    if State.(get bt) st then begin
+      Tui.eprintf "%s@."
+        (Printexc.raw_backtrace_to_string bt)
+    end;
     handle_exn st exn
 
 let run st =
-  if Loop.State.get Loop.State.debug st then begin
+  if State.get State.debug st then begin
     Dolmen.Std.Expr.Print.print_index := true;
     ()
   end;
   let st, g =
     try
       Loop.Parser.parse_logic [] st
-        (Loop.State.get Loop.State.logic_file st)
+        (State.get State.logic_file st)
     with exn -> handle_exn st exn
   in
   let st =
@@ -62,8 +63,9 @@ let run st =
       )
     )
   in
+  let () = Tui.finalise_display () in
   let st = Loop.Header.check st in
-  let _st = Dolmen_loop.State.flush st () in
+  let _st = State.flush st () in
   ()
 
 (* Warning/Error list *)

src/bin/options.ml

@@ -18,7 +18,7 @@ let profiling_section = "PROFILING"
 
 type cmd =
   | Run of {
-      state : Loop.State.t;
+      state : State.t;
     }
   | List_reports of {
       conf : Dolmen_loop.Report.Conf.t;
@@ -244,9 +244,9 @@ let c_size = parse_size, print_size
 
 let report_style =
   Arg.enum [
-    "minimal", Loop.State.Minimal;
-    "regular", Loop.State.Regular;
-    "contextual", Loop.State.Contextual;
+    "minimal", State.Minimal;
+    "regular", State.Regular;
+    "contextual", State.Contextual;
   ]
 
 
@@ -324,6 +324,7 @@ let mk_run_state
     header_lang_version
     smtlib2_forced_logic type_check check_model
     debug report_style max_warn reports syntax_error_ref
+    progress_enabled progress_mem
   =
   (* Side-effects *)
   let () = Option.iter Gc.set gc_opt in
@@ -337,11 +338,17 @@ let mk_run_state
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
   let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
   (* State creation *)
-  Loop.State.empty
-  |> Loop.State.init
+  State.empty
+  |> State.init
     ~bt ~debug ~report_style ~reports
     ~max_warn ~time_limit ~size_limit
     ~logic_file ~response_file
+  |> Stats.init
+    ~mem:progress_mem
+    ~max_mem:(int_of_float size_limit)
+    ~enabled:progress_enabled
+    ~typing:type_check
+    ~model:check_model
   |> Loop.Parser.init
     ~syntax_error_ref
     ~interactive_prompt:Loop.Parser.interactive_prompt_lang
@@ -432,8 +439,8 @@ let reports =
 (* ************************************************************************* *)
 
 let mk_file lang mode input =
-  let dir,source = Loop.State.split_input input in
-  Loop.State.mk_file ?lang ?mode dir source
+  let dir,source = State.split_input input in
+  State.mk_file ?lang ?mode dir source
 
 let logic_file =
   let docs = common_section in
@@ -517,7 +524,7 @@ let state =
   let size =
     let doc = "Stop the program if it tries and use more the $(docv) memory space. " ^
               "Accepts usual suffixes for sizes : k,M,G,T. " ^
-              "Without suffix, default to a size in octet." in
+              "Without suffix, default to a size in bytes/octet." in
     Arg.(value & opt c_size 1_000_000_000. &
          info ["s"; "size"] ~docv:"SIZE" ~doc ~docs)
   in
@@ -571,19 +578,37 @@ let state =
          would be too long), and lastly $(b,minimal) prints each report on one line"
     in
     Arg.(value & opt report_style Contextual & info ["report-style"] ~doc ~docs:error_section)
-    in
+  in
   let max_warn =
     let doc = Format.asprintf
         "Maximum number of warnings to display (excess warnings will be
          counted and a count of silenced warnings reported at the end)." in
     Arg.(value & opt int max_int & info ["max-warn"] ~doc ~docs:error_section)
+  in
+  let syntax_error_ref =
+    let doc = Format.asprintf
+        "Print the syntax error reference number when a syntax error is raised."
     in
-    let syntax_error_ref =
-      let doc = Format.asprintf
-         "Print the syntax error reference number when a syntax error is raised."
-      in
-      Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section)
+    Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section)
+  in
+  let progress_enabled =
+    let default = false in
+    let pos_flag =
+      let doc = Format.asprintf "Enable printing of progress bars." in
+      Arg.info ["p"; "progress"] ~doc ~docs:profiling_section
+    in
+    let neg_flag =
+      let doc = Format.asprintf "Disable printing of progress bars." in
+      Arg.info ["no-progress"] ~doc ~docs:profiling_section
     in
+    Arg.(value & vflag default [true, pos_flag; false, neg_flag])
+  in
+  let progress_mem =
+    let doc = Format.asprintf
+        "Compute memory usage in progress info. Note that this may slow \
+         down dolmen significantly (experiments suggest around 3x)." in
+    Arg.(value & opt bool true & info ["progress-mem"] ~doc ~docs:profiling_section)
+  in
   Term.(const mk_run_state $ profiling_t $
         gc $ gc_t $ bt $ colors $
         abort_on_bug $
@@ -592,7 +617,8 @@ let state =
         header_check $ header_licenses $
         header_lang_version $
         force_smtlib2_logic $ typing $ check_model $
-        debug $ report_style $ max_warn $ reports $ syntax_error_ref)
+        debug $ report_style $ max_warn $ reports $ syntax_error_ref $
+        progress_enabled $ progress_mem)
 
 
 (* List command term *)
@@ -604,10 +630,10 @@ let cli =
     | false, None ->
       `Ok (Run { state; })
     | false, Some report ->
-      let conf = Loop.State.get Loop.State.reports state in
+      let conf = State.get State.reports state in
       `Ok (Doc { report; conf; })
     | true, None ->
-      let conf = Loop.State.get Loop.State.reports state in
+      let conf = State.get State.reports state in
       `Ok (List_reports { conf; })
     | true, Some _ ->
       `Error (false,