[Agda] installing agda

[Andrea Amantini]

Dear Ingo,

> 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.
And probably just the notebook model and Agda evaluation are not really made for each other :-)

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.

glad to share more if you like,

Andrea