[Agda] Offer of Elisp help

Thorsten Altenkirch Thorsten.Altenkirch at nottingham.ac.uk
Fri Sep 28 11:25:18 CEST 2018


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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180928/7e218982/attachment.html>


More information about the Agda mailing list