Conversation
arthurpaulino
left a comment
arthurpaulino
left a comment
There was a problem hiding this comment.
There are non-trivial trade-offs at stake on this PR.
The ergonomic Rust types that mimic the memory layout of Lean objects are gone. But at least we don't need to keep the synchronization by hand, which is more principled.
The layer that abstracts unsafe operations is gone. Maybe we can redefine it in terms of this new API later.
Also, docs/ffi.md needs to be completely rewritten. Or deleted, if we no longer bother explaining our FFI infrastructure since it's now a straightforward Lean -> Rust dependency.
arthurpaulino
left a comment
arthurpaulino
left a comment
There was a problem hiding this comment.
This patch is superb! Truly amazing work 🎉
I've left my last batch of comments. Also, docs/ffi.md needs to be either rewritten or deleted.
| commitment_parameters: LeanObject, | ||
| ) -> LeanExternal<AiurSystem> { | ||
| let system = AiurSystem::build( | ||
| lean_ptr_to_toplevel(toplevel), |
There was a problem hiding this comment.
I think we can change the convention from lean_ptr_to_* to decode_*. I don't have strong feelings about it though, just a mild preference.
| lean_ptr_to_toplevel(toplevel), | |
| decode_toplevel(toplevel), |
| proof_obj: LeanExternal<Proof>, | ||
| ) -> LeanExcept { | ||
| let fri_parameters = lean_ctor_to_fri_parameters(fri_parameters); | ||
| let claim = claim.as_array().map(lean_unbox_g); |
There was a problem hiding this comment.
Throughout the PR, sometimes you receive a LeanObject and convert it with, e.g., .to_array() and sometimes you receive the right object type already in the type signature of the function. Maybe it's worth picking one standard and following it.
| let arr = exprs_obj; | ||
| let exprs: Vec<Arc<IxonExpr>> = arr.map(lean_ptr_to_ixon_expr); |
There was a problem hiding this comment.
| let arr = exprs_obj; | |
| let exprs: Vec<Arc<IxonExpr>> = arr.map(lean_ptr_to_ixon_expr); | |
| let exprs: Vec<Arc<IxonExpr>> = exprs_obj.map(lean_ptr_to_ixon_expr); |
| /// Debug-asserts the tag is in range. | ||
| #[inline] | ||
| pub fn as_ctor(self) -> LeanCtor { | ||
| debug_assert!(!self.is_scalar() && self.tag() <= 243); |
There was a problem hiding this comment.
Please extract these values to constants, with a commentary mentioning that these values are extracted from lean.h
| )*}; | ||
| } | ||
|
|
||
| lean_domain_type! { |
There was a problem hiding this comment.
Defining the macro on this file, as above, is fine. But I don't think this is a good place to use it with Ix-specific types.
I'm already considering factoring out the FFI code to its own subcrate. We don't want to mix up what's general to Lean FFI with what's particular to the Ix code base.
2 participants
No description provided.