Installing Agda 2.5.4.1 on Windows 10

I plan to go through the CS410 2017 Agda course. This is how I installed Agda on my Windows machine.

I decided to go through the “use Cabal to compile the Agda package from Hackage” route.

Preliminaries

• The Haskell Platform for Windows version 8.4.3, the Core installer not the Full one. I went with the default options, Stack and all, even as I only intended to use Cabal.
  The Cabal store of compiled packages is located for me at ~\AppData\Roaming\cabal\store\ghc-8.4.3\.
• Git for Windows, just to have access to the Git Bash shell.
• Emacs 26.1, downloaded from here.
  It seems that, unless a HOME variable is specified, the configuration file is expected to be ~\AppData\Roaming\.emacs.

Compilation

I performed the compilation inside Git Bash.

First I updated the Cabal package index with

cabal update

Then I started to compile Agda with

cabal new-install Agda

and went to take a long walk.

cabal new-install has options like bindir and symlink-bindir to control the output directory of the generated binaries, but they weren’t working very well. Once the compilation finished, I had to go the Cabal package store mentioned earlier and into the Agda subfolder, and copy the executables found there to some other place.

Setting up the Emacs mode

This didn’t work:

agda-mode setup

But editing the .emacs file manually did work:

(load-file (let ((coding-system-for-read ‘utf-8))
(shell-command-to-string “agda-mode locate”)))

Remember to use the correct config file location; it might be the one in AppData.

Installing the standard library

I cloned tag v.0.16.1 of this repo. and then followed the instructions here.

I created a ~/AppData/Roaming/agda/ folder with two files, named libraries and defaults.

The content of libraries is

full-path-to-the-cloned-agda-stdlib-repo/standard-library.agda-lib

The contents of defaults is

standard-library

Some basic smoke tests

I created a Foo.agda file with a dumb import and a dumb data definition

module Foo where

import IO.Primitive

data Foo : Set where

After loading it in Emacs and typing C-c C-l, we get this glorious semantic highlighting:

The TeX/LaTeX commands for entering Unicode characters also seem to work. Like writing \lambda for λ.

Compiling using the GHC backend

I tried to compile the “Hello, world” example described here:

agda --compile HelloWorld.agda

but I encountered the following error:

MAlonzo\RTE.hs:11:1: error:

Could not find module `Numeric.IEEE’

Use -v to see a list of the files searched for.

I got around it by creating a .cabal file containing a dummy library stanza like this

library
build-depends: base >=4.11 && <4.12, ieee754 == 0.8.0, text
default-language: Haskell2010

Building it with

cabal new-build

will create an .ghc.environment file with a view of the global store in which ieee754 and text are both present (is there a simpler way to generate the environment file?)

Now we can use cabal new-exec to make the compiler aware of ieee754:

cabal new-exec -- agda --compile HelloWorld.agda

Solving Unicode slowness

After entering some Unicode mathematical symbols (like \top or \bottom) for some reason Emacs slowed down noticeably and became unresponsive.

It tried the solution mentioned here of adding

(setq inhibit-compacting-font-caches 1)

To the .emacs file and it appears to work.