refactor: separate proof/spec files into a dedicated LckSpec lake target

Đang mở

#33 mở ngày 26/2/2026 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó: 4/5
Thời gian dự kiến: 3-5 ngày
Mức phù hợp với người mới: 48/100

Loại issue: Tái cấu trúc
Độ rõ ràng: Khá rõ ràng
Mức độ hoạt động: Đình trệ
Lĩnh vực: build-system, compilers

Hướng nghiên cứu

Kiểm tra định nghĩa target Lake hiện tại và các tệp spec/proof được liệt kê, bao gồm RegexSpec.lean, DesugarSpec.lean và ParserSpec.lean. Xác nhận những tệp nào được đưa vào target Lck chính, sau đó tách chúng thành một target LckSpec được build một cách tường minh, đồng thời giữ mã liên quan đến runtime trong Lck. Hoàn tất khi các bản build downstream của Lck không còn biên dịch hạ tầng proof, trong khi LckSpec vẫn có sẵn cho việc verification hoặc CI.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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

Ngôn ngữ chính: Lean
Star: 2
Fork: 1
Chỉ số merge pull request: Không có pull request nào được merge trong 30 ngày

Hướng dẫn đóng góp

Chưa lập chỉ mục được hướng dẫn đóng góp cho kho mã nguồn này

Bắt đầu từ đâu

Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
Fork repository và làm thay đổi trên một nhánh.
Mở pull request có tham chiếu số hiệu của issue.

Issue khác của lambdaclass/lambda_compiler_kit

refactor: remove unnecessary import of Parser.lean from Semantics.lean Đang mở

Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 72/100

lambdaclass/lambda_compiler_kit#31 · Mở ngày 26/2/2026
nit: fix misleading traversal-order comments in Syntax.lean and Parser.lean Đang mở

Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 68/100

lambdaclass/lambda_compiler_kit#26 · Mở ngày 26/2/2026
bug: CLI readAll stops reading at first empty line instead of reading to EOF Đang mở

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100

lambdaclass/lambda_compiler_kit#22 · Mở ngày 26/2/2026
Enable --wfail axiom-guard gate once warnings are clean Đang mở

enhancement

Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 48/100

lambdaclass/lambda_compiler_kit#38 · Mở ngày 9/6/2026
feat: add --version flag to lck-grep CLI Đang mở

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 50/100

lambdaclass/lambda_compiler_kit#36 · Mở ngày 26/2/2026

Tất cả issue của lambdaclass/lambda_compiler_kit

Issue tương tự

[BUG] @mastra/deployer copies the monorepo root lockfile into .mastra/output, breaking the output install for workspace deps Đang mở

status: needs triage

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100

mastra-ai/mastra#24879 · 1 bình luận · Mở ngày 23/9/2026
import spacy fails with ModuleNotFoundError: No module named 'click' Đang mở

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100

conda-forge/spacy-feedstock#177 · Mở ngày 23/9/2026
[Enhancement] Delete the newer core themes, and only on initial install Đang mở

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100

vigetlabs/wordpress-site-starter#288 · Mở ngày 23/9/2026
New cross-tree layering dependency: jail/ -> proxy/ (build_ca_bundle.py) Đang mở

area:jail bug security severity:low track:open-source

Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 75/100

ntindle/spark-vm#304 · Mở ngày 23/9/2026
Please create a lyrical branch in this repo Đang mở

Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 65/100

micro-ROS/micro_ros_setup#837 · Mở ngày 23/9/2026

Thêm issue về Build System