Improvement FFI
- Dominant language
- Zig
- Stars
- 12
- Forks
- 3
- PR merge metrics
- No merged PRs in 30d
Description
It is intended to extend the interoperability between ziglang and lean4 with primitive and user defined types.
Also add support in C and C++, with zig in the middle.
**Following**:
- [ ] https://github.com/leanprover/lean4/issues/2490
- [x] https://github.com/leanprover/lean4/pull/2497
- [x] https://github.com/leanprover/lean4/issues/2436
**TODO**
- [ ] add more examples
- [ ] add atomic support - [LLVM memory order](https://ziggit.dev/t/what-is-std-atomic-ordering-monotonic/1067)
- [ ] use zig libraries w/ [zig-pkg](https://ziglang.org/download/0.11.0/release-notes.html#Package-Management) on lean4 applications - e.g.: [comath](https://github.com/InKryption/comath), [zalgebra](https://github.com/kooparse/zalgebra),
[zlm](https://github.com/ziglibs/zlm)
- [ ] use lean4 [mathlib4](https://github.com/leanprover-community/mathlib4) on zig applications.
**Note:** I know that many are already tired of seeing this information, but it is worth remembering that the zig toolchain for C++ only static-linking with `llvm-libcxx` + `llvm-libunwind` [builtin] in almost all LLVM targets. In addition to the custom `libcompiler-rt`.
The zffi sample (`build.zig`) even to build Debug and ReleaseSafe (enable `@setRuntimeSafety`) mode in static library requires adding `libcompiler-rt` for another C and C++ compilers.
https://github.com/kassane/lean4-zig/blob/4d4f8bff9970c6ea1ae9c093c7c3318464fd510c/examples/ffi/lib/build.zig#L15-L18
### Reference
- https://github.com/tigerbeetle/tigerbeetle/pull/792
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.