Calling out to libraries?

Stream: lean4

[Tanner Swett]

Is it (yet) common for authors of Lean 4 applications to use libraries that aren't specifically designed for Lean? If so, how is it usually done? It looks like you can do it using the FFI without terrible trouble; just write a C wrapper around the library that makes it use simple types, then write a Lean wrapper around the C wrapper that provides a nice Lean-friendly interface.

Another option, of course, is to just use stdin and stdout to communicate with something.

[Henrik Böving]

Well...if FFI is possible there isnt really a reason to not use FFI (apart from being lazy)

[Tanner Swett]

Yup. I guess I was hoping there was some magical alternative option.

"Oh, you haven't heard of LeaPyn, the Lean library that lets you import Python libraries?" :grinning_face_with_smiling_eyes:

[Henrik Böving]

I mean you can FFI with cpython to call python libraries if you want

[Mac Malone]

Tanner Swett said:

Yup. I guess I was hoping there was some magical alternative option.

"Oh, you haven't heard of LeaPyn, the Lean library that lets you import Python libraries?" :grinning_face_with_smiling_eyes:

This is kind of what my library Alloy tries to do for C (apologies for the shameless self-plug). A similar approach for Python would be quite cool.

[Siddhartha Gadgil]

Does alloy let one (easily) use a C library? For example C API of tensorflow?

[Mac Malone]

@Siddhartha Gadgil It should be relatively easy. You just do the normal extern_lib/moreLinkArgs linking configuration as for any Lean FFI and then alloy c include the relevant C headers (as e.g. the S example does for std headers).

[Mac Malone]

@Siddhartha Gadgil One missing feature is that you cannot currently customize the server include path, so the server features (e.g., autocomplete, go-to def, hover) will not be available for the C library at the moment (if the library is not part of the system include path). However, you can still customize the build include path via the usual moreLeancArgs).

[Mac Malone]

@Siddhartha Gadgil Also, if you decide to give Alloy a shot for some project, I would greatly appreciate it if you would report any bugs / missing features you encounter. I would love to make alloy the best it could be!

[Siddhartha Gadgil]

Sure