Gurkenglas (Jun 19 2020 at 20:08): Gurkenglas (Jun 19 2020 at 20:08):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?
Karl Palmskog (Jun 19 2020 at 20:19):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
Karl Palmskog (Jun 19 2020 at 20:22):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
Gurkenglas (Jun 19 2020 at 21:28):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
Karl Palmskog (Jun 19 2020 at 21:31):sounds like a downloading problem, you may want to just try again
Emilio Jesús Gallego Arias (Jun 19 2020 at 21:31):@Gurkenglas are you using Opam 2?
Karl Palmskog (Jun 19 2020 at 21:32):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: Oct 01 2023 at 18:01 UTC