add a simple binary to dump proof traces

proof-trace-dump.sh

@@ -0,0 +1,2 @@
+#!/usr/bin/env sh
+exec dune exec --profile=release src/proof-trace-dump/proof_trace_dump.exe -- $@

src/main/main.ml

@@ -31,6 +31,7 @@ let p_gc_stat = ref false
 let p_progress = ref false
 let proof_file = ref ""
 let proof_store_memory = ref false
+let proof_store_file = ref ""
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -71,6 +72,7 @@ let argspec = Arg.align [
     "--proof", Arg.Set p_proof, " print proof";
     "--no-proof", Arg.Clear p_proof, " do not print proof";
     "--proof-in-memory", Arg.Set proof_store_memory, " store temporary proof in memory";
+    "--proof-trace-file", Arg.Set_string proof_store_file, " store temporary proof in given file (no cleanup)";
     "-o", Arg.Set_string proof_file, " file into which to output a proof";
     "--model", Arg.Set p_model, " print model";
     "--no-model", Arg.Clear p_model, " do not print model";
@@ -104,13 +106,15 @@ let main_smt () : _ result =
 
   (* call [k] with the name of a temporary proof file, and cleanup if necessary *)
   let run_with_tmp_file k =
+    (* TODO: use memory writer if [!proof_store_memory] *)
     if enable_proof_ then (
-      let file = ".sidekick-trace.dat" in
+      if !proof_store_file <> "" then (
+        let file = !proof_store_file in
         k file
-      (*  TODO
+      ) else (
         CCIO.File.with_temp
           ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
-          *)
+      )
     ) else (
       k "/dev/null"
     )

src/proof-trace-dump/dune

@@ -0,0 +1,6 @@
+
+(executable
+  (name proof_trace_dump)
+  (modes native)
+  (libraries containers sidekick.util sidekick-base.proof-trace)
+  (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))

src/proof-trace-dump/proof_trace_dump.ml

@@ -0,0 +1,35 @@
+
+module CS = Chunk_stack
+module Proof_ser = Sidekick_base_proof_trace.Proof_ser
+
+let parse_file (file:string) : unit =
+  Log.debugf 2 (fun k->k"parsing file %S" file);
+
+  CS.Reader.with_file_backward file @@ fun reader ->
+
+  let n = ref 0 in
+  let rec display_steps () =
+    CS.Reader.next reader
+      ~finish:(fun () -> ())
+      ~yield:(fun b i _len ->
+          let decode = {Proof_ser.Bare.Decode.bs=b; off=i} in
+          let step = Proof_ser.Step.decode decode in
+          incr n;
+          Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step;
+          display_steps();
+        );
+  in
+  display_steps();
+  Format.printf "read %d steps@." !n;
+  ()
+
+let () =
+  let file = ref "" in
+  let opts = [
+    "--bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces";
+    "-d", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> file := f) "proof-trace-dump <file>";
+  if !file = "" then failwith "please provide a file";
+
+  parse_file !file