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).