[Agda] installing agda

[Ingo Blechschmidt]

Dear Andrea,

On Sat 30 Jan 2021 06:14:11 PM GMT, Andrea Amantini wrote:
> > On each request, a lightweight container is
> > spawned which the browser communicates with using the VNC protocol.
> > There are some optimizations with pre-starting containers so that
> > loading time is minimized.
> 
> yeah, that’s very nice. Glad you saw our PLFA (which I need to
> update), did you try that out for teaching? As I wrote, our
> interaction with the typechecker a bit limited and some user might be
> deceived by that.

yes, I like the notebook integration very much :-)

I didn't try Nextjournal for teaching -- for my course I wanted the full
Emacs experience and the collaborative aspect of people sharing the
same Emacs window.

> The “nice” part is that the top module you need to define in our
> notebooks is actually dumped to a file by the python kernel, so when
> you export a runtime (actually a docker commit) you actually can
> re-import your module in other notebooks.

Yes, that is very nice!

I guess the two approaches are nicely complimentary. :-)

Cheers,
Ingo