kassane / kassane/lean4-zig

Improvement FFI

Open
#7 0 comments 0 reactions 0 assignees View on GitHub
enhancement help wanted
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.