I have been playing some more with mm0 lately and made some progress : - I implemented AGAIN a mm0 parser, a mmu parser, a mm0/mmu proof checker with a different design (my first try was with immutable structures and lots of allocations, I tried to reduce allocations by using mutable structures/views/events)
My first try took 15 s to proof check set.mm.mm0 My second (mutable) try took 3min30s (lol), which made me realize how stupid I can be. My third try is at 22s (but with unique string usage, a lot less memory) and I realized a few things about parsers, so there is still room for performance improvements. I would really like to reach something like 5s at some point, which might not be easy when you have to handle 480 MB of data. but performance is not the issue there. A second go at implementing parsers/proof checkers gave me a chance to further understand mm0/mmu and how things should be done. So, my second implementation is actually more correct. Also, it is a good enough foundation, for me to start working on : - adding mm0 features to set.mm - Mephistolus on mm0 So, I'll now work on writing a patcher routine that takes set.mm.mm0/set.mm.mmu and slowly : - add simple notations (to make the parser work with stuff like 1 + 2 + 3) - replace terms with definitions - replace axioms on terms with theorems on definitions (using conversibility proofs) - replace usage co like "co (1 + 2 )" with regular binary operators like "1+2" So far, I have only changed c1 into 1 (same for c2, c3, c4, c5, c6, c7, c8, c10). Which requires to replace every instance of "c1" in the mmu and mm0 files with "1" (some work, but not very hard) and added simple notations for the logical operators (this is even easier) but now, I'll try to do something hard : - either replace the term for logical or with a definition (which means refactoring lots of proofs) - or replacing the co usage for +, with using a term (which probably means more refactoring) I am not at all sure that I'll be able to pull this off. I do not know how long it will take me either. (I only know that if I can pull this off, I'll be able to improve stuff a lot) I'll probably go with replacing the or term with a definition (which will make me able to write conversibility proof, a necessary requirement for me). Wish me luck ! Best regards, Olivier ps : I'll soon publish my patched mm0/mmu files (in case someone is interested) ans also my mm0/mmu parsers (first). Those can/should still be improved but it can be done later. Stay home and stay safe ! :) -- 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/65485950-3987-4be2-8746-cf1e93df5267%40googlegroups.com.
