The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

Hi Thorsten,

> I am preparing some lecture notes using latex and I'd like to explain
> some coq proofs, displaying the changing proof state in my notes. Is
> there any tool support for this? It seems that neither coqdoc or
> coq-tex are up to the job.
>
> Obviously, it is rather doubtful whether paper is the best way to
> present a proof and maybe one should step through a proof using coqide
> and diplay the comments in a different window. However, for the moment
> I'd be happy if there is an easy way to avoid lots of ugly verbatims
> in my notes.

I've been wrestling with the same issue while preparing lectures for  
the graduate "software foundations" course that I'm now in the middle  
of teaching (lecture 5 goes live at noon!).  In the end, I wound up  
deciding to use *only* Coq (running under ProofGeneral) to give the  
lectures: all the textual material is just comments in the coq  
script.  So far I am very happy with this approach, since it means  
that (a) I can step back and forth within proofs during the lecture  
and let the students see how the state changes and (b) when the  
students go home, they have a verbatim copy of exactly what I showed  
in lecture that they can replay, experiment with, change, etc.

Best,

   - Benjamin

P.S.  In case anybody is interested in having a look, the lecture  
notes can be found here:

   http://www.seas.upenn.edu/~cis500/cis500-f07/schedule.html