digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
312 stars 40 forks source link

mm0-rs as a library #34

Open digama0 opened 4 years ago

digama0 commented 4 years ago

This is a tracking issue for mm0-rs as a library:

The details of the API are TBD, but might include REPL-like usage where you give MM1 commands and get them elaborated, and a query API for the Environment object.

c-cube commented 4 years ago

regarding python in particular, pyo3 should be much easier than going throught hand made C bindings.

digama0 commented 4 years ago

I see. The plan was not to make any particular reference to python in mm0-rs, but rather have some generic bindings that can be used in whatever setting. I guess the easiest way to do python bindings specifically would be to use mm0-rs as a pure rust library, and have the main application be a python shim using pyo3 which links with mm0-rs.

c-cube commented 4 years ago

Yes, you can make a separate crate that uses pyo3 and generates a .so file (or .dynlib I guess) that is also a native python module. I wouldn't dare suggest to add python directly into mm0-rs :grin: