Agda is a dependently typed functional programming language and a proof assistant. You can also use a native VNC viewer instead of this in-browser viewer. Learn more about this project. This online version of Agda was made by Ingo Blechschmidt for an Agda course at the University of Padova, building on awesome free technology:

About Agdapad

This page connects you to a remote server on which an Emacs instance is spawned for you. The purpose of Agdapad is to lower the bar for playing with Agda and its standard library, as local installation becomes superfluous, and to allow live collaboration on small Agda projects. Agdapad was built to facilitate an Agda course at the University of Padova.

Versions installed on the server: Agda 2.6.1, standard-library 1.3, cubical 0.2, agda-categories 5a49c6

Server concerns

In case of connection problems, try reloading the page. You will be able to continue where you left off.

The server is not very well-equipped, hence please be mindful of your resource usage. You do not need to quit Emacs when leaving this page, but please do terminate Agda or quit Emacs in case Agda is taking an extraordinate amount of time.

This service is provided free of charge and comes without any guarantees. It might vanish at any point. Your Agda programs are stored on the server, unencrypted, but no personal data is recorded. Please notify me with any security concerns you discover.

A NixOS package for self-hosting this server will be available in the next couple of days (AGPL-licensed). You can also access this server using a native VNC viewer.

Installing Agda on your local computer

For larger experiments, Agda is more fun if you install it locally on your computer. Instructions are available at the Agda wiki. Unfortunately the installation process it not entirely straightforward, especially on Windows. For this reason you can also download an “all batteries included” system image and run it as a virtual machine using, for instance, VirtualBox. Albeit a bit heavy, this is a fast way to get going.

Contact

Ingo Blechschmidt
iblech@speicherleck.de
+49 176 95110311
Arberstr. 5
86179 Augsburg
Germany

Using a native VNC viewer

Simply direct your favorite VNC viewer to the address wss://agdapad.quasicoherent.io/SessionName.

However, most VNC clients do not support the WebSocket protocol, the noVNC client being a notable exception. Hence you need to setup a TCP proxy; on Linux, websocat (packaged for most Linux distributions) can do this for you:

  1. Run websocat tcp-l:127.0.0.1:5901 wss://agdapad.quasicoherent.io/SessionName.
  2. Direct your VNC viewer to localhost:1.