[Agda] installing agda

[Andrea Amantini]

Dear All,

we’re hosting online Agda notebooks on nextjournal which you can try out at

https://nextjournal.com/try/agda <https://nextjournal.com/try/agda>

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.
You can build your own custom environments in the platform itself, since these are also built in notebooks. Check how Cubical library is installed

https://nextjournal.com/nextjournal/agda-environment#cubical-agda-❒ <https://nextjournal.com/nextjournal/agda-environment#cubical-agda-%E2%9D%92>


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

Ingo’s solution is indeed amazing as I guess delivers a 1:1 emacs experience right?

Cheers,
Andrea


> On 30. Jan 2021, at 15:32, Manuel Bärenz <manuel at enigmage.de> wrote:
> 
> 
>> In case there are still installation difficulties, you might want to
>> check out the online version of Agda at
>> 
>>    https://agdapad.quasicoherent.io/.
> 
> This is fantastic! What software is this? Can it be embedded easily in
> an existing page?
> 
> How about making an "official" server that is linked from the agda docs?
> It would be great to have this linked so beginners find it quickly.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210130/9f9892f0/attachment.html>