[Agda] Offer of Elisp help

[Bas Spitters]

There is jscoq for coq.
Perhaps some parts can be reused.

from my phone

On Wed, 24 Oct 2018, 17:10 Apostolis Xekoukoulotakis, <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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
>>
> _______________________________________________
> 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/94cd7807/attachment.html>