[Agda] Offer of Elisp help

[Simon Huber]

There is also awe for a previous version of Agda (might not work anymore):

  https://github.com/danr/awe/

(And I am not quite sure if this is what you are after.)

--Simon

--Simon

On Wed, Oct 24, 2018 at 5:29 PM Bas Spitters <b.a.w.spitters at gmail.com> wrote:
>
> 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