I'm trying to make OpenAI's new text generator complete Coq proofs. First I tried to make it generate lines to feed into coqtop, but I ran into problems sending and receiving single lines at a time between process inputs and outputs. So now I'm trying to compile the whole file each time GPT-3 adds a line, but coqc throws an error when the last proof isn't complete. Is there a way to make coqc accept any proof that coqide would? Should I be using another API?

if you're looking for a machine-friendly API to use for interacting with Coq, take a look at https://github.com/ejgallego/coq-serapi --- several applications in machine learning and similar are listed

by the way, doesn't GPT-3 still need Coq-specific training? If so, since Coq code is close-to-impossible to parse ad-hoc externally, you may want to take a look at our machine-readable Coq dataset generated via SerAPI: https://github.com/EngineeringSoftware/math-comp-corpus

As I tried to opam install coq-serapi, I got [ERROR] The sources of the following couldn't be obtained, aborting: - ppx_import.1.4

sounds like a downloading problem, you may want to just try again

@Gurkenglas are you using Opam 2?

ah right, I thought 1.4 sounded old, indeed the latest version is 1.7.1 if one has the proper opam version (2.0.5 or later)

Last updated: Jan 29 2023 at 05:03 UTC