eimm -i < test.mmp chokes on lines starting with * and !, also labels starting with d

[LM]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/207d31b0-3426-4620-8d78-089967874e72n%40googlegroups.com.

[Mario Carneiro]

> 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.

[LM]

Thanks for your detailed answers.

I had assumed that for import and export the mmP files were most suitable, but actually the mmT files are more suitable.

I hadn't set my MMT folder initially (a bit confusing with all the different RunParams.txt files, and the many options which can be set.).

The menu TL-> Unify + Store in MMT Folder does what I need. But didn't pop up any folder selection menu when tried it... which is handy once you know what it does, but at first one doesn't and its a bit of a mystery of where this MMT folder would be, so a beginner naturally gravitates effort towards the File menu (where opening and saving proofs in mmP format occurs), theres also the luring "Export via GMMF" in the File menu.

I was hoping for directly set.mm compatible snippets, in separate files, so I can append it to my sandbox.mm (which includes set.mm).

Luckily this exactly what the MMT format Theorem Loader menu does! 

So my workflow is that I have  a script and modified RunParams (to set the MMT directory). The tell mmj2 to load my sandbox.mm ( which implicitly loads set.mm).

I can thus CTRL-G(et) any proof for inspection / inspiration, or make a new proof, when finished I renumber and TL->Unify+StoreMMT.

Then I append the resulting file to my sandbox.mm: cat myMMT/someproof.mmt >> sandbox.mm

Then I can do some cosmetic commenting etc either on the .mmt file before concatenating to sandbox.mm or else if after appending to sandbox.mm, I can still edit it in sandbox.mm using in my case nano.

So I never need to use a pointer device (mouse) to select and copy/paste fragments.

Again, thanks for your patience in guiding me around.

I had some email conversation in the past with Norm, back when I implemented  a non-publish worthy verifier (as an exercise or check that I understood the verifier itself, as its too easy to nod in agreement while reading the book)

Is there a way to download all of the Metamath google groups discussions without scraping? I'm sure theres many interesting observations, and having a physical backup would be nice.

For fun I went all the way back to the earliest messages, and noticed some bit rot already: a stale URL to an introductory pdf on formal verification, without title in the message. Luckily I was able to find that file by filename on the web.

I don't know how long that would be possible with more and more transitioning to ML search engines.

There is a search bar in Google Groups, but I'm not sure how to make it for example emit all URL's in the emails, in the hopes of recovering as many references to convserve the history of metamath.

If we could have a bulk dump of the Metamath group conversations (names or emails obscured would be fine), it would be easy to grep for URL's, sort them by domain, etc... in order to efficiently locate broken links.

Also Norm was always exceptionally kind in his communications.

I feel like I lack some kind of biography of Norm, apart from a single youtube video in which he appears (the discussion with Stephen Wolfram, Norm and You) and apart from the academic articles I can find via semantic scholar, 

Possibly thats why I feel hoarding these google groups messages ..

Op woensdag 19 april 2023 om 17:57:40 UTC+2 schreef di....@gmail.com: