Draft: Initiate a Prosa Tutorial

This is an attempt to revive Borislav's Prosa tutorial.

This is currently still in a very initial state but I hope to reach a reviewable state in the coming weeks.

This uses the Alectryon tool https://github.com/cpitclaudel/alectryon to build a nice webpage while still remaining a simple vernacular file that can be stepped through.

added 10 commits

• f9ef8745 - 1 commit from branch RT-PROOFS:master
• e371952c - add alectryon wrapper script and `make alectryon` target
• 6731e5e1 - CI: use alectryon for proof-state display
• d03906d8 - CI: don't run expensive jobs in wip- branches
• d391887e - CI: use custom Docker image for proof-state collection
• 5470f685 - CI: remove old proof-state scripts
• 2b87d4dc - Makefile: allow alectryon to work in parallel
• 6eafb6cd - Initiate a Prosa Tutorial
• 60c139c5 - Makefile: add a `make tutorial` target
• 190f468e - CI: compile the tutorial with alectryon

Compare with previous version

(Sorry for the long silence! I was swamped with service work.)

Hi Pierre,

this is great, thank you very much! Alectryon looks great; I definitely want to use it for Prosa (see also !136 (merged)).

I've taken the liberty to rebase your work, add a Makefile target, and hook it up to CI.

From my PoV, we can and should get this merged even before the tutorial content itself is finalized, because that is likely going to take a while and require contributions by many authors. What do you think?

CC: @sbozhko @mmaida @sophie — please have a look, too. make tutorial should now give you a beautiful HTML file in html/tutorial.html with steppable proofs.

For this to work, you need to have the alyctryon tool installed. It's very simple:

1. opam install "coq-serapi>=8.10.0+0.7.0"
2. python3 -m pip install alectryon

Thanks,
Björn

added 3 commits

• b3bd60cb - filter backticks in comments
• 1044ee7d - address some spelling issues
• 24ec737b - CI: exclude doc/ from comments spell-check

Compare with previous version

The tutorial is now also available as part of the documentation for all current branches.

• http://prosa.mpi-sws.org/branches/tutorial/html-tutorial/tutorial.html

(I pushed a copy of the tutorial branch to the official repo for this so it would get picked up by the update script.)

added 14 commits

• 24ec737b...9f99f33f - 8 commits from branch RT-PROOFS:master
• f5879945 - Initiate a Prosa Tutorial
• c728b708 - Makefile: add a `make tutorial` target
• 2c29c97f - CI: compile the tutorial with alectryon
• fe2cf602 - filter backticks in comments
• 72dba6f7 - address some spelling issues
• 4df3c306 - CI: exclude doc/ from comments spell-check

Compare with previous version

added 2 commits

• 195a8884 - Add Coq installation instructions to tutorial
• 224b64ea - Add Contributing sectio (TODO)

Compare with previous version

added 66 commits

• 224b64ea...4c867396 - 58 commits from branch RT-PROOFS:master
• c9071ada - Initiate a Prosa Tutorial
• ad7c9c12 - Makefile: add a `make tutorial` target
• 6fb43f08 - CI: compile the tutorial with alectryon
• 08ef10bb - filter backticks in comments
• 11c69e1e - address some spelling issues
• 125f419c - CI: exclude doc/ from comments spell-check
• 107ae85f - Add Coq installation instructions to tutorial
• 45ac6947 - Add Contributing sectio (TODO)

Compare with previous version

I'm closing this and opening a new MR because it should track branch tutorial and not proux:tutorial to ease collaboration (there doesn't seem to be a way to change that in gitlab). Sorry about that, that was originally my mistake.

closed

mentioned in merge request !191

So the new MR is there: !191