> I'm not sure how other people are using mmj2, and how they export/import...
Ah, I just realized that you are talking about a subsystem of mmj2 which is intended for export? If so it makes sense that it would be out of date, because I am the mmj2 maintainer and I have never used or attempted to figure out how to use that feature, so it has most likely bit-rot. As for "how do people export/import from mmj2": for import, I make a stub proof in set.mm including the full theorem statement, comments, etc, prove it by ?, restart mmj2, and locate the theorem to work on it. For export, when the proof is complete it prints a big block of text, and I copy that block into the .mm file. On Wed, Apr 19, 2023 at 11:51 AM Mario Carneiro <[email protected]> wrote: > You can use the "Renumber" option in the menu of mmj2 to get rid of "d" > and other alphabetic naming. The ! steps should also go away once you have > proved the step, meaning that complete proofs will hopefully not have these > things. * comments though are ubiquitous in mmj2 proof worksheets and I > don't know any method other than manually removing them if they cause > problems. > > But really, this all sounds like problems with eimm (which I don't know > much about). Parsing the full syntax of mmj2-acceptable worksheets is a bit > annoying because it is very forgiving of malformed steps, but I think it is > reasonable to at least be able to support the kinds of worksheets that mmj2 > actually generates. I would assume that it is just an out of date parser, > since mmj2 was not always capable of parsing alphabetic step names, and did > not always put !, although it has put * as long as I can remember. > > Mario > > On Wed, Apr 19, 2023 at 8:49 AM LM <[email protected]> wrote: > >> I am probably doing something wrong, but when I try using eimm it doesn't >> like the .mmp saved by mmj2. >> >> the labels are expected to be purely numeric, while the autogenerated >> labels have a 'd' prefix. >> >> it also fails to ignore * comments >> >> >> I'm not sure how other people are using mmj2, and how they >> export/import... >> >> Greetings, >> Ludwig >> >> -- >> 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/207d31b0-3426-4620-8d78-089967874e72n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/207d31b0-3426-4620-8d78-089967874e72n%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 on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvBfmWzTz%3DHb0vdvARo2Rc1mAgdviQkSOFV8cZp0m3PUg%40mail.gmail.com.
