In short,
READ '/path/to/database.mm'
SAVE PROOF * /NORMAL
WRITE SOURCEThat should convert all proofs from COMPRESSED into NORMAL format and save it to disk. The WRITE command will ask for the output file name if you wish to save to a different file instead of overwriting. However, such an extreme measure might not be necessary, depending on what you're doing. If you are looking to just explore and read proofs, using the native facilities of the metamath frontend might be a lot more convenient, e.g. SHOW LABELS, SHOW PROOF, etc. If you give us a little more detail about what you're trying to do, we might be able to give you some better ideas. On Fri, Oct 18, 2019 at 08:48:35AM -0700, Juho Kupiainen wrote: > I would like to read the entire set.mm database in uncompressed format. Is > there a way to uncompress the whole database? > > -- > 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/b170460b-d0b2-42f4-b44c-8a69954382c0%40googlegroups.com. -- 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/20191019014821.GC16041%40lang.
signature.asc
Description: PGP signature
