write tactics in another language

Stream: general

[Huỳnh Trần Khanh]

let's say i need to use Algorithm X in my new tactic. Algorithm X can't be implemented efficiently in Lean but it can be implemented efficiently in C. how can i write a tactic in C and use it in Lean? is it even possible? i think it should be because the gptf tactic uses the OpenAI API, which is of course not a Lean feature

[Huỳnh Trần Khanh]

I've watched the metaprogramming video in the Logical Verification course so i think i know the basics

[Jason Rute]

The short answer is that lean tactics have io. So you can run command line stuff and process the results. See https://agentultra.github.io/lean-for-hackers/. Also see other posts by me mentioning “io”.

[Jason Rute]

Since you mentioned it, gptf specifically works by running a curl command via the command line which sends a request to the openai API (over the internet). You can similarly run a local script via the command line or communicate with a locally running process. This io interface is largely undocumented (except through the lean code and random posts here on Zulip). Also, there is now built in support for JSON parsing in lean which makes this communication easier. (But again, no good documentation.)

[Patrick Stevens]

See https://github.com/robertylewis/mathematica for example!

[Patrick Stevens]

(https://robertylewis.com/leanmm/index.html)

[Scott Morrison]

Another answer is: use/wait for Lean 4, and search for "FFI" here on zulip to find discussions about how to connect to external C code.