Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Suggestions for Proof General?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Suggestions for Proof General?
  • Date: Thu, 16 Jun 2016 11:33:50 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f48.google.com
  • Ironport-phdr: 9a23:rP6KNBMsG8xBtc3ly1Ul6mtUPXoX/o7sNwtQ0KIMzox0KPv8rarrMEGX3/hxlliBBdydsKIVzbqG+Pi8EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxh7D5o8GbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLHzX8BWC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijdbE5Qy6vp4xsVQX0iSoaf2oh8WzNkME2h6VGug6gqgFXzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmxOs5WV7IM
As it is it can really help beginners into Ltac programming.

The fact that debug mode is not available in coqide (and was not easy to use in pg) explains the fact that few people use it.

For power users it lacks some feature, mainly breakpoints and printing commands.

Maybe we could also have a support for the "Drop" machinery?

P.

2016-06-16 1:34 GMT+02:00 Jonathan Leivent <jonikelee AT gmail.com>:


On 06/15/2016 06:39 PM, Pierre Courtieu wrote:
Supporting Ltac debug mode would be good.
P.



Does anyone use that?  I find it unhelpful.  Although, the UI has something to do with that.  If Ltac had a more gdb-style debug mode, with real breakpoints & watchpoints, inspection of env bindings, stack view, source-level display, debug entry on break, and a richer command set, then supporting that would be great.

-- Jonathan



Archive powered by MHonArc 2.6.18.

Top of Page