From 03e01c5adce7d72cc212b23956f15dedef4e3244 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sun, 25 Dec 2022 12:47:56 +0100
Subject: [PATCH] Vendor progress lib

---
 .gitmodules      |  3 +++
 dolmen_bin.opam  | 11 +++++------
 dolmen_loop.opam |  1 -
 dune             |  3 +++
 src/bin/dune     |  2 ++
 src/bin/main.ml  |  7 ++++---
 src/loop/dune    |  2 +-
 vendor/progress  |  1 +
 8 files changed, 19 insertions(+), 11 deletions(-)
 create mode 100644 .gitmodules
 create mode 160000 vendor/progress

diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 000000000..cb9cd24ad
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "vendor/progress"]
+	path = vendor/progress
+	url = https://github.com/Gbury/progress.git
diff --git a/dolmen_bin.opam b/dolmen_bin.opam
index c3507b30c..5afadec61 100644
--- a/dolmen_bin.opam
+++ b/dolmen_bin.opam
@@ -14,15 +14,14 @@ depends: [
   "dolmen_type" {= version }
   "dolmen_loop" {= version }
   "dolmen_model" {= version }
+  "odoc" { with-doc }
   "dune" { >= "3.0" }
   "fmt"
   "cmdliner" { >= "1.1.0" }
-  "odoc" { with-doc }
-  "progress"
-  "terminal"
-]
-pin-depends: [
-  [ "progress" "git+https://github.com/Gbury/progress.git#custom" ]
+  "pp_loc" { >= "2.0.0" }
+# These two are currently vendored
+#  "progress"
+#  "terminal"
 ]
 depopts: [
   "memtrace"
diff --git a/dolmen_loop.opam b/dolmen_loop.opam
index 030ef34e3..cae0c8d7e 100644
--- a/dolmen_loop.opam
+++ b/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"
diff --git a/dune b/dune
index 1bcb14139..3b7203e6c 100644
--- a/dune
+++ b/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))
diff --git a/src/bin/dune b/src/bin/dune
index 3a5f51545..ff1843e95 100644
--- a/src/bin/dune
+++ b/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
diff --git a/src/bin/main.ml b/src/bin/main.ml
index 468fdace7..17dd2ed13 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -32,9 +32,10 @@ let finally st e =
   | None -> st
   | Some (bt,exn) ->
     (* Print the backtrace if requested *)
-    if State.(get bt) st then (
-      (* TODO: use Tui *)
-      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 =
diff --git a/src/loop/dune b/src/loop/dune
index cc3081fcf..0ed4ff9ce 100644
--- a/src/loop/dune
+++ b/src/loop/dune
@@ -4,7 +4,7 @@
   (instrumentation (backend bisect_ppx))
   (libraries
     ; External deps
-    gen unix fmt pp_loc terminal progress
+    gen unix fmt
     ; main dolmen deps, with versioned languages deps
     dolmen
     dolmen.intf dolmen.std dolmen.class
diff --git a/vendor/progress b/vendor/progress
new file mode 160000
index 000000000..019cc6ae1
--- /dev/null
+++ b/vendor/progress
@@ -0,0 +1 @@
+Subproject commit 019cc6ae1622535ce260694f19eaaec3a360ad27