[Agda] Offer of Elisp help

[David Thrane Christiansen]

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

[Alan & Kim Zimmerman]

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 <

Post by David Thrane Christiansen
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
https://lists.chalmers.se/mailman/listinfo/agda

[Thorsten Altenkirch]

Actually is there anybody working on a browser based frontend for Agda?

Thorsten

From: Agda <agda-***@lists.chalmers.se> on behalf of Alan & Kim Zimmerman <***@gmail.com>
Date: Thursday, 27 September 2018 at 20:59
To: "***@davidchristiansen.dk" <***@davidchristiansen.dk>
Cc: "***@lists.chalmers.se" <***@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 <***@davidchristiansen.dk<mailto:***@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
***@lists.chalmers.se<mailto:***@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.

[Peter Divianszky]

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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for Agda?
Thorsten
*Date: *Thursday, 27 September 2018 at 20:59
*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
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
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
https://lists.chalmers.se/mailman/listinfo/agda

[Thorsten Altenkirch]

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" <***@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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for Agda?
Thorsten
*Date: *Thursday, 27 September 2018 at 20:59
*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
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
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
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.

[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 <

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this as
part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for

Agda?

Post by Thorsten Altenkirch
Thorsten

Kim

Post by Thorsten Altenkirch
*Date: *Thursday, 27 September 2018 at 20:59
*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
Hello Agda users and implementors,
I've talked to a few people at ICFP in the last few days who

have said

Post by Thorsten Altenkirch
that a bottleneck in Agda development is that there are too few

people

Post by Thorsten Altenkirch
who know Emacs Lisp.
I know Emacs Lisp decently well. I wrote the majority of the

code in

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
advice on libraries, review code, and otherwise help out with

getting

Post by Thorsten Altenkirch
more interested developers up and running on Elisp for Agda.

This is

Post by Thorsten Altenkirch
an open offer - please just email me if you'd like to take me up

on

Post by Thorsten Altenkirch
it.
Also, if you see a feature in idris-mode that you'd like in

agda-mode,

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
know!
David
_______________________________________________
Agda mailing list
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
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
https://lists.chalmers.se/mailman/listinfo/agda

[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, <

Post by 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 <

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this as
part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for

Agda?

Post by Thorsten Altenkirch
Thorsten

Kim

Post by Thorsten Altenkirch
*Date: *Thursday, 27 September 2018 at 20:59
*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
Hello Agda users and implementors,
I've talked to a few people at ICFP in the last few days who

have said

Post by Thorsten Altenkirch
that a bottleneck in Agda development is that there are too few

people

Post by Thorsten Altenkirch
who know Emacs Lisp.
I know Emacs Lisp decently well. I wrote the majority of the

code in

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
advice on libraries, review code, and otherwise help out with

getting

Post by Thorsten Altenkirch
more interested developers up and running on Elisp for Agda.

This is

Post by Thorsten Altenkirch
an open offer - please just email me if you'd like to take me

up on

Post by Thorsten Altenkirch
it.
Also, if you see a feature in idris-mode that you'd like in

agda-mode,

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
know!
David
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the

addressee

Post by Thorsten Altenkirch
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
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

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 <

Post by 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 <

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this as
part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for

Agda?

Post by Thorsten Altenkirch
Thorsten

Kim

Post by Thorsten Altenkirch
*Date: *Thursday, 27 September 2018 at 20:59
*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
Hello Agda users and implementors,
I've talked to a few people at ICFP in the last few days who

have said

Post by Thorsten Altenkirch
that a bottleneck in Agda development is that there are too few

people

Post by Thorsten Altenkirch
who know Emacs Lisp.
I know Emacs Lisp decently well. I wrote the majority of the

code in

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
advice on libraries, review code, and otherwise help out with

getting

Post by Thorsten Altenkirch
more interested developers up and running on Elisp for Agda.

This is

Post by Thorsten Altenkirch
an open offer - please just email me if you'd like to take me

up on

Post by Thorsten Altenkirch
it.
Also, if you see a feature in idris-mode that you'd like in

agda-mode,

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
know!
David
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the

addressee

Post by Thorsten Altenkirch
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
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

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.

Post by Philip Wadler
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 <

Post by 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 <

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this
as part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for

Agda?

Post by Thorsten Altenkirch
Thorsten

Kim

Post by Thorsten Altenkirch
*Date: *Thursday, 27 September 2018 at 20:59
*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
Hello Agda users and implementors,
I've talked to a few people at ICFP in the last few days who

have said

Post by Thorsten Altenkirch
that a bottleneck in Agda development is that there are too

few people

Post by Thorsten Altenkirch
who know Emacs Lisp.
I know Emacs Lisp decently well. I wrote the majority of the

code in

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
advice on libraries, review code, and otherwise help out with

getting

Post by Thorsten Altenkirch
more interested developers up and running on Elisp for Agda.

This is

Post by Thorsten Altenkirch
an open offer - please just email me if you'd like to take me

up on

Post by Thorsten Altenkirch
it.
Also, if you see a feature in idris-mode that you'd like in

agda-mode,

Post by Thorsten Altenkirch
perhaps we can extract it into a common library to save work

for

Post by Thorsten Altenkirch
everyone. I've already done this with the keyboard- and
mouse-accessible context menus, for instance. So please just

let me

Post by Thorsten Altenkirch
know!
David
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the

addressee

Post by Thorsten Altenkirch
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email

and

Post by Thorsten Altenkirch
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham.

Email

Post by Thorsten Altenkirch
communications with the University of Nottingham may be monitored
where permitted by law.
_______________________________________________
Agda mailing list
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Philip Wadler]

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 <

Post by Apostolis Xekoukoulotakis
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.

Post by Philip Wadler
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 <

Post by 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 <

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this
as part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for

Agda?

Post by Thorsten Altenkirch
Thorsten

& Kim

Post by Thorsten Altenkirch
*Date: *Thursday, 27 September 2018 at 20:59
*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.

Post by Thorsten Altenkirch
Alan
On Thu, 27 Sep 2018 at 14:56, David Thrane Christiansen
Hello Agda users and implementors,
I've talked to a few people at ICFP in the last few days who

have said

Post by Thorsten Altenkirch
that a bottleneck in Agda development is that there are too

few people

Post by Thorsten Altenkirch
who know Emacs Lisp.
I know Emacs Lisp decently well. I wrote the majority of the

code in

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
advice on libraries, review code, and otherwise help out with

getting

Post by Thorsten Altenkirch
more interested developers up and running on Elisp for Agda.

This is

Post by Thorsten Altenkirch
an open offer - please just email me if you'd like to take me

up on

Post by Thorsten Altenkirch
it.
Also, if you see a feature in idris-mode that you'd like in

agda-mode,

Post by Thorsten Altenkirch
perhaps we can extract it into a common library to save work

for

Post by Thorsten Altenkirch
everyone. I've already done this with the keyboard- and
mouse-accessible context menus, for instance. So please just

let me

Post by Thorsten Altenkirch
know!
David
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the

addressee

Post by Thorsten Altenkirch
and may contain confidential information. If you have received

this

Post by Thorsten Altenkirch
message in error, please contact the sender and delete the email

and

Post by Thorsten Altenkirch
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham.

Email

Post by Thorsten Altenkirch
communications with the University of Nottingham may be monitored
where permitted by law.
_______________________________________________
Agda mailing list
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[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

Post by Bas Spitters
There is jscoq for coq.
Perhaps some parts can be reused.
from my phone

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.

Post by Thorsten Altenkirch
That's a shame. Could you/we not recruit some students to work on this as part of a project?
Thorsten
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

Post by Thorsten Altenkirch
Actually is there anybody working on a browser based frontend for Agda?
Thorsten
*Date: *Thursday, 27 September 2018 at 20:59
*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
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
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
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Simon Huber
https://github.com/danr/awe/
(And I am not quite sure if this is what you are after.)

One question is if the Agda process should run on the client or on the
server. I can imagine that it is not so easy to compile Agda to
Javascript. On the other hand, Agda can be resource intensive, which can
lead to problems for a server-based implementation. Furthermore Agda is
not designed for this kind of environment. (For instance, it is compiled
with -rtsopts, which can in some cases be a security issue.)