From 8944cb6951e3ef7cf74ea1de3490aca1130d655a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Aug 2018 15:49:54 -0700 Subject: [PATCH] fix(frontends/lean/builtin_cmds): do not include time spent copying memory We will read the data from the disk and give it directly to the compacted_region object --- src/frontends/lean/builtin_cmds.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b1869e7f74..fad0dd0500 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -589,9 +589,9 @@ environment compact_tst_cmd(parser & p) { } tout() << "compactor size: " << compactor.size() << "\n"; } + compacted_region r(compactor); { timeit timer(out, "compacted region time"); - compacted_region r(compactor); unsigned i = 0; while (r.read() != nullptr) { i++; @@ -611,9 +611,9 @@ environment compact_tst_cmd(parser & p) { s << e; tout() << "serialization size: " << sout.str().size() << "\n"; } + std::istringstream in(sout.str()); + deserializer d(in); { - std::istringstream in(sout.str()); - deserializer d(in); timeit timer1(out, "deserializing objects"); for (unsigned i = 0; i < objects_to_write.size(); i++) { d.read_object();