Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding lean support #862

Open
DanielFabian opened this issue Jul 31, 2023 · 1 comment
Open

Adding lean support #862

DanielFabian opened this issue Jul 31, 2023 · 1 comment

Comments

@DanielFabian
Copy link

I'm interested in interop for the lean theorem prover. Rust would be a great candidate for that since lean's memory model is not extremely far from rust's with borrowing, no gc, etc.

Having access to rust libraries would enrich the lean eco system quite a lot and make it a lot easier to use outside of pure theorem proving.

From a quick glance at the code it looks like you already have 3 language backends; C, C++ and CPython.

Would you be potentially willing to accept upstreaming a lean backend, or would I have to work entirely on a fork because you have absolutely no interest.

@jschwe
Copy link
Contributor

jschwe commented Sep 4, 2023

Please note that I'm not a Maintainer, but realistically speaking I think you would have to do this on a fork. cbindgen currently is only passively maintained by one maintainer with a very limited review bandwidth. On the flipside, there is not too much activity in the repository, so it shouldn't be too much effort keeping your fork up to date.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants