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:
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 220.127.116.11, standard-library 2.0, cubical 0.6, agda-categories 0.2.0
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 identifying data is recorded. Please notify me with any security concerns you discover.
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 (1.7 GiB, also see 1.3 GiB minimal image without Firefox and with less firmware) and run it as a virtual machine using, for instance, VirtualBox. Albeit a bit heavy, this is a fast way to get going.
Simply direct your favorite VNC viewer to the address
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:
websocat --binary tcp-l:127.0.0.1:5901