Compile time regexes!

Stream: general

[Alfredo Moreira-Rosa]

Link To Playground

I didn't know that there was a great formal regex library out there, and i was toying around with elaborators and i was thinking, it would be great to have compile time regexes.

So above you have a one single file project for this idea.
No formal proofs here, since lean-regex library does already a great job at that.

I just wanted to share for others developpers that are intrigued about elaborator in Lean and how it compare to Rust.
And i have to say, Lean 4 for a system programming language have some good qualities and i think if the ecosystem evolves (with better support for networking, https (not just http), concurrency, parrelism, effects (like ZIO), it has a bright future.
The proof system can be used not just to formally proove your whole program, you can also use it as a compile time contract engine. pre-conditions, invariants, post-condition, and all that at compile time.
Really love it.

[pandaman]

Hey I'm the author of lean-regex! I'm thrilled to see the post and like-minded peers!

The regex elaborator is definitely interesting. My library also has one, but also I've been pondering the possibility of compiling regexes into specialized Lean functions (rather than the general search routines) using the elaborators (I hae an issue). I'd love to connect and discuss how we might combine our efforts :grinning_face_with_smiling_eyes:

[Alfredo Moreira-Rosa]

Hello,
Did you do some benchmarks against other state of the art compile time regex (i think, rust and cpp that have those), just to check that having generated code vs runtime state machine is worth compared to what you have already ?
If not, maybe it's a first step ?

[François G. Dorais]

See also https://github.com/fgdorais/lean4-parser/tree/main/Parser/RegEx part of my more general parser library. There is also this WIP student-led project: https://github.com/fgdorais/lean4-automata