building bindings to lean

Stream: general

[Miguel Raz Guzmán Macedo]

Is there a C/C++ api bind to call out to Lean? Has anyone built such a project already?

[Uranus Testing]

Lean 4 compiles in C++, so it obviously supports C/C++ bindings.

[Miguel Raz Guzmán Macedo]

Does Lean 4 have documented bindings yet?

[Miguel Raz Guzmán Macedo]

Ah, found some python bindings to lean. https://github.com/dselsam/lean-python-bindings/blob/master/lean/lang/expr.py

[Uranus Testing]

I have not seen such documentation, because Lean 4 is still in development, but you can look at mixed C++/Lean project here: https://github.com/o89/n2o

[Uranus Testing]

There are useful headers in https://github.com/leanprover/lean4/tree/master/src/runtime (for example, https://github.com/leanprover/lean4/blob/master/src/runtime/object.h), these headers can be used as some kind of documentation.

[Uranus Testing]

In addition, you can look at the code generated by Lean 4: LEAN_PATH=/path/to/lean4/src/Init:Test=. /path/to/lean4/bin/lean -c hello.cpp hello.lean.

[Patrick Massot]

@Uranus Testing what are this n2o thing and other projects in o89? What are you trying to achieve here?

[Uranus Testing]

@Patrick Massot

what are this n2o thing and other projects in o89?

N2O is application server, as described, which can be used to construct, for example, web applications (with NITRO).

What are you trying to achieve here?

I brought it just as an example of mixed C++/Lean application, because I do not know any other.

[Patrick Massot]

Did you use it for anything, or intend to use it for anything, or is it only the beginning of a proof of concept?

[Uranus Testing]

Did you use it for anything

Currently no, but this applies only to Lean 4 implementation (if interested, here is information about other implementations: https://n2o.tech/, or you can ask @Namdak Tonpa).

[Patrick Massot]

Thanks. It's still hard for me to understand what it's about, but I guess it means I don't need it.

[Namdak Tonpa]

Patrick Massot said:

Thanks. It's still hard for me to understand what it's about, but I guess it means I don't need it.

You can think of this as an analogue to coq.io in Coq world. This is practical web framework/stack which is port of Nitrogen Web Framework, famous in ERP, CRM and banking industry. We are trying to bring pure dep-types development to industry (Agda /w MAlonzo, Coq /w coq.io, Lean4 /w https://lean4.dev). The full info about N2O stack is here https://n2o.dev, you can find there 7 years history with books, manuals, etc.