Pin Aeneus in `lakefile.lean` in SymCRust
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 1/5
- Thời gian dự kiến
- Dưới một giờ
- Mức phù hợp với người mới
- 85/100
- Loại issue
- Tái cấu trúc
- Độ rõ ràng
- Đặc tả rõ ràng
- Mức độ hoạt động
- Ít trao đổi
- Công nghệ
- git
- Lĩnh vực
- build-system
Hướng nghiên cứu
Thiết lập dependency nằm trong SymCRust/lean/lakefile.lean tại dòng được liên kết; hãy bắt đầu từ đó và so sánh cách sắp xếp các thư mục cùng cấp với yêu cầu Aeneas git tường minh được nêu trong issue. Sử dụng commit d71d2e3f và đường dẫn backends/lean, sau đó xác minh rằng dự án Lean resolve Aeneas từ khai báo.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
Currently, aeneas is expected to be in a sibling directory and pinned to d71d2e3f.
However, aeneas can be explicitly pinned in the lakefile.lean by doing
require aeneas from git
"https://github.com/AeneasVerif/aeneas" @ "d71d2e3f2cb763f7faf15ab606ac9cf32da8dead" / "backends/lean"
Disclosure: I am interested in using this repository to mine Lean4 proving challenges for evaluating and training LLMs, which I would like to publish to HuggingFace as open source. This change will make running these evaluations a little more turnkey.
- Ngôn ngữ chính
- C
- Star
- 890
- Fork
- 91
- 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 microsoft/SymCrypt
-
bug compiler-support
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 42/100
-
enhancement
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100
-
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100
-
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100
-
enhancement
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 20/100
Tất cả issue của microsoft/SymCrypt
Issue tương tự
-
task
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100
vsanthanam/JBird#429 ·
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100
-
bug documentation
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
es-ude/OnDeviceTraining#459 ·
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 65/100
bilelmoussaoui/gobject-linter#199 · 1 bình luận ·
-
bug
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
bradcypert/plum#53 ·