[Agda] Introducing Agdapad, a website for real-time collaborative Agda experiments (early preview)

Ingo Blechschmidt iblech at speicherleck.de
Mon Apr 27 22:35:45 CEST 2020


Dear friends of Agda,

I'm happy to announce Agdapad: like Etherpad or Ethercalc, but for Agda.

    https://agdapad.quasicoherent.io/

The purpose of Agdapad is to lower the bar for playing with Agda, as
local installation becomes superfluous, and to allow live collaboration
on small Agda experiments.

I'm building Agdapad to facilitate a first course on Agda which I'm
teaching at the invitation of Milly Maietti in Padova. Accordingly it is
intended for short programs and presentations; it is not suitable for
large developments.

* This is an early preview. I appreciate your thoughts on how Agdapad
  could be made more useful for your purposes. Already on my to do list
  is a text-only mode, which should make Agdapad more accessible on
  connections with low bandwidth. Over the next couple days, I'll clean
  up the source and then put it online (AGPL-licensed) so that people
  can self-host Agdapad.

* Agdapad comes without any guarantees. It might vanish at any point.
  Do not rely on it. In particular, since the host on which Agdapad runs
  is rather underpowered, I might need to restrict access when I need it
  for my own course.

* Have fun and feel invited to play with Agdapad in any way you see fit!
  Agda is a truly amazing and captivating game, conveying so many
  insights. This real-time collaborative extension hopefully
  increases its charm even more.

I'm grateful to Martín Escardó and Anja Petković, with whom I took my
my first steps with Agda.

Cheers,
Ingo


More information about the Agda mailing list