The Windows Subsystem for Linux (WSL) more or less runs a linux kernel on Windows 10. In this post, I will describe how to use WSL to compile and run Agda, a dependently typed functional programming language. Compiling agda yourself makes sense if you want to use the latest features, of which there are quite nice ones. The approach presented here is just my preferred way of compiling and using Agda on a Linux system with some minor adjustments.
Prerequisits for compiling
First, you need the “ubuntu app”, you can install it following this guide. Essentially, you just have to activate WSL and install the app through the Microsoft Store, but following the guide step by step allowed me to do it without creating a Microsoft account.
After installing your ubuntu app will ask you to create a new account and it will probably need some updating, which you can do by running:
sudo apt-get update
A usability hint: You can copy-paste to the ubuntu app by copying with CTRL-C and right-clicking into the ubuntu-window. You have to make the ubuntu-window active before the right-click. You can copy stuff in the ubuntu-window by marking and pressing CTRL-C.
There are two tools that can get the dependencies and compile Agda for you, “cabal” and “stack”. I prefer to use stack:
https://docs.haskellstack.org/en/stable/README/
After installing, stack asked me to append something to my PATH, which I did only for the session:
export PATH=$PATH:/home/USER/.local/bin
Getting the sources and compiling
Git is preinstalled, so you can just get the agda sources with:
git clone https://github.com/agda/agda.git
Go into the agda folder. It will contain a couple of files with names like
stack-8.8.1.yaml
These are configuration files for stack. The numbers indicate the version of ghc (the haskell compiler) that will be used. I take always the newest version (if everything works with it…) and make a copy
cp stack-8.8.1.yaml stack.yaml
– since stack will just use the “stack.yaml” for configuration when run in a folder. Now:
stack setup
will download ghc binaries and install them somewhere below “HOME/.stack/”. Before building, we have to install a dependency (otherwise there will be a linker error with the current ubuntu app):
sudo apt install libtinfo-dev
Then tell stack to build and hope for the best (that took around 5.2GB of RAM and half an hour on my system…):
stack build
On success, it should look like this:
If you are not confident with finding the locations from the last lines again, you should secure the path from the last lines. We will need “agda” and “agda-mode”, which are in the same folder.
Using Agda
Of course, you can use agda from the command line, but it is a lot more fun to use from emacs (or, possibly atom, which I have not checked out). Since the ubuntu app does not come with a window system and on the other hand our freshly built agda cannot be invoked easily from windows programs, I found it most convenient to run emacs in the ubuntu app, but use an x-server in windows.
For the latter, you can install Xming and start it. Then install emacs in the ubuntu app:
sudo apt install emacs
Before starting emacs, we should install the “agda-mode” for emacs. This can be done by
./stack/install/[LONG PATH FROM ABOVE]/bin/agda-mode setup
Now run emacs with the variables “DISPLAY” set to something which connects it to Xming and “PATH” appended by the long thing from above, so emacs can find agda (and agda-mode):
PATH=$PATH:~/agda/.stack-work/[LONG PATH FROM ABOVE]/bin/ DISPLAY=:0 emacs
Then everything should work and you can test the agda-mode, for example with a new file containing the following:
CTRL-C, CTRL-L tells agda-mode to check and highlight the contents of the file. Here is more on using the agda-mode. Have fun!
Sources:
Schneide Blog 
By now, one has to use
git clone –recurse-submodules https://github.com/agda/agda.git