[opentheory-users] Is OpenTheory usable with Coq?

[Rob Arthan]

> On 30 Dec 2015, at 03:54, Yannick <yannick_duchene at yahoo.fr> wrote:
> 
> 
> 
> ------- Forwarded message -------
> From: Yannick <yannick_duchene at yahoo.fr>
> To: "Ramana Kumar" <ramana at member.fsf.org>
> Cc:
> Subject: Re: [opentheory-users] Is OpenTheory usable with Coq?
> Date: Wed, 30 Dec 2015 02:46:31 +0100
> 
> On Tue, 29 Dec 2015 13:25:44 +0100, Ramana Kumar <ramana at member.fsf.org> wrote:
> 
> I should add that for HOL4 (and HOL Light, I think) there are editor-based interfaces (for Vim and for Emacs, at least) so you are not confined to using only the read-eval-print loop.
> 
> Precisely the two editors I'm afraid of :-D . Don't mind, I will setup what I need if I'm really not OK with the SML interpreter interface.
> 

The ProofPower user interface (called xpp) is at heart just a simple mouse- and menu -driven wisiwyg text editor that lets you execute selections from the text you are editing in the read-eval-print loop of an interactive program. I routinely use it to develop scripts not just for ProofPower but for HOL Light, HOL4 and other programs like sh, bc and gnuplot. I believe it was quite popular for developing HOL Light code with some of the Flyspeck team in Vietnam.

Regards,

Rob.