In this public repository, https://github.com/Lakedaemon/mm0-kotlin-tooling
,
I'll publish soon :
- the antlr parsers I wrote for metamath (battle tested)
- the handwritten parsers I'm writing for metamath zero
- a proof-checker I'm writing for metamath zero
As it is all pure kotlin code, I'll try to provide a multi platform project
that provides for the mm0 proof checker
- a jvm target
- a js target (for node.js/the browser)
- a native target (linux or android)
I'll also publish a summary of my ramblings and understanding of metamath
and metamath zero. So that, more people can understand the benefits of
metamath and mm0
I already published a translation of set.mm (obtained through mm0-hs
written by Mario) in
- a set.mm.mm0 spec
- a set.mm.mmu companion ascii proof file
- a set.mm.mmb companion binary proof file
so that other people don't have to struggle with Haskel stack to build and
compile the mm0 tools to do the translation themselves.
With those files, you can directly delve and use mm0. They are especially
usefull if you have a prior experience with set.mm.
About compression :
mm and mm0 both use back references to shorten proofs, which is a kind of
compression scheme especially usefull because it saves a lot of time,
memory and energy.
I used zip, tar.xz and 7z on the result files to see what compression could
be achieved by archivers and here are the results :
size of
set.mm (2020-02-13):
- uncompressed 37.3MB
- zip 13MB
- tar.xz 10.5MB
+ set.mm0:
- uncompressed 9MB
- zip 921KB
- tar.xz 707KB
+ set.mmu:
- uncompressed 448MB
- zip 22.7MB
- tar.xz 13.4MB
+ set.mmb:
- uncompressed 31.2MB
- zip 12.3MB
- tar.xz 9.6MB
- 7z 9.6MB
Best regards,
Olivier
--
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/61f554d3-72f2-4390-85cc-b0f1d737aa0a%40googlegroups.com.
