Add scripts for proof state recording and interspersing

This MR adds two new scripts:

• scripts/record-proof-state.py, which runs a .v file through coqtop and records the interactions as a JSON or YAML file, and
• scripts/intersperse-proof-state.py, which annotates a .v file by injecting the recorded proof state as a comment after each step of a proof.

I believe this will be helpful for studying and teaching how to work with Coq/Prosa.

This MR also hooks this up with GitLab CI to auto-generate documentation with interspersed proof state. You may see an example here: rt.restructuring.analysis.edf.optimality.html

Here's the tree: http://prosa.mpi-sws.org/branches/proof-recorder/with-proofs-and-proof-state/tree.html

Please let me know if you have any comments or suggestions.

CC: @sophie @mlesourd @sbozhko @proux @borni @mmaida