<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Dear All,</div><div class=""><br class=""></div><div class="">we’re hosting online Agda notebooks on nextjournal which you can try out at</div><div class=""><br class=""></div><div class=""><a href="https://nextjournal.com/try/agda" class="">https://nextjournal.com/try/agda</a></div><div class=""><br class=""></div><div class="">and it’s an installation-free solution as well. We have a default environment with atm Agda 2.6.1.2 + standard library version 1.4.</div><div class="">You can build your own custom environments in the platform itself, since these are also built in notebooks. Check how Cubical library is installed</div><div class=""><br class=""></div><div class=""><a href="https://nextjournal.com/nextjournal/agda-environment#cubical-agda-%E2%9D%92" class="">https://nextjournal.com/nextjournal/agda-environment#cubical-agda-❒</a></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Our typechecking is based on a Jupyter Kernel and as such is limited to a subset of the whole emacs mode interaction (rudimentary hole goal inspection and Auto/Split/Refine).</div><div class="">So our approach rather focused on literate programming and ease of sharing and reusing notebooks, some of our users use notebooks for teaching. I’ll be glad to share more facts if you need.</div><div class=""><br class=""></div><div class="">Ingo’s solution is indeed amazing as I guess delivers a 1:1 emacs experience right?</div><div class=""><br class=""></div><div class="">Cheers,</div><div class="">Andrea</div><div class=""><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">On 30. Jan 2021, at 15:32, Manuel Bärenz <<a href="mailto:manuel@enigmage.de" class="">manuel@enigmage.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class=""><br class=""><blockquote type="cite" class="">In case there are still installation difficulties, you might want to<br class="">check out the online version of Agda at<br class=""><br class=""> <a href="https://agdapad.quasicoherent.io/" class="">https://agdapad.quasicoherent.io/</a>.<br class=""></blockquote><br class="">This is fantastic! What software is this? Can it be embedded easily in<br class="">an existing page?<br class=""><br class="">How about making an "official" server that is linked from the agda docs?<br class="">It would be great to have this linked so beginners find it quickly.<br class=""><br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></div></blockquote></div><br class=""></body></html>