argumentcomputer / argumentcomputer/RustFFI.lean
Are the integers really signed or unsigned?
未关闭
- 主要语言
- Lean
- 星标
- 17
- 派生
- 2
- PR 合并指标
- 30 天内没有已合并 PR
描述
Rust code defines the parameters to be signed `i32`:
https://github.com/lurk-lab/RustFFI.lean/blob/af3a8f68d1657d4db9cac43e9bbba0bec1aaf1ad/src/lib.rs#L2
But Lean defines them to be unsigned `UInt32`:
https://github.com/lurk-lab/RustFFI.lean/blob/af3a8f68d1657d4db9cac43e9bbba0bec1aaf1ad/Main.lean#L2
How does that even work 🤯
贡献指南
这个仓库没有索引到贡献指南
调研方向
比较 src/lib.rs 第 2 行和 Main.lean 第 2 行中的参数定义,然后跟踪 Rust FFI 边界如何表示和传递这些值。确定有符号性不匹配是有意为之还是一个 bug;当该 issue 有了文档化的解决方案,并且在需要更改时定义保持一致,即视为完成。
由索引模型根据 Issue 内容生成。
评估
- 技术栈
- rust
- 领域
- compilers
- Issue 类型
- 缺陷
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 活跃度
- 停滞
- 描述清晰度
- 需要澄清
- 新手友好度
- 30/100