max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/builtin_cmds): do not include time spent copying memory

Browse source 
We will read the data from the disk and give it directly to the
compacted_region object
This commit is contained in:
Leonardo de Moura 2018-08-20 15:49:54 -07:00
parent 38b23431a3
commit 8944cb6951
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/builtin_cmds.cpp
View file

@ -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();