chore: move constructor invocations to Lean - #18
Conversation
73e2ae1 to
6986723
Compare
Lean PR #13679 will reduce the guarantees provided by the compiler for constructor representation, allowing more freedom. This means that C code will need to invoke/destructure constructors via externed Lean declarations instead. This PR implements the required changes. There shouldn't be any backwards compatibility issues with this. To ensure that the changes work, this PR also adds recent releases to CI, inluding a Windows build. Because Windows builds revealed important differences in the linker, the PR also restructures the Lakefile to build one big shared library with the C and Lean parts together, rather than separate shared libraries that are loaded at the same time. This is because Windows resolves symbols in a DLL at link time, rather than at load time. Additionally, missing initializers were added to the FFI wrapper, fixing an intermittent bug.
6986723 to
108c869
Compare
acmepjz
left a comment
acmepjz
left a comment
There was a problem hiding this comment.
Thank you!
Is this final version and is ready for deploy?
| @[export lean_md4c_some_document] def someDocument (d : Document) : Option Document := some d | ||
| @[export lean_md4c_some_string] def someString (s : String) : Option String := some s |
There was a problem hiding this comment.
Do you think it's possible to export Option.some (type polymorphic version)? Or these two has different ABIs?
There was a problem hiding this comment.
They should be the same. Would you prefer a polymorphic version?
There was a problem hiding this comment.
Would you prefer a polymorphic version?
Yes, sure.
There was a problem hiding this comment.
I was wrong - the exported polymorphic version include a slot for the type argument, which is not pleasant C code.
There was a problem hiding this comment.
I was wrong - the exported polymorphic version include a slot for the type argument, which is not pleasant C code.
OK that's new to me. I originally thought that type argument does not appear in the compiled C code.
Co-authored-by: Jz Pan <acme_pjz@hotmail.com>
|
Once you're happy with this code, I see no reason not to squash-merge it. Or I can squash the PR branch myself, if you'd like. |
I see. I can do the squash-merge by myself. |
|
OK then, I think it's ready to go. Thanks! |
|
Thanks! |
2 participants
Lean PR #13679 will reduce the guarantees provided by the compiler for constructor representation, allowing more freedom. This means that C code will need to invoke/destructure constructors via externed Lean declarations instead.
This PR implements the required changes. There shouldn't be any backwards compatibility issues with this.
To ensure that the changes work, this PR also adds recent releases to CI, inluding a Windows and a Mac build. Because Windows builds revealed important differences in the linker, the PR also restructures the Lakefile to build one big shared library with the C and Lean parts together, rather than separate shared libraries that are loaded at the same time. This is because Windows resolves symbols in a DLL at link time, rather than at load time. Additionally, missing initializers were added to the FFI wrapper, fixing an intermittent bug.