Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Suggestions for Proof General?


Chronological Thread 
  • From: "Paul A. Steckler" <steck AT stecksoft.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Suggestions for Proof General?
  • Date: Wed, 15 Jun 2016 15:59:33 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
  • Ironport-phdr: 9a23:jUfHzhLGGCqiiX8pJtmcpTZWNBhigK39O0sv0rFitYgUL/jxwZ3uMQTl6Ol3ixeRBMOAu6MC27Sd6vy6EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxh775osGJKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBnxyOGcsocbvqBPrTA2V53JaXH9AwTRSBA2QpinzQ5O5m22yjfZw0yqeMNe8BeQvRTmp7I9wVBLjizwAOSJ/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz
I'm in the process of reworking Proof General to support async
processing in coqtop.

As part of that exercise, I'll be doing quite a bit of code
reorganization. In particular, I'll be discarding support for the Coq
REPL (as well as other REPLs). This may be a good time to consider
adding other features, or at least accommodating their future
implementation.

One such feature might be the ability to run multiple coqtop's.

Anything else that others can suggest?

-- Paul

Archive powered by MHonArc 2.6.18.

Top of Page