On Sun, 22 Dec 2019 05:26:30 -0800 (PST), savask <[email protected]> wrote: > 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.
I don't think switching dashes would help. Like all language specs, the EBNF is high-level. An implementation should make a number of changes to implement it efficiently. For example, you need to rewrite them to avoid left/right recursion as necessary for LL or LALR parsers. By that point, switching the labels is trivial. We could separately post a GNU bison implementation. If someone wants to start with GNU bison, that'd be a far better help. Of course, it's so trivial to parse Metamath files that I'm not sure it'd help much. Does anyone think that'd be worth the trouble to create? > 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. I don't have a Mac, so I can't reproduce that. Can someone with a Mac help us reproduce & then help us fix that? > 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. I agree. There's nothing fundamental about Metamath that prevents the implementation of higher-level & more powerful tactics, but Metamath currently doesn't have that. I'd love to see those additions. > 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. Sounds sensible. --- David A. Wheeler -- 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/E1inX4b-0004Rm-U9%40rmmprod07.runbox.
