Metamath Zero specification status?

[Cris Perdue]

In the mailing list archives I see mentions of a specification for MM0 / Metamath Zero. I am interested in catching up with the definition of it at some point, but I'm not sure what to look at, nor whether it might be better to wait a bit.

There is a document from February on GitHub at https://github.com/digama0/mm0/blob/master/docs/index.html.

Would that be the thing to read?  Might it be better to wait for some near-term developments in it, or just go ahead?  Or will there be something else in the near future?

Thanks,

Cris

[Mario Carneiro]

Hi Cris,

I'm happy to hear you are interested. MM0 is currently under active development so lots of things are in flux, but the best resources for MM0 are currently the specification https://github.com/digama0/mm0/blob/master/mm0.md and other files in the https://github.com/digama0/mm0/ repo, and the MM0 thread on this list (https://groups.google.com/forum/#!topic/metamath/raGj9fO6U2I). The mailing list thread has some high level description of the progress. The mm0.md spec is a specification of the .mm0 file format, which is sufficient for being able to read the examples in the examples/ directory. The proofs are not contained in the mm0 files, but all the information needed to understand the statement of the target theorem(s) are.

The main verifier if you want to play with this yourself is the mm0-hs verifier in Haskell. There is another spec in https://github.com/digama0/mm0/blob/master/mm0-hs/README.md that gives the implementation-defined aspects of MM0 specific to the haskell verifier. In particular, the .mmu proof format is described there, so you can also use that to read .mmu files in the examples/ directory.

I'm documenting on the fly, so if you have any suggestions of areas I should focus on to make anything clearer please let me know.

Mario Carneiro

--
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/CAOoe%3DWJ0iLg40N30j0D%2B_XBcq-Lm5EQ7iHjE-VyMkCyEWjHpfg%40mail.gmail.com.