Integrate Glushkov NFA engine into lck-grep CLI utility
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 38/100
Research direction
Start with cli/Lck.Grep.lean, Lck/Regex.lean, and the Glushkov engine under Lck/Regex/Glushkov/. Expose Glushkov.build, replace the Thompson NFA calls, and run the existing examples or tests in test/ to compare grep behavior. Done means the CLI uses the verified engine and the formally verified properties are documented.
Written by the indexing model from the issue text.
Description
Summary
The cli/Lck.Grep.lean CLI utility currently has a hardcoded Thompson NFA implementation for proof-of-concept. We now have a verified Glushkov NFA engine with formal correctness proofs.
Goal
Replace the Thompson PoC with the verified Glushkov engine:
- Use
Glushkov.buildto compile regexes to NFAs - Verify that the Glushkov engine produces equivalent results
- Validate against existing test cases in
cli/
Implementation steps
- Expose
Glushkov.buildinLck/Regex.lean - Replace Thompson NFA calls with
Glushkov.build - Run existing grep tests to confirm behavior equivalence
- Document which properties are now formally verified
Related
- Glushkov NFA file:
Lck/Regex/Glushkov/ - CLI entry point:
cli/Lck.Grep.lean - Test suite: (existing example usage in
test/)
- Dominant language
- Lean
- Stars
- 2
- Forks
- 1
- PR merge metrics
- No merged PRs in 30d
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from lambdaclass/lambda_compiler_kit
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
-
Difficulty 1/5 Under an hour Newbie friendliness 68/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
enhancement
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 50/100
All issues in lambdaclass/lambda_compiler_kit
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
nightscout/nocturne#1424 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
paritytech/zombienet-sdk#591 ·
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
mruangutai/harness#1897 ·
-
os:linux
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
mpv-player/mpv#18510 · 2 comments ·