I wanted generate a (AST) of proof tree and potentially save it (as a text file or json or something easy to manipulate, ideally cross plataform/language, ocaml, python…).
How does one do this? I read from the discussion on the Coq grammar that one can use SerAPI or Coq to split the script into sentences. Is that the main thing I need to do to generate a savable proof tree of Coq?
Since you’re asking quite a few related questions with many “unknowns”, can you elaborate more on the goal behind your questions?
You might also be interested in https://plv.csail.mit.edu/blog/pages/how-to.html#how-to, since it points to potentially related tools.
How does one do this? I read from the discussion on the Coq grammar that one can use SerAPI or Coq to split the script into sentences. Is that the main thing I need to do to generate a savable proof tree of Coq?
If you just want to split into sentences, the -time option of coqc might be enough. Otherwise, you should look into SerAPI and sercomp. I have some yet-unreleased tools for this, which are used to generate the page that @Blaisorblade pointed to; feel free to PM me if you want to have a look. You can look into proviola too, the keyword is a movie (a recording of a proof script and its output).