lean-regex: discussion and looking for contributors

Stream: general

[pandaman]

This is the discussion thread for lean-regex, a formally verified regular expression engine in Lean 4.

I'm looking for contributors interested in pushing it forward! Areas for contribution include:

• Feature support: case-insensitive matching, Unicode classes, word boundaries, etc
• Optimization: DFA compilation, KMP-based search, benchmarking, and so on
• Formal verification of these optimizations
• Optimized re! macro to generate an efficient Lean search function from a regular expression
• Ecosystem integration to make it easy to use in parsers, scripts, and other tools, including better error messages

If you are interested in any of these ideas or just curious about regular expressions, please let me know!

[Julian Berman]

First of all congrats! That looks great.

This is extremely petty but given it's the first impression someone gets perhaps you might consider not showing email address matching as your first example in the readme. The world will be a very slightly better place when no one even thinks of using regular expressions to validate email addresses (especially with a pattern there that will fail on my own typically used email addresses.) Happy to send a PR as well of course.

[pandaman]

Thank you for the suggestion! That's an oversight on my part. Fixed in main.

[Krishna Padmasola]

Hi @pandaman I'd like to contribute, it would give me chance to improve my Lean skills. Issue 93 seems like something I could take a shot at.