Zulip Chat Archive

Stream: general

Topic: write tactics in another language


Huỳnh Trần Khanh (Oct 30 2021 at 16:11):

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 (Oct 30 2021 at 16:12):

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

Jason Rute (Oct 30 2021 at 16:51):

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 (Oct 30 2021 at 17:30):

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 (Oct 30 2021 at 19:35):

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

Patrick Stevens (Oct 30 2021 at 19:35):

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

Scott Morrison (Oct 30 2021 at 23:55):

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.


Last updated: Dec 20 2023 at 11:08 UTC