Note that the syntax is a bit more flexible than that document implies; one of my first early additions to mmj2 was to make the step:hyp:ref blob accept more abbreviated forms. Also, an optional "!" also precedes the blob, this indicates whether it is to be solved using the default automation.
The unabbreviated syntax is (!)?step:hyps:ref, where: * step can be hN | qed | N | "" where N is any sequence of alphanumeric characters * hyps is a comma separated list of "" | ? | N where N is a step label * ref is "" | ? | #N | T where N is a step label and T is a theorem label In most places "" and ? are treated the same, but a hyp list [a,b,?] is not always the same as [a,b]; the latter is sometimes interpreted as a theorem which refers only to steps a and b while the former can also refer to other steps. (This is confusing and annoying in practice, so some parts of mmj2 ignore the distinction and always allow other steps.) The abbreviations allow you to leave off some of the colons. Here are the abbreviations I recall: #ref -> ::#ref (!)?step -> (!)?step:: (!)?step:ref -> (!)?step::ref The source of truth is parseStepHypRef(), https://github.com/digama0/mmj2/blob/8f49fb2c93531c5c75fcb65886837c8d0617c033/src/mmj/pa/WorksheetTokenizer.java#L158 On Mon, Apr 25, 2022 at 12:20 PM Thierry Arnoux <[email protected]> wrote: > Hi Glauco, > > I think I found what you're looking for: > > http://mmj2-doc.tirix.org/doc/ProofAssistantGUIDetailedInfo.html > <http://mmj2-doc.tirix.org/doc/ProofAssistantGUIDetailedInfo.html> > > > As far as I'm concerned I only have a difference at the level of the proof > step, and then these components, so I did not have to name that "prefix". > The comments in ProofWorksheet.loadWorksheet > <https://github.com/digama0/mmj2/blob/8f49fb2c93531c5c75fcb65886837c8d0617c033/src/mmj/pa/ProofWorksheet.java#L1025> > contain some information about what is being checked when loading a proof > step, but it is not a definition either. > > It could be useful to have such a definition of what a "Metamath Proof > File" is. My previous Eclipse plugin (which was a shell around MMJ2) used > the same format, *metamath-knife* can output that format, and I'm > starting to use the exact same format in *metamath-vspa*. > > Maybe we could simply write a ".MD" markdown file in set.mm for filling > that purpose? > BR, > _ > Thierry > > > On 25/04/2022 23:47, Glauco wrote: > > Hi Thierry, > > >> - "StepName" would be the name of the step, "72" in your example, >> - "HypSteps" would be the essential hypotheses, "71,70" in your >> example, >> - "RefLabel" would be the label of the theorem applied, like "mpbid", >> - and "formula" is the formula itself (not shown in your example) >> >> > I've come up with names for the single "components" of the blob, and the > formula, but I was looking for a "name" for the whole blob (from the > standpoint of my WHITESPACE based tokenizer, it's the first token of a mmp > statement, when present; then of course another parser breaks this token > down to its components). > > Are you aware of a formal syntax description of .mmp files? > > Thanks again > Glauco > > -- > 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/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%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/4a64ad66-71b6-8087-23b9-4ee607d756de%40gmx.net > <https://groups.google.com/d/msgid/metamath/4a64ad66-71b6-8087-23b9-4ee607d756de%40gmx.net?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/CAFXXJSuXvYV5SPCnXEfrgCTXOUa9CU7pz8M2eYndbiDaGfgFnQ%40mail.gmail.com.
