The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello,

Not exactly what you want but you may wanna check Proviola [1]. It may be what you want if you are willing to distribute html files for your course support material.

[1] http://mws.cs.ru.nl/proviola/

2013/11/19 Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>

Hi,

I'd like to revise my lecture notes (for my course Introduction to formal reasoning) and explain some coq proofs referring to the current proof state. Hence I am looking for some software support to do this easily: ideally a tool (maybe somebody already made something for this purpose) or some suggestion how to make one (without too much effort). I want to insert these annotated proof scripts into a latex document.

I know ideally this shouldn't necessary and people should just step through the proof interactively. However, I find often people (especially students) don't do that and it seems better if one could just insert proof state and comments and certain points in a proof.

I have been using coq-doc to produce html and latex but as far as I know there isn't a way to insert the proof state into the documents produced by coqdoc. There is also coq-tex which sort of does what I want but too much of it and the output is really ugly. Maybe I need to post process coq-tex output? Or can I use coqtop directly?

Cheers,

Thorsten

P.S. Apologies for not being able to give a link to my course but my university decided to disable anonymous login for moodle which means that nobody from outside can look at our courses. We are still arguing with them.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.