The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Dear Thorsten,

  there is an easy way to incorporate proof states in the .v file as a 
comment 
(and even a key binding for doing that in proof-general, can’t remember which 
as
it happened to me accidentally). Basically, you can put the generated text 
inside
[[ ]] in the comment and get “nice" output. Not fully automatic but that’s 
something. 
I suppose the new coqdoc (Yann ?) is able to do better. coq-tex reprocesses 
the 
commands while (old) coqdoc is based on a lexer only (!).

Cheers,
— Matthieu

On 21 nov. 2013, at 13:19, Altenkirch Thorsten 
<psztxa AT exmail.nottingham.ac.uk>
 wrote:

> Thank you Nuno.
> 
> I need something which works with latex. Basically an improved coq-tex :-)
> 
> I need a bit more flexibitlity (I..e sometimes I want to display a prrof 
> state and something I don't) and I would like something that looks a bit 
> better. I was just wondering wether anybody has done something like this or 
> has a good idea how to go about it. E.g. how does coq-tex work?
> 
> Cheers,
> Thorsten
> 
> 
> 
> From: Nuno Gaspar 
> <nmpgaspar AT gmail.com>
> To: Thorsten Altenkirch 
> <psztxa AT exmail.nottingham.ac.uk>
> Cc: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] print coq proof states?
> 
> 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.
> 
> 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.
>