diff --git a/dune b/dune index af1fdb08..1b55029c 100644 --- a/dune +++ b/dune @@ -1 +1,8 @@ (data_only_dirs tests) + +(env + (_ + (flags :standard -warn-error -a+8+9 -w +a-4-32-40-41-42-44-48-70 -color + always -strict-sequence -safe-string -short-paths) + (ocamlopt_flags :standard -O3 -color always -unbox-closures + -unbox-closures-factor 20))) diff --git a/sidekick.opam b/sidekick.opam index c9da08f3..49f9e558 100644 --- a/sidekick.opam +++ b/sidekick.opam @@ -21,6 +21,7 @@ depends: [ ] depopts: [ "mtime" # for profiling stuff + "memtrace" # memory profiling "zarith" # for arithmetic ] conflicts: [ diff --git a/src/base/Proof.ml b/src/base/Proof.ml index 6f243a84..8cca974b 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -46,11 +46,10 @@ type term = Term.t type t = { mutable enabled : bool; - config: Config.t; buf: Buffer.t; out: Proof_ser.Bare.Encode.t; mutable storage: Storage.t; - mutable dispose: unit -> unit; + dispose: unit -> unit; mutable steps_writer: CS.Writer.t; mutable next_id: int; map_term: term_id Term.Tbl.t; (* term -> proof ID *) @@ -91,12 +90,12 @@ let create ?(config=Config.default) () : t = let dispose () = close_out oc in Storage.On_disk (file, oc), w, dispose in - let buf = Buffer.create 1024 in + let buf = Buffer.create 1_024 in + let out = Proof_ser.Bare.Encode.of_buffer buf in { enabled=config.Config.enabled; - config; next_id=1; buf; - out=Proof_ser.Bare.Encode.of_buffer buf; + out; map_term=Term.Tbl.create 32; map_fun=Fun.Tbl.create 32; steps_writer; storage; dispose; diff --git a/src/dune b/src/dune deleted file mode 100644 index 17d9707a..00000000 --- a/src/dune +++ /dev/null @@ -1,7 +0,0 @@ - -(env - (_ - (flags :standard -warn-error - -a+8+9 -w +a-4-32-40-41-42-44-48 - -color always -strict-sequence -safe-string -short-paths) - (ocamlopt_flags :standard -O3 -color always -unbox-closures -unbox-closures-factor 20)))