coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coqtop machine interface

From: Ian Zimmerman <itz AT very.loosely.org>
To: Coq-Club Mailinglist <coq-club AT inria.fr>
Subject: [Coq-Club] Coqtop machine interface
Date: Thu, 31 Oct 2019 12:25:59 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=itz AT very.loosely.org; spf=Pass smtp.mailfrom=itz AT very.loosely.org; spf=Pass smtp.helo=postmaster AT very.loosely.org
Ironport-phdr: 9a23:AYA3wRf6kSvzVUMcxnPlJAcslGMj4u6mDksu8pMizoh2WeGdxcS8bB7h7PlgxGXEQZ/co6odzbaP6Oa5ATFLuMzY+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi4oAnLq8UanYtvJqksxhfXv3dDZvhby35vKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zMh8dukKxUvg6upx1nw47Vfo6VMuZ+frjAdt8eXGZNQ9pdWzBEDo66aIQBEvcBPf1Ar4bju1QOsRWwBQ6pBOz1yz9IgGL90ak13uklFA3L2hErEdATv3TOtNj7OqccX/6owqfLwjrMc+5Z1jnm5YjUbhwsu+2AUa5qfMbPz0QkCgPLjk+XqYzgJz6b1f4Cs26G5OVjVOKvjmsnpB9rojiq3MgsjJTCi4UUylDY9CR025g1KsOiSE97e9KkFJxQtyaBN4RoRsMjQ3tkuCEgyr0JoJO2ejUBxpogxx7acfOHco6I7wrmVOaWJjd4g2hpd664hxa390Wr1+7yVtGs3VpXrCdInMPAum4N2hHT8MSLVOZx80e71TuO0w3f8uBJLEIumabGKZMszaQ8moQdvEnNBCP6hlj6ga2Qe0454Oan8f7nba/jppKEN497lAX+MqM2l8yhH+s4KAgPU3Kf+eS7073j5lP2QLFKj/EslanZqp/aKdwapq6/HQBVzp4u5wu9AjqoytgUg3kKIVJfdB6ZkoTkO0vCLfH8APunhlSjijZrx/TIPr37BZXNK2DOkLb9fbd88ENc1hQ8zcpf5p5ODrEBJ/XzWlTvu9zcDh41KQu0w/zoCNllzIMRRXqPArOFMKPVqVKH+uUvI/CVaIAJvDb9NuMq6uX1jX45nF8dZbOm0YEWaHC+BPRmIl+WbWDigtcbQi82uV8VS/Wvo1mfW3Z2bne2XqQz4jAgFMryBoDaA4upnbap3SGhH5QQaHoQWX6WFnK9VoyCE8UNbSefOMpolHRQVKSzY5EszwDosAj90LdjP6zT4CJO5sGr78R8++CGzUJ6zjdzFcnIljzUFjAmriYzXzYzmZtHjwl4w1aH37J/hqUIR8Je/eIPVgA9LpPY3qp9Ed+gA1ucLOfMc06vR5CdOR90Tt81xIZeMVhwAcTkihfExCeuEvkSjbPZXcVooJKZ5GD4IoNG81iDzLMo1gl0XMZVJCuigalk+gzCQYnTnBfBmg==

I have a series of related questions about coq user interfaces.

1. coqide seems to invoke not coqtop, but coqidetop. What is the
difference?

2. What is the protocol spoken between coqide and coqidetop? Is it
documented somewhere?

3. Is the protocol the same between Proof General and whatever coq
program PG invokes?

I am an Emacs user since forever (as some people here know, ahem) and I
would really very much prefer an Emacs interface to coq, but I find PG
to be a badly behaved Emacs package in several ways, so I'm tempted to
do my own.

--
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.

[Coq-Club] Coqtop machine interface, Ian Zimmerman, 10/31/2019
- Re: [Coq-Club] Coqtop machine interface, Rustam Zhumagambetov, 10/31/2019