coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] external editor in coqide

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] external editor in coqide
Date: Thu, 24 Jan 2019 11:10:53 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f47.google.com
Ironport-phdr: 9a23:IpD8AhGbz+74FpV3bWBdk51GYnF86YWxBRYc798ds5kLTJ78rsqwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb4UBAekcM+hGs4bwvEEBoQekCAS2GO/j1j1Fi3nr1qM6yeQhFgTG0RQ+EdIOqnPUq836O6QTUeCwyanH0y/Db/ZM1jf77ojDbxcsoe2MXb1udsrd00guFwLAjlWVqIzoJDyV1uEXvGia6+psT/6gi2kiqwxopDWk28kiio7Mho0Py1DE8z10wIgvJdKiTU50e9GkEJpMty2AMIt2WMwiTmd1syg50r0LoYC3cDQOxZg9xBPSa+aLf5aW7h79TuqcLjV1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HJtn8X1hzT7tGLSuZn8Uu8wDqP2Q/e5+NeLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvgPqgwhMCzG+s1PwoWU2ie4+u81bnj/UPjQLVNi/07irXZsJDEKsQcvKK4Ag5V0oMm6xa+FDqm39EYkmMGLFJBYh6Ik4/pO1TWLPDiEfi/m0iskCtsx/3eIrLhBYzNImHfn7flYLZy8FVRyBEzzNBa/5JbEKsNIPP1Wk/rtdzXFAU1MwKuw7WvNNIo/YQHEUmLH6XRZKjVqBqD4v8lC+iKfo4c/jjnfasL/fnr2EM5GFgqT6is2JYNbXm+GLwyP0WUZjz+g9IEEE8FuwM/SKrhj1jUAm0bXGq7Q69pvmJzM4mhF4qWA9n12OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMXCdJ8ZglnoPUr3zEtZ9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/B54w1aHlLVx2rlWSYMV6PROXQM3c5Xbyr4iBg==

I just discovered https://framagit.org/manu/coq-au-vim which apparently supports talking with Coq using the asychronous XML protocol (like CoqIDE and the corresponding Proof General branch).

Are some vim people using it? Is it good?

Of course, there is also the older coquille which also provides vim support, in the style of Proof General. I don't know if it kept working with recent Coq version though: the last commit is quite old.

Le jeu. 24 janv. 2019 à 10:46, Laurent Thery <Laurent.Thery AT inria.fr> a écrit :

On 1/24/19 6:44 AM, Jeremy Dawson wrote:
> So how do I start up my usual text editor (vi) while using coqide?

You can configurate the editor in Edit->Preferences->Externals->External
Editor replacing emacs by gex

--
Laurent

[Coq-Club] external editor in coqide, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] external editor in coqide, Laurent Thery, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Théo Zimmermann, 01/24/2019
    - Re: [Coq-Club] external editor in coqide, Anders Lundstedt, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019
    - Re: [Coq-Club] external editor in coqide, Jason -Zhong Sheng- Hu, 01/29/2019
      - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019