Pin Aeneus in `lakefile.lean` in SymCRust
还没有人认领这个 Issue。
评估
- 难度
- 1/5
- 预计耗时
- 1 小时以内
- 新手友好度
- 85/100
- Issue 类型
- 重构
- 描述清晰度
- 描述清楚
- 活跃度
- 冷清
- 技术栈
- git
- 领域
- build-system
调研方向
依赖设置位于链接行中的 SymCRust/lean/lakefile.lean；从那里开始，将兄弟目录的布局与 issue 中显示的显式 Aeneas git 要求进行比较。使用 commit d71d2e3f 和路径 backends/lean，然后验证 Lean 项目是否根据声明解析 Aeneas。
由索引模型根据 Issue 内容生成。
描述
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.
- 主要语言
- C
- 星标
- 893
- 派生
- 90
- PR 合并指标
- 30 天内没有已合并 PR
环境准备
- 没有 Dockerfile 或 Docker Compose 文件
- 有 Pull Request 模板
- 没有贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
microsoft/SymCrypt 的其他 Issue
-
难度 4/5 3-5 天 新手友好度 55/100
-
bug compiler-support
难度 4/5 3-5 天 新手友好度 42/100
-
enhancement
难度 5/5 一周以上 新手友好度 25/100
-
难度 5/5 一周以上 新手友好度 25/100
-
难度 5/5 一周以上 新手友好度 25/100
查看 microsoft/SymCrypt 的全部 Issue
相似的 Issue
-
systemd-binfmt exits 1 when the binfmt_misc flush fails, even though all rules register successfully可能已有人在做 @turbcool 今天认领。 未关闭binfmt
难度 2/5 1-3 小时 新手友好度 80/100
维护者通常 1 天内回复
-
follow: logical decoding messages (wal2json "M") stop apply; on main follow then reports endpos reached with changes missing可能已有人在做 @vgul 今天认领。 未关闭
难度 2/5 1-3 小时 新手友好度 78/100
-
bug
难度 2/5 1-3 小时 新手友好度 76/100
维护者通常 2 天内回复
-
难度 2/5 1-3 小时 新手友好度 72/100
libsdl-org/SDL#16444 ·
维护者通常 1 天内回复
-
bug Component component: net
难度 1/5 1 小时以内 新手友好度 90/100
RT-Thread/rt-thread#11852 · 1 条评论 ·
维护者通常 1 天内回复