On Fri, 18 Oct 2019 10:26:54 -0700 (PDT), Norman Megill <[email protected]>
wrote:
> Yes, using the metamath.exe program,
>
> MM> read set.mm
> MM> save proof * /normal
> MM> write source set.mm
>
> The output file size will be very large, although I haven't checked its
> size recently. It will also be slower to read and verify.
Running:
metamath 'read set.mm' 'save proof * /normal' 'write source
set-uncompressed.mm' quit
wc set*.mm
Produces:
595027 4485207 34531089 set.mm
2605454 45188012 191634836 set-uncompressed.mm
Those are the the counts of lines, words, and bytes. Looking at the bytes we
see:
34,531,089 - the compressed form is ~34.5MB.
191,634,836 - the uncompressed form is ~191.6MB.
Both are in ASCII, so you can use a compression format like .gz to
get even more space savings.
--- David A. Wheeler
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1iLYcF-0004Nr-IG%40rmmprod07.runbox.
