The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Mon, Mar 03, 2014 at 02:46:03PM +0100, Enrico Tassi wrote:

> Still I'd like to understand your usecase.  Using coqtop from the
> terminal is useful for debugging only.  There are plenty of user
> interfaces, graphical or textual, and even more are coming.  And with a
> user interface you don't need Show Script to store your work in a text
> file.  Could you explain why you need Show Script?

Historical reasons:

1/ I started this way three years ago
2/ When I started Coq, there were no Coq users around me to advise me
3/ I am used to this way now
4/ I am an old man having my habits
5/ I could change, but since nobody loves me, I am not motivated

Intellectual reasons:

1/ I don't like running programs in my emacs, except "make"
2/ I dislike unnecessary desktop environments
3/ I like to be minimalist: emacs, terminal, that's all
4/ I like to organize my windows my way
5/ I tested "proofgeneral": not convinced; too many too small windows
6/ I tested "coqide": see 2/ and 5/
7/ I did not test other interfaces: you tell me they are numerous?
8/ I like to know what happens, what are tactics, what are commands, etc.
9/ In shell, I prefer typing commands in a terminal better than clicking
10/ I am the author of ledit, it's my baby, I like to see it running
11/ in debugging, don't you need Show Script in your coqtop?

I recognize that my system is strange:

1/ I run two coqs: "coqtop" in a term and "make" in my emacs that runs coqc
2/ I have to cut-and-paste from term to emacs and vice-versa,
3/ I use another term running "ledit -u >/dev/null" to store my intermediate
   information: unfinished scripts, Checks, SearchAbout, etc.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/