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

feat(frontends/lean/builtin_cmds): write/read compacted region file

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-20 16:35:37 -07:00
parent 8944cb6951
commit fd9bc9e15b
1 changed files with 24 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -589,9 +589,31 @@ environment compact_tst_cmd(parser & p) {
}
tout() << "compactor size: " << compactor.size() << "\n";
}
compacted_region r(compactor);
{
timeit timer(out, "compacted region time");
timeit timer(out, "saving file 'compact.out'");
FILE * fp = fopen("compact.out", "wb");
if (fp == nullptr) throw exception("failed to open file 'compact.out'");
size_t sz = compactor.size();
fwrite(&sz, sizeof(size_t), 1, fp);
if (fwrite(compactor.data(), 1, sz, fp) != sz)
throw exception("failed to write file 'compact.out'");
fclose(fp);
}
void * in_buffer;
size_t in_sz;
{
timeit timer(out, "reading file 'compact.out'");
FILE * fp = fopen("compact.out", "rb");
if (fp == nullptr) throw exception("failed to open file 'compact.out'");
fread(&in_sz, sizeof(size_t), 1, fp);
in_buffer = malloc(in_sz);
if (fread(in_buffer, 1, in_sz, fp) != in_sz)
throw exception("failed to read file 'compact.out'");
fclose(fp);
}
compacted_region r(in_sz, in_buffer);
{
timeit timer(out, "compacted region fixing pointers time");
unsigned i = 0;
while (r.read() != nullptr) {
i++;