On Monday, May 2, 2022 at 6:26:00 PM UTC-4 Benoit wrote: > I was writing a Metamath verifier some time ago (in OCaml), and I found > looking at mmverify.py in Python by Raph Levien very useful, see > https://github.com/david-a-wheeler/mmverify.py/blob/master/mmverify.py > (the "proof decompression" was added by Scott Fenton). Actually, I made a > PR that avoids decompression and directly verifies the compressed proofs > (making a four-fold speedup), that adds some comments (some especially > relevant to your questions) and typing annotations for clarity, and that > separates the different steps (see the three functions "treat_step", > "treat_normal_proof", and "treat_compressed_proof"), see > https://github.com/benjub/mmverify.py/blob/faster/mmverify.py. >
Ah, very nice. thanks for the reference. I was reading through the original mmverify to see how compressed proofs were handled. I think decompressing prior to verification is harder to follow because then you have to figure out which proofs are part of a particular subproof. I guess doing verification at the same time as decompression also has the nice property of being faster. Unrelated: my verifier is also in OCaml. I don't expect it to set any speed records; my ambition is more in the direction of making a web-based proof visualization tool, and perhaps also a proof assistant UI. > With compressed proofs, we add another data structure, the "heap", which >> also consists of statements but has random access unlike the stack. The Z >> command pushes the thing on top of the stack to the heap (labeled with the >> next available number). When you reference a heap element, that statement >> is pushed onto the stack. So you can do a big subproof to generate some >> statement, save it to the heap (which does not pop it from the stack), and >> then recall it later to use that same statement 2 or more times in the same >> proof without having to go through all the steps of the proof again. >> > Your whole explanation, and especially the heap analogy, is extremely helpful; thank you so much! - Philip -- 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/6b41900c-1514-4f3f-b0de-5e0a302cf985n%40googlegroups.com.
