jasonrute
commented
4 years ago A few things:
- This isn't a full API, certainly not at the level of CoqGym, but more of a prototype for how one could make such an API.
- If one was serious about using this API, we should replace my tacky lean server with the new lean-python client (probably the Trio version).
- This prototype has serious robustness and performance issues, including:
- If one wants to put goal X into the prover, then one types the goal into a lean file via the lean server. If one takes Lean's official pretty print of a theorem (and enter it back Lean) then Lean may not except it. (I guess this round-trip problem is getting serious attention in Lean 4.)
- It is even worse for intermediate tactic states. The way this currently works is that you take the intermediate tactic state (i.e. goal state, goal stack) and then serialize it (via the pretty printer) and plug it back into Lean. This often won't work for complicated goals. I don't have exact numbers, but I think it would be a significant problem.
- The Lean server it built as a language server for editors like VSCode and Emacs. We are really hacking it to make it work for our purposes here. In particular, there is a hardcoded delay of 0.1 seconds for checking a modification of a file. In practice, this means unless one batches requests to the Lean server, the round trip is 0.1 seconds.
I'm currently working on a different prototype with a different vision:
- communicate directly with a lean file via Lean's IO mechanism.
- Lean will keep track of and index tactic states. You can tell Lean to jump to a previous state in a proof.
- There will be a curated fix list of Lean tactics (or reasonable equivalents to the standard interactive tactics). (This will be similar to CoqGym's context-free grammer.)
- One can use this interface in a few different ways:
- (Gym for specific points in a tactic script) Put a special marker in a lean file proof. Have a python script call that Lean file as a process and then lean communicates to python information about the state, and python tells Lean what tactics to try.)
- (Gym for theorems) Put a marker just before a theorem in a lean file. Have a python script call that Lean file as a process and then lean communicates to python information about the state in a proof (starting from scratch), and python tells Lean what tactics to try.)
- (Gym for new theorems) Put a marker in a file with the imports to use (and maybe universe levels?). Have a python script call that Lean file as a process and that python script tells the Lean file which (possibly new) theorem to start proving.
- (Lean proof advisor) Call a tactic in Lean (as normal from VSCode) and that tactic calls a pre-trained Python AI process which suggests a proof (or partial proof). This will be a big breakthrough, since currently I don't think there is an easy way to use, say, CoqGym to help with Coq proof engineering.
As for CoqGym, I'd like to learn more, but this isn't the place to discuss it. I'll hit you up on the lean prover Zulip.
Hi @jasonrute!
I think it would be great to have a document so we can compare the API to CoqGym (the only usable API for AITP that I know of).
Do you agree this is worth it and could help LeanGym (what seems your building here)?