I'm interested in this. In particular, I would like to use the tactics features of MM1 to create MM proofs. Unfortunately, I'm far from being proficient enough to provide good answers to the challenges expressed above. I watched the tutorial and have MM0 installed in VS Code, but so far I've only used MM1 to create a few test proofs to get an intuition of its functionalities. Having a translator that can go back and forth between MM and MM1 would give me a strong reason to dive deeper into it, helping me better understand the world of MM0/MM1 and potentially produce proofs more quickly.
A general suggestion regarding the above challenges is that the translator would ideally preserve the original MM file. That is, if I translate set.mm into set.mm1, and then translate back from set.mm1 into set.mm, the resulting MM file would preferably be identical to the original, except for the parts that I have manually edited. Not sure if this is feasable tho. Regarding point 6 of part 1, I would choose option 1: "Live with it, drop the tactics, metamath was never designed for this". I'm interested in using MM1 tactics to create MM proofs, but I'm not interested in preserving the MM1 tactics themselves. A "fringe idea" could be to export those MM1 tactics as a separate Rumm file, but Rumm is currently very primitive and not under active development (despite my efforts), so I don't think it's worth getting too hung up on it. Perhaps, instead of translating the entire database, one could extract only the portion of set.mm that the user intends to revise. In metamath.exe, there is "write source <output-name> /extract <theorem>" that allows the user to create a MM file containing only the material needed to prove a specified theorem. A similar approach could be used to derive a smaller MM1 file from MM. It would be really cool to have a "flawless" translation between MM and MM1 because it would essentially be equivalent to having tactics directly in Metamath, which I think would provide a significant gain in the long term (tho, I'm not sure whether my aim aligns with the constraints of the MM0/MM1 language). -- 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 visit https://groups.google.com/d/msgid/metamath/4654b1d5-cb5f-4f77-ada6-0c6a166b80a0n%40googlegroups.com.
