coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, stvienna wiener <stvienna AT gmail.com>
Subject: Re: [Coq-Club] What IDE features are most missed in Coq?
Date: Thu, 25 Jan 2018 17:14:45 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:Aw5lsRzqxSE3hcHXCy+O+j09IxM/srCxBDY+r6Qd2+oVIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CWGRPQMhRWSxCDI2yYYQAAOgOMvpXoYTmu1sDrwGzCRWwCO7hyDJFgGL9060g0+QmFAHLxBAuEMgKsHTasd77MLoSUea6zKLVyjjDbe5W2THy6IXTdxAhufCMUatrccvf0kkjDQTFjk+fqYH8OT6ey+oDs2+e7+V6VOKvjXYqqw5wojizxscsl5LGipgUylDD8yhy3YU7JcWgRUJmb9OpFIFcuzyeOodsQc4vQntktSkmxrEepJK2ciwHxI46yxPbcfCLbomF7xz5WOqMJTp1i3Roc6+liRmo60iv0Oj8W9G00FlUqipFlcHBtnIQ1xzV7ciLUP59/l+g2TqW1ADT7vpELlsumareM54hzaQ8mYcNvkjbHy/2nlv5jLOOe0k59OWl7/7rbqjiq5OGNIJ5ixvyP6sylsCnBOQ3KAkOX2yV+eSm073j+FX0QLdXjv0wnanUq5XaJdwapqKgGA9U3J0j5wy4Dze839QUhWMHI05deBKbk4jpPEnDL+z/DfemmlijjDNrx+3dMbD6GZXMLn3DkK/7crpn6k5czhAzzdFF6J5OBLEBOqG7Zkikv9vBSxQ9LgacwuD9Cdw72JlaEXmTHK6UNqXb+UCJ6+QiOaHYf5MLuTv7LfEN6PvnjHt/klgYK/qHx5wSPUqxGvouAVifbjK4gMoHHk8Ppgt7V/PxzlqYXmgAND6JQ6sg62RjW8qdBoDZS9Xo2eTZhXbpLthtfmlDT2u0PzLtfoSAVe0LbXvJcMp5k3kfSqPnTJUuh0j36F3KjoF/J++RwRU28Ir53YEutejLlFQp6icyCN6SgTnUEjNE21gQTjpz55hR5ExwzlDZi/p6nvpfU9lL5rZKVhwwc5vEwKp2BoKqVw==

Hi,

there's also Coqoon: <https://coqoon.github.io/>

; Ralf

On 16.01.2018 16:59, stvienna wiener wrote:
> 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