| 08:36 | <Olivier Flückiger> | Afaik it's just that nobody put the time in to polish the experimental regexp engine to the point where it could be shipped. The existing one has decades of performance optimizations, heuristics, and so on. I share the sentiment that the properties Barriere etal worked out should be preserved to keep the door open for a future implementation leveraging these properties. |
| 18:15 | <bakkot> | assuming no backreferences, surely? |
| 18:16 | <bakkot> | I agree that it would be good to preserve linearity as much as possible but it's already gone if we include backreferences so it would not be that bad to have other features which also lose linearity |
| 18:18 | <Michael Ficarra> | @bakkot including backreferences |
| 18:18 | <Michael Ficarra> | there's no caveats, they've mechanised the full ES2023 regexp section |
| 18:19 | <bakkot> | ... I was pretty sure regexes with backreferences were NP |
| 18:23 | <bakkot> | they've mechanised the whole thing, but it's only linear if there's no backreferences |
| 18:28 | <Michael Ficarra> | my understanding was they proved equivalence between their linear implementation and the mechanised regexp section |
| 18:28 | <Michael Ficarra> | I'll see if I can find more info in the paper |
| 18:49 | <Michael Ficarra> | found it: you're right, it's only for patterns with no backreferences |