refactor: separate proof/spec files into a dedicated LckSpec lake target
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 48/100
- Issue type
- Refactor
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- build-system, compilers
Research direction
Inspect the current Lake target definition and the listed spec/proof files, including RegexSpec.lean, DesugarSpec.lean, and ParserSpec.lean. Confirm which files are pulled into the main Lck target, then separate them into an explicitly built LckSpec target while keeping runtime-relevant code in Lck. Done means downstream builds of Lck no longer compile the proof infrastructure, while LckSpec remains available for verification or CI.
Written by the indexing model from the issue text.
Description
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
- 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
freedomofpress/dangerzone#1562 ·
-
Mend: dependency security vulnerability status: needs triage 🕵️♀️
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
carbon-design-system/ibm-products#9907 ·
-
intake mcp-intake needs-ac needs-human-review priority:medium type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
Ikalus1988/MisakaNet#2102 · 2 comments ·
-
onnx-ir re-exports ModelProto and GraphProto but not NodeProto, AttributeProto and AttributeType Open
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
llvm/lighthouse#283 ·