The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Mar 03, 2014 at 03:37:10PM +0100, Daniel de Rauglaudre wrote:
> 7/ I did not test other interfaces: you tell me they are numerous?

I've heard of a vim based one and an eclipse based one.  Neither works
for you I guess.

No, when we debug we don't produce a new proof script: we already have
one (that does not work).  We Drop into the ML toplevel to inspect
things (when the byte toplevel is fast enough).  Or, as I do most of the
times, add printf here and there and inspect the resulting trace.
No need to produce a well indented proof script in these scenarios.

> I recognize that my system is strange:

Yep.  Hence nobody notices when this workflow breaks.  And nobody's
energy is being spent into making this very peculiar interaction mode
work better, I'm afraid.

What I suggest is to write a couple of tests in coq/test-suite/output/
so that we notice when things break badly.  Or switch to a more popular
user interface...

Cheers
-- 
Enrico Tassi