coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] What IDE features are most missed in Coq?

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] What IDE features are most missed in Coq?
Date: Tue, 16 Jan 2018 11:09:56 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:C2D3xB+R7Lq8G/9uRHKM819IXTAuvvDOBiVQ1KB42uscTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhz1hikHKTA3/mPYisJsg6xcrx2svBN/z5LObYyPLvdyYqHQcNUHTmRBRMZRUClBD5u4YYsIFeUOIeZYr4j4p1ATsBa+HxejBOLzyj9OmHD2x7Ax3uMkEQ7c3QwgG8kDsHbTrNrvKKgSUeG1zKzRwTrYdfNZxzb96JTOch8/u/GAR69/ftTIxEQpCgjLgFKQqYn/MDOU0OQAq2ub7+t8Ve61lWEothxxriCtxscrkIbGmoIVylHB9Slg24k1P8O3SE9nYd6iDpRQrTuWOJZoTc4kXmpmuz46x6UbtZO5fSUG0pAqywTBZ/CafYWE+A/vWeifLDp+mXlrYqiwhwyo/kil0uD8Vte70FJNriddktnDqGoN1xnN5cicUPd95Vmu2SyR1w/N8OFLO0U0mrDBJ5E83LE8jpsTsULdES/qgEj6ka2be0Q+9uWs8ejrfKjqq5GGO4NphAzzPLwimsmlDuQ5NggOUXKb+eO51LD7+E32WrRKjvktn6nbt5DVP9gUpq64Aw9Qy4os8Ay/ACmn0NQEm3kIMkhFdAiagIf3I13OOuz3De+jg1Swlzdm3+zJPrr4ApnUMnfDlKrhcq1m5k5HyAszyMhf6IhOBrEAJvLzQE7xu8bCAh83KQzni9rgXd56z8YVXX+FKq6fKqLb91GStcw1JOzZRogcszb8LrAP/fPvkXk0gxdJeKCo2bMVb3mzHvVjZk+DbHvwhNobV2sH6FltBNf2gUGPBGYAL025WLgxs2liWdCWSLzbT4Xou4SvmSKyH5lYfGdDUAneE3DhfIWFXrIGci+TPslsiHoIWOr7EtNz5VSVrAb/joFfAK/M4CRC7MDh09F+5+zW0Bso+D1oCcmHlW2AHTktwzE4AgQu1aU6mnRTj1eO1a8i2q5YGMZW6ugPSQogK5PGxulzTdz/CFrM

Hi,

Am Dienstag, den 16.01.2018, 16:59 +0100 schrieb stvienna wiener:
> PS: I have read 3 papers on recent Coq IDE developments:
>
> * CoqPIE: An IDE aimed at improving proof development productivity
> * Company-Coq: Taking Proof General one step closer to a real IDE
> * jsCoq: Towards Hybrid Theorem Proving Interfaces

“A Usability Evaluation of Interactive Theorem Provers Using Focus
Groups” and other work by https://formal.iti.kit.edu/grebing/ might be
relevant.

Joachim

--
Joachim Breitner

mail AT joachim-breitner.de
http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] What IDE features are most missed in Coq?, stvienna wiener, 01/16/2018
- Re: [Coq-Club] What IDE features are most missed in Coq?, Joachim Breitner, 01/16/2018
- Re: [Coq-Club] What IDE features are most missed in Coq?, Ralf Jung, 01/25/2018