Code repository for our work on Quantum Pi "How to Bake a Quantum \Pi"
Tested with Agda version 2.6.4.1, stdlib-2.0 and agda-categories 0.2.0. Things should work with 2.6.4.3 as well. Interactive versions have been tested with Emacs 27.2 (on Linux, MacOS and WSL).
You need to install Agda and stdlib-2.0. See Agda installation and Library Management for the standard ways to do this. Warning: if you have not done this before, this can be quite finicky. Please seek the help of someone who has done it before.
For the purposes of these instructions, we will assume as unix-like system (so any flavour of Linux, MacOS X or WSL on Windows) with command-line instructions. Although it appears possible to do things via Visual Studio, we have not tested this in any way.
To check everything, simply do
make
(though this only really does)
agda Everything.agda
at the command line. This should take less than 30 seconds, where the
bulk of the time will be spent checking TestsSlow.agda.
The best entry points is Everything.agda which gives a quick overview
of what is all the files. The basic verification that we can indeed
correctly interpret some quantum circuits are in the modules Tests
and TestsSlow.