I watched though the video and spotted a few things not mentioned in Wolf's notes.
At around 1:02 (1 hour 2 minutes), he starts writing a grammar file based on the EBNF in the Metamath book. The book uses dashes inside symbols on the left hand side of each rule, which is apparently not shared by all EBNF standards, so he has to replace them by underscores. GNU bison supports dashes (but calls it a GNU extension, incompatible with POSIX Yacc), Happy parser verifier (for Haskell) also doesn't allow dashes in symbol names. Maybe it is worthwhile replacing dashes by underscores in the Metamath book EBNF? It may save someone time, in case if they would like to simply copy the grammar file from the book. At 5:02, he tries mmj2. Apparently there's some sort of trouble launching it on the MacOS (he had to modify the starting script), so maybe that bug should be fixed. My impression is that most of his complaints come from missing proof-assisting capabilities of the metamath program and mmj2, but main points stand of course. Our tooling is scarce and most of work is done manually anyway. On the other hand, the video has quite a lot of praise for the Metamath book and the design of the language itself (stressing its simplicity), so Metamath clearly has its strong points in comparison with other proof systems. -- 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/b2f84723-5ae7-4889-9403-176463bb5fb6%40googlegroups.com.
