<div dir="auto">There is jscoq for coq.<div dir="auto">Perhaps some parts can be reused.<br><br><div data-smartmail="gmail_signature" dir="auto">from my phone</div></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, 24 Oct 2018, 17:10 Apostolis Xekoukoulotakis, <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Here is the tragedy. This could cut the cost of theorem proving to "half" for a multitude of mathematicians out there <br></div><div>but its development is not original research, thus noone wants to develop it.</div><div><br></div><div>For the same reason, I cannot understand why universities would not fund such a project , since it would increase their speed of research.</div><div>The reduction of research costs, simply makes the lack of funding illogical.</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Oct 24, 2018 at 4:31 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank" rel="noreferrer">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That's a shame. Could you/we not recruit some students to work on this as part of a project?<br>
<br>
Thorsten<br>
<br>
On 24/10/2018, 07:44, "Peter Divianszky" <<a href="mailto:divipp@gmail.com" target="_blank" rel="noreferrer">divipp@gmail.com</a>> wrote:<br>
<br>
I started to work on a browser based frontend but stopped a long time <br>
ago. I don't think I'll work on it in the near future.<br>
<br>
Péter<br>
<br>
On 9/28/18 11:25 AM, Thorsten Altenkirch wrote:<br>
> Actually is there anybody working on a browser based frontend for Agda?<br>
> <br>
> Thorsten<br>
> <br>
> *From: *Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank" rel="noreferrer">agda-bounces@lists.chalmers.se</a>> on behalf of Alan & Kim <br>
> Zimmerman <<a href="mailto:alan.zimm@gmail.com" target="_blank" rel="noreferrer">alan.zimm@gmail.com</a>><br>
> *Date: *Thursday, 27 September 2018 at 20:59<br>
> *To: *"<a href="mailto:david@davidchristiansen.dk" target="_blank" rel="noreferrer">david@davidchristiansen.dk</a>" <<a href="mailto:david@davidchristiansen.dk" target="_blank" rel="noreferrer">david@davidchristiansen.dk</a>><br>
> *Cc: *"<a href="mailto:agda@lists.chalmers.se" target="_blank" rel="noreferrer">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank" rel="noreferrer">agda@lists.chalmers.se</a>><br>
> *Subject: *Re: [Agda] Offer of Elisp help<br>
> <br>
> Would there be any benefit to doing this around the <br>
> language-server-protocol?<br>
> <br>
> I would love to get some of these features into Haskell, over time.<br>
> <br>
> Alan<br>
> <br>
> On Thu, 27 Sep 2018 at 14:56, David Thrane Christiansen <br>
> <<a href="mailto:david@davidchristiansen.dk" target="_blank" rel="noreferrer">david@davidchristiansen.dk</a><mailto:<a href="mailto:david@davidchristiansen.dk" target="_blank" rel="noreferrer">david@davidchristiansen.dk</a>>> wrote:<br>
> <br>
> Hello Agda users and implementors,<br>
> <br>
> I've talked to a few people at ICFP in the last few days who have said<br>
> that a bottleneck in Agda development is that there are too few people<br>
> who know Emacs Lisp.<br>
> <br>
> I know Emacs Lisp decently well. I wrote the majority of the code in<br>
> Idris's Emacs mode, for instance. I don't have time to take on<br>
> projects in Agda's interface, but I'm happy to discuss designs, give<br>
> advice on libraries, review code, and otherwise help out with getting<br>
> more interested developers up and running on Elisp for Agda. This is<br>
> an open offer - please just email me if you'd like to take me up on<br>
> it.<br>
> <br>
> Also, if you see a feature in idris-mode that you'd like in agda-mode,<br>
> perhaps we can extract it into a common library to save work for<br>
> everyone. I've already done this with the keyboard- and<br>
> mouse-accessible context menus, for instance. So please just let me<br>
> know!<br>
> <br>
> David<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> This message and any attachment are intended solely for the addressee<br>
> and may contain confidential information. If you have received this<br>
> message in error, please contact the sender and delete the email and<br>
> attachment.<br>
> <br>
> Any views or opinions expressed by the author of this email do not<br>
> necessarily reflect the views of the University of Nottingham. Email<br>
> communications with the University of Nottingham may be monitored<br>
> where permitted by law.<br>
> <br>
> <br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>