Feature/vm dynload #49
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This module will allow the vm to dynamically link shared objects at run time so that Lean can call external code written in C/C++. Fixes: leanprover-community/lean #24
Following some conventions established in (#20) I added some constructor functions to allocate the `vm_foreign_obj` struct in the VM.
As I'm learning about the VM architecture in Lean I'm adding notes to help future contributors.
We add libffi to our build dependencies
Add initial documentation on the VM FFI
WIP
We register a declaration attribute to bind foreign functions to Lean
constants like so:
@[ffi `libfoo]
constant foo_fun : c_int -> c_int -> c_int
Allowing the vm to get a handle to the foreign function from `dlsym`
and map it with a `ffi_cif` struct from `ffi.h`. This will allow Lean
users to then create functions using this type to marshal Lean values
into the bound `ffi_cif` and make the call with `libffi` under the
hood.
Fix relative paths to work on linux
Normalize the file path handed to `load_foreign_object`
…lean into upstream/vm-dynload
cipher1024
force-pushed
the
master
branch
2 times, most recently
from
08a832d
to
217862b
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Pull Request Description
Ensure you have read the contribution guide before filling in a description of the
pull request, regardless of whether it is complete or a work in progress.
All Pull Requests should include test case(s) which demonstrates the intended
behavior of a feature, or a regression test demonstrating that the fix resolves
the issue.