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