Another possibility which I did not mention in that post is to add constraints to MM1 (or specifically mm0-rs) to allow it to operate in "MM mode", where certain things are disallowed to make translation easier. That makes more sense if your goal is to use MM1 to develop set.mm rather than embedding peano.mm1 et al into set.mm.
A less ambitious goal which seems practically doable would be to allow MM1 to import MM (this is another version of MM -> MM0 translation which already exists), and then just produce small scale MM1 -> MM translations like single theorems, using an approach similar to mmj2 or rumm where you get some code blocks to copy into set.mm. If all the theorem statements are written on the MM side then this solves most of the issues about variable naming etc. On Sun, May 25, 2025 at 11:10 PM Gino Giotto <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/4654b1d5-cb5f-4f77-ada6-0c6a166b80a0n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuAyKx%3D3ADrbdm2r%3D2W2sgiVc%2BdLbUX-_ruUf77rhCAkQ%40mail.gmail.com.
