Integrate Glushkov NFA engine into lck-grep CLI utility
还没有人认领这个 Issue。
评估
调研方向
从 cli/Lck.Grep.lean、Lck/Regex.lean 以及 Lck/Regex/Glushkov/ 下的 Glushkov 引擎开始。公开 Glushkov.build，替换 Thompson NFA 调用，并运行 test/ 中现有的示例或测试，以比较 grep 的行为。当 CLI 使用经过验证的引擎，并且形式化验证的性质已记录在案时，即视为完成。
由索引模型根据 Issue 内容生成。
描述
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/)
- 主要语言
- Lean
- 星标
- 2
- 派生
- 1
- PR 合并指标
- 30 天内没有已合并 PR
环境准备
我们还没有检查这个项目的环境配置文件。先看它的 README，通用步骤见我们的新手贡献指南。
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
lambdaclass/lambda_compiler_kit 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 72/100
-
难度 1/5 1 小时以内 新手友好度 68/100
-
难度 2/5 1-3 小时 新手友好度 68/100
-
enhancement
难度 4/5 3-5 天 新手友好度 48/100
-
难度 2/5 1-3 小时 新手友好度 50/100
查看 lambdaclass/lambda_compiler_kit 的全部 Issue
相似的 Issue
-
`sysknife history --help` says --since takes ISO-8601, and the parser refuses offsets and bare dates未关闭bug easy good first issue help wanted
难度 1/5 1-3 小时 新手友好度 94/100
lacs-project/sysknife#519 ·
维护者通常 1 天内回复
-
enhancement
难度 1/5 1 小时以内 新手友好度 72/100
-
area:breg bug criticality:p3 triage:needs-implementation
难度 2/5 1-3 小时 新手友好度 78/100
registrystack/registry-stack#1699 ·
维护者通常 1 天内回复
-
bug
难度 2/5 1-3 小时 新手友好度 88/100
-
难度 2/5 1-3 小时 新手友好度 87/100
juejin-cn/juejin-usage#214 ·
维护者通常 1 天内回复