Calling external process in a tactic

Stream: general

[Jason Rute]

I'm working on a (sort of ambitious) project in Lean. One thing I'm doing is making tactics which can call external Python scripts (using Lean's io capabilities). For now they are mostly toy examples, but I'll eventually call trained machine learning algorithms. I'm just curious if there are any other projects which have done this sort of interface? I think the Lean-Mathematica interface of @Minchao Wu and @Rob Lewis used the Lean server to call Lean from within Mathematica (and there are a few projects which call Lean from within Python with the Lean server). The LeanHammer project of @Gabriel Ebner uses custom C++ code if I recall. (I think I know what I'm doing, but it would be good to see prior art.)

[Scott Morrison]

@Keeley Hoek's experimental version of rewrite_search called a classifier written in C++. If I remember correctly, an initial version used io to call an external process, and subsequently he just forked Lean and inlined the C++ he needed.

[Rob Lewis]

The Mathematica link goes both ways. From Mathematica, you can interact with a Lean server. And from Lean, you can query Mathematica. The latter direction does exactly what you're proposing. We wrote a small Mathematica server in Mathematica (so that we didn't relaunch it for every query), and using the io monad in Lean, we called a Python script that interacted with this server.

[Rob Lewis]

The Python layer is very small, just a handful of lines, but it was easier than doing the server interface directly from Lean...

[Jason Rute]

Ok great. I just found your code: https://github.com/robertylewis/mathematica

I got confused since the other direction of the interface is stored in a separate repo: https://github.com/minchaowu/mm-lean

[Jason Rute]

Another way to communicate with Lean is by hacking the C++ code. Since I don't know C++, I don't think about these sort of things. I think the Python Lean Bindings are an example of this. However, I also think the bindings may not work any more (Does anyone know?) which is a danger of such approaches. Other projects, like the Lean hammer and @Keeley Hoek's experimental version of rewrite_search (where is the code?) also write custom C++ code to interact with Lean.