Post #2479114

2026-05-09 06:46 UTC

@olynch@mathstodon.xyz What if you had *two* parsers? * One damn fast, prone to formal verification, following known theory, that is bad at error recovery. * The other ad hoc and slower that is better at error recovery and giving useful information about errors, triggered when the first one reports a failure. In a large codebase, the first one would be used most of the time. The second one would be applicable only at the file you are currently developing or modifying.

Replies (2)

@olynch@mathstodon.xyz 2026-05-09 07:51

@MartinEscardo@mathstodon.xyz A couple things. 1. I'd need concrete performance data that my handwritten parser was a performance bottleneck in the overall compilation pipeline before I would ever take on the maintenance burden of keeping two implementations in sync. 2. I would design the grammar in the first place for predictable and understandable errors, which concretely means: LL(1) with respect to whatever my tokenizer is doing. In this situation, I would expect that a parser generator wouldn't be that much faster than handwritten recursive descent, and quite possibly slower. 3. There are techniques in recursive descent like Pratt parsing which handle infix precedence or even fancier stuff like custom mixfix operators which are annoying to encode into a traditional BNF grammar; you can write an ambiguous grammar and then add precedences, but it's not so clear when you've done this that it's still LL(1), and I'd rather not bother. 4. I would expect that bigger performance gains would be around cache usage. E.g., use a sum of struct of arrays for your AST with 32 bit IDs instead of pointers, put token tags into single bytes in a byte array and store the associated spans elsewhere, use SIMD instructions in lexing, etc. These are the kind of things that production compilers do in order to really optimize performance. Again, I don't really care about performance for my parsers right now because it's not a bottleneck, but this is what I would do if I did care.

Open ##2479115
@soaproot@sfba.social 2026-05-09 16:30

@MartinEscardo@mathstodon.xyz I'm not sure there is anything about error reporting and/or recovery which inherently makes an implementation slow, but for what it is worth I typically use two implementations of the metamath proof verifier. One is fast, and the other gives better error messages (particularly in one commonly encountered situation). As far as I know this is an accident of history and the error messages I'm looking for may eventually get added to the fast verifier. @olynch@mathstodon.xyz

Open ##2479118