Is there a way to uncompress the entire metamath database?

[Juho Kupiainen]

I would like to see the entire metamath database in uncompressed format. Is there a way to do this?

[Norman Megill]

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.

There are actually 6 formats recognized by metamath.exe (though only "compressed" and "normal" are official).  These are discussed here:
https://groups.google.com/d/msg/metamath/7uJBdCd9tbc/r5iRJifpAgAJ
in case another format would be more useful for your project.

Norm

[David A. Wheeler]

On Fri, 18 Oct 2019 10:26:54 -0700 (PDT), Norman Megill <n...@alum.mit.edu> 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

[Jon P]

You probably know already Juho but on the web there are uncompressed versions with nice formatting and hyperlinks. I think this might be easier for reading than decompressing the source file. 

Also there is "Structured View" in the top right of each proof page which gives "normal" mathematical notation. 

http://us.metamath.org/mpeuni/mmtheorems.html