[Agda] Offer of Elisp help
Philip Wadler
wadler at inf.ed.ac.uk
Wed Oct 24 22:49:39 CEST 2018
Thank you for the suggestions. I would be surprised if they showed a
two-fold improvement in productivity as you claim, but would be delighted
to be convinced. Regardless, I believe that a browser-based interface for
Agda could be of value. Yours, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Too brief? Here's why: http://www.emailcharter.org/
On Wed, 24 Oct 2018 at 21:01, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:
> Philip, I am not part of a university at the moment, but since you asked :
>
> Some options to show the above are :
> a) Acquire written testimonies from researchers that use the software ,
> describing the impact that it has on their work.
> b) Measuring the scientific impact of the software by assembling the
> number of research papers that reference it, their citations etc.
> c) Measure the increase of productivity. The best way to do that would by
> expressing analytically how it saves time to users. And idris could be used
> as a concrete point of reference for such time savings.
>
> Using b) and c) , one could provide an estimate for a future increase of
> scientific impact.
>
> On Wed, Oct 24, 2018 at 8:40 PM Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>
>> Apostolis, Can you document your claim? That would help one of us to
>> submit a proposal along the lines you suggest. Cheers, -- P
>>
>> . \ Philip Wadler, Professor of Theoretical Computer Science,
>> . /\ School of Informatics, University of Edinburgh
>> . / \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> Too brief? Here's why: http://www.emailcharter.org/
>>
>>
>> On Wed, 24 Oct 2018 at 16:43, 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
>>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181024/06eac9e1/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181024/06eac9e1/attachment.ksh>
More information about the Agda
mailing list