Looking for the notes of the 2024 Verona course on extracting programs from proofs? Here
Similar projects for other languages: Coq • Lean 4 (with their Natural Number Game) • Minlog
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.7.0, standard-library 2.1.1, cubical 0.7, agda-categories 0.2.0, 1lab 7cc9bf (because of naming conflicts, you need to manually add 1lab to ~/.agda/defaults in order to use it), functional-linear-algebra 0.5.0, generics 1.0.1.
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 identifying data is recorded. Please notify me with any security concerns you discover.
A NixOS package for self-hosting this server is available here (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 (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.
Contact
Ingo Blechschmidt
iblech@speicherleck.de
+49 176 95110311
Using a native VNC viewer
Simply direct your favorite VNC viewer to the address
wss://agdapad.quasicoherent.io/__vnc/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:
- Run
websocat --binary tcp-l:127.0.0.1:5901 wss://agdapad.quasicoherent.io/__vnc/SessionName. - Direct your VNC viewer to
localhost:1.