[Agda] Offer of Elisp help

[Apostolis Xekoukoulotakis]

Here is the tragedy. This could cut the cost of theorem proving to "half"
for a multitude of mathematicians out there
but its development is not original research, thus noone wants to develop
it.

For the same reason, I cannot understand why universities would not fund
such a project , since it would increase their speed of research.
The reduction of research costs, simply makes the lack of funding illogical.


On Wed, Oct 24, 2018 at 4:31 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> That's a shame. Could you/we not recruit some students to work on this as
> part of a project?
>
> Thorsten
>
> On 24/10/2018, 07:44, "Peter Divianszky" <divipp at gmail.com> wrote:
>
>     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
>     >
>
>
>
>
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181024/a23ca5af/attachment.html>