refactor: separate proof/spec files into a dedicated LckSpec lake target
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 48/100
- issue の種類
- リファクタリング
- 明瞭さ
- おおむね明確
- 活発さ
- 停滞
調査の方向性
現在の Lake ターゲット定義と、一覧にある spec/proof ファイル（RegexSpec.lean、DesugarSpec.lean、ParserSpec.lean を含む）を調査します。どのファイルがメインの Lck ターゲットに取り込まれているかを確認し、それらを明示的にビルドされる LckSpec ターゲットに分離します。その際、ランタイムに関係するコードは Lck に残します。Lck の下流ビルドで proof インフラストラクチャがコンパイルされなくなり、LckSpec が引き続き検証または CI に利用できれば完了です。
索引モデルが issue の本文から書いたものです。
説明
Problem
Spec and proof files (RegexSpec.lean, DesugarSpec.lean, ParserSpec.lean, etc.) are included in the main Lck library target. This means every downstream user of the library also compiles the proof infrastructure, which is heavyweight (imports Mathlib, long compile times).
Expected fix
Move spec/proof files into a separate LckSpec Lake target (or library) that is only built when explicitly requested (e.g., for verification or CI). The main Lck target should contain only the runtime-relevant code.
References
- Suggested by AI code review on PR #9
- 主要言語
- 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
freedomofpress/dangerzone#1562 ·
-
Mend: dependency security vulnerability status: needs triage 🕵️♀️
難易度 2/5 1〜3時間 初心者へのやさしさ 70/100
carbon-design-system/ibm-products#9907 ·
-
intake mcp-intake needs-ac needs-human-review priority:medium type:feature
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
Ikalus1988/MisakaNet#2102 · コメント 2 件 ·
-
onnx-ir re-exports ModelProto and GraphProto but not NodeProto, AttributeProto and AttributeType オープン
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 65/100
llvm/lighthouse#283 ·