[Agda] Offer of Elisp help

Peter Divianszky divipp at gmail.com
Wed Oct 24 08:44:43 CEST 2018


I started to work on a browser based frontend but stopped a long time 
ago. I don't think I'll work on it in the near future.

Péter

On 9/28/18 11:25 AM, Thorsten Altenkirch wrote:
> Actually is there anybody working on a browser based frontend for Agda?
> 
> Thorsten
> 
> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Alan & Kim 
> Zimmerman <alan.zimm at gmail.com>
> *Date: *Thursday, 27 September 2018 at 20:59
> *To: *"david at davidchristiansen.dk" <david at davidchristiansen.dk>
> *Cc: *"agda at lists.chalmers.se" <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Offer of Elisp help
> 
> Would there be any benefit to doing this around the 
> language-server-protocol?
> 
> I would love to get some of these features into Haskell, over time.
> 
> Alan
> 
> On Thu, 27 Sep 2018 at 14:56, David Thrane Christiansen 
> <david at davidchristiansen.dk<mailto:david at davidchristiansen.dk>> wrote:
> 
>     Hello Agda users and implementors,
> 
>     I've talked to a few people at ICFP in the last few days who have said
>     that a bottleneck in Agda development is that there are too few people
>     who know Emacs Lisp.
> 
>     I know Emacs Lisp decently well. I wrote the majority of the code in
>     Idris's Emacs mode, for instance. I don't have time to take on
>     projects in Agda's interface, but I'm happy to discuss designs, give
>     advice on libraries, review code, and otherwise help out with getting
>     more interested developers up and running on Elisp for Agda. This is
>     an open offer - please just email me if you'd like to take me up on
>     it.
> 
>     Also, if you see a feature in idris-mode that you'd like in agda-mode,
>     perhaps we can extract it into a common library to save work for
>     everyone. I've already done this with the keyboard- and
>     mouse-accessible context menus, for instance. So please just let me
>     know!
> 
>     David
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


More information about the Agda mailing list