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

As a newbie, I like this featurea a lot. I find it a little bit difficult to read though, because for every step I have to spot the differences displayed in the coqtop annotation.

To make it become really beautiful, we could process this data even more and create a replica of the coq IDE, in which you can move through the proof with left and right arrows.

There already exists a web IDE for Coq; we don’t need to build that.

https://github.com/ejgallego/jscoq

Do you and/or @perronet want to look into setting it up with Prosa “pre-loaded” and ready to step through?

The tools in this branch are not intended as a substitute for interactive proof exploration. Rather, I think this will be useful for preparing written tutorials, slides for teaching, etc.

This looks cool, I will look into how to integrate this.

added 30 commits

• 85c52dd0...f4330fe0 - 25 commits from branch master
• 84947804 - add script for recording proof state
• d0189446 - don't pick up annotated copies in create_makefile.sh
• be102e4e - add script for interspersing proof state in source files
• fdfef6bf - CI: build docs with interspersed proof state
• 1f5f0a2f - proofloc.py: "Next Obligation" also starts a proof

Compare with previous version

added 2 commits

• 21c1e92e - CI: build docs with interspersed proof state
• d9d1c285 - proofloc.py: "Next Obligation" also starts a proof

Compare with previous version

added 35 commits

• d9d1c285...0d392409 - 30 commits from branch master
• 323c243a - add script for recording proof state
• bd0752cf - don't pick up annotated copies in create_makefile.sh
• 0230b50e - add script for interspersing proof state in source files
• 8e06a296 - CI: build docs with interspersed proof state
• 8fa7605a - proofloc.py: "Next Obligation" also starts a proof

Compare with previous version

As there are no complaints, I'm merging this.

merged