Integrate Glushkov NFA engine into lck-grep CLI utility
まだ誰も着手していません。
評価
調査の方向性
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 はありません
コントリビューションガイド
このリポジトリのコントリビューションガイドは索引されていません
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- 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
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
nightscout/nocturne#1424 ·
-
難易度 2/5 1〜3時間 初心者へのやさしさ 65/100
paritytech/zombienet-sdk#591 ·
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
mruangutai/harness#1897 ·
-
os:linux
難易度 2/5 1〜3時間 初心者へのやさしさ 70/100
mpv-player/mpv#18510 · コメント 2 件 ·