00:06 <discocaml> <._null._> Just to be sure, Pratt parsing is completely subsumed by menhir, it can just be much more annoying to write in menhir, right ? The only definite advantage I know of Pratt parsing is for variable precedence operators

00:13 <discocaml> <contificate> I don't think it is subsumed by Menhir

00:14 <discocaml> <contificate> Haskell is famously parsed by a LALR(1) parser generator but, as you mention, it has user-defined precedence and requires a tree fixup pass (akin to Pratt's algorithm) in the compiler

00:14 <discocaml> <contificate> so there's variable and also dynamic, in that you could parameterise the parser with different precedences and basically emulate a GLR parser in some contexts

00:15 <discocaml> <contificate> so there's variable and also dynamic, in that you could parameterise the parser with different precedences and basically emulate what a GLR parser may succeed to parse in some fork of the parser in some contexts

00:16 <discocaml> <contificate> ignoring any formal arguments about how powerful LR(1) parsing is, there's no doubt it's tedious, difficult to maintain, difficult to debug, difficult to find people skilled enough to contribute effectively, etc.

00:16 <discocaml> <contificate> and that's not even citing the weak arguments you usually get which concern error recovery and error messages, which Menhir can deal with decently

00:17 <discocaml> <._null._> Disregarding parsing power, I want a tool which prevents me from resolving conflicts unknwoingly

00:17 <discocaml> <contificate> I like Pratt parsing, it's like you're defining a step-wise semantics for the parser, in the fairly obvious way: each left denotation is asking what you do when encountering a token, given some "left" you've already parsed etc.

00:17 <discocaml> <contificate> I think coverage is all you need

00:20 <discocaml> <._null._> Is that testing ? I prefer formal proofs

00:22 <discocaml> <contificate> unfortunate, I find tests cheaper and more plentiful and more viable

00:23 <discocaml> <contificate> would you consider translation validaton as sufficient

00:23 <discocaml> <contificate> that's how compcert works in certain parts, right? its register allocation algorithm itself isn't proved correct, its output is verified to be correct w.r.t the constraints it determines

00:23 <discocaml> <contificate> would you consider translation validation as sufficient

00:24 <discocaml> <._null._> I don't care if the generator is proven correct, only about its output if that's your question

00:25 <discocaml> <._null._> But the generator should be able to take a grammar and some disambiguation hints as inputs and output a sound parser

00:25 <discocaml> <._null._> or fail if the disambiguation hints aren't sufficient

00:25 <discocaml> <contificate> yes, but how many yaks do you want to shave to determine those hints

00:26 <discocaml> <contificate> I appreciate the ideal, but my main gripe is purely with "just use menhir" polling results, with no nuance about what you're using it for, the inherent learning curve of LR parsing, etc.

00:26 <discocaml> <contificate> if you are happy to spend a lot of time and energy and master the fine arts of LR grammar design and disambiguation, great - I feel I got quite close and then just got tired of it

00:27 <discocaml> <._null._> What is "LR grammar design" ? What LR is it ? I would believe it's all about the disambiguation

00:28 <discocaml> <._null._> Then the disambiguation has to be improved, I won't deny it

00:29 <discocaml> <contificate> well, you have to massage grammars to make them compatible with these tools

00:29 <discocaml> <contificate> if you look at basically any grammar online, it's not suitable for generation by any parser generator

00:30 <discocaml> <contificate> like https://people.mpi-sws.org/~rossberg/sml.html this purely for human consumption, as it expresses the important rules, SML grammars for mlyacc have to be structured in various ways to work

00:31 <discocaml> <contificate> the "grammar design" is factoring a naive grammar in your head to use these generators efficiently

00:31 <discocaml> <contificate> which takes a good amount of time and energy to acquire the skillset

00:41 <discocaml> <._null._> I might be completely lost, but if you gave this grammar as is to menhir, it would only complain about shift/reduce and reduce/reduce conflicts right ? And if you somehow explain how to resolve all of these conflicts, you'd get your desired parser ?

00:42 <discocaml> <contificate> yes, but it's not just finding a set of directives that would just work

00:42 <discocaml> <contificate> you'd need to factor it

00:43 <discocaml> <contificate> so you'd transform the grammar in a way that requires a lot of care

00:43 <discocaml> <._null._> Why do you need to change the grammar?

00:43 <discocaml> <contificate> because `expr -> expr expr` is a nonsense

00:43 <discocaml> <._null._> Only if you don't explain the conflicts it creates

00:43 <discocaml> <contificate> you'd get hundreds of errors

00:43 <discocaml> <._null._> resolve*

00:45 <discocaml> <._null._> Already by making it so that this rule is always reduced, you'd solve many conflicts

00:46 <discocaml> <contificate> fixing a grammar is much harder than building it up incrementally and documenting the problems you've skirted over, as people do

00:46 <discocaml> <contificate> like fixing this grammar would be akin to basically boiling it down and building it from scratch

00:48 <discocaml> <._null._> What I want is the tool that tells me how it's broken

00:49 <discocaml> <contificate> with AI, the future may be bright, we could throw deep learning at our vibecoded garbage

00:50 <discocaml> <contificate> tell our customers in the automotive industry that we're sure of its correctness because it routinely passes the "factorial function" test on the nightly test suite

01:05 <discocaml> <tornato> Just vibe code Why3

01:05 <discocaml> <contificate> sorry, I only do things that increase shareholder value

01:08 <discocaml> <cod1r> hmmmm

01:08 <discocaml> <cod1r> HRMMMM