coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: stvienna wiener <stvienna AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] What IDE features are most missed in Coq?
Date: Tue, 16 Jan 2018 16:59:45 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stvienna AT gmail.com; spf=Pass smtp.mailfrom=stvienna AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f176.google.com
Ironport-phdr: 9a23:qlm6VxRft+RGcHziQW+q+GY7Mdpsv+yvbD5Q0YIujvd0So/mwa68bRaN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHZhMJzkaxVvg6uqgdjw4LIeoyZKOZycr/fcN4cWGFPXtxRVytEAo6kdIsPE/QBPedGoIn7oVsBtwa1BAetBOzxzD9HmGX21rA93uQ6DQHGwg0gEMwIsHTSttr4L6gSUeWvw6nJyTXPde9Z2TD46IXRdB0qvPKCXapofMbP1UUiExnJg1aQpID/Ij+Y0voBv3KG4+diVO+ijXMspRtrrTi13Mgsj5HEhoILxVDA8iV02IM1Kse5SE5/eNKkCJVQuz2DO4t4X88vQWBltDw1yr0Bvp67cywKx4o9yxHDbPyHdpCE4hPlVOmPPTd1nGxpdK67ihqo8kWtyvfwWtSw3VpUtCZJj9vBu3EV2xzW8MeHS/99/km72TaI0gDe8vpEIVwqlaraNZEhxLgwmYAIvETMGy/5gkT2jKuMeko4/eio7vzrYq/6qZ+EK490lgb+P7wylcy4GOQ0KxQBX2yG+eunz7Dj5k34QLBSjvIsiKXZsZbaJd4apqGjGQNV3JwjuF6DCGKt181dln0aJnpEfgiGhs7nIQLgOvf9WOyjnVWhljFij+/HM7vsGN2ZNWTdkbrne79V5EtVyQ51xtdascEHQoodKe7+Dxei/OfTCQU0ZlTtkrTXTe5l34ZbYlqhR6qQMafcq1iNv7t9LOyFZYtTszH4eaF8u6zeyEQhkFpYRpGHmIMNYSnhTPtjKkSdJ3Hrh4VZSDpYjk8FVOXvzWa6f3tTanK1Bfxu4zg6DMe+A9+GSNny3vqO2yC0GpAQbWdDWAiB

Hi all,

I am doing a survey of current state-of the art IDEs for theorem
proves such as Coq, Agda, Lean, Isabelle, etc.

What is on the top of the list of the most missed features? I guess
most Coq users use the emacs proof general interface.

Best,
Stephan

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

[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