Installing Agda 2.4.2 on Windows 7 and 8
2014-10-22 Updated from
Installing Agda 2.3.2 on Windows 7
November 25, 2013
Aaron Stump These notes are based on my experience installing Agda on a Windows 7 computer. I have not tried this yet for Windows 8. The notes below do not assume you know anything about Haskell, emacs, Windows command shell, or Agda.
I. Installing Agda and emacs
1. Download the Haskell Platform for Windows from
http://www.haskell.org/platform/
and run the installer. Haskell wants to install itself to C:\Program Files (x86)\Haskell Platform\2014.2.0.0 This should be fine.
The installer will also ask you want kind of installation you want. The "standard" installation is fine.
Once the installer finishes, it will ask you if you want to install GLUT on your computer. GLUT is a Haskell library for doing graphics with Open GL. Agda does not need GLUT, so you can decline.
2. Open a Windows command shell from the Start Menu, by typing "cmd" in the box which lets you search for files and programs, and hitting enter.
3. From the Windows command shell, first run
cabal update
Next run
cabal install Agda
This 'cabal' program is a package manager for Haskell. Running 'cabal install Agda' will download the Agda source code from hackage.haskell.org, a central server where Haskell libraries and programs are posted. Cabal will also download compile and additional Haskell packages needed by Agda.
3'. Depending on your system locale setting, the previous Step 3 may fail with error messages like
cpphs: src/full\Agda\Interaction\BasicOps.hs: hGetContents: invalid argument (invalid byte sequence)
cabal: Error: some packages failed to install:
Agda-2.4.2 failed during the building phase. The exception was:
ExitFailure 1
If this happens, you can try changing the system locale to English(US) following the instruction here. After Step 3 succeeds, the system locale should be changed back to the orginal locale.
3''. It's also possible that previous Step 3 fails with message like
Failed to install Agda-2.5.3
Build log ( C:\Users\user\AppData\Roaming\cabal\logs\ghc-8.2.1\Agda-2.5.3-9MnddGMG90dKhOoB0RHfaX.log ):
cabal: Entering directory 'C:\Users\USER\AppData\Local\Temp\cabal-tmp-9660\Agda-2.5.3'
[1 of 1] Compiling Main ( C:\Users\USER\AppData\Local\Temp\cabal-tmp-9660\Agda-2.5.3\dist\setup\setup.hs, C:\Users\USER\AppData\Local\Temp\cabal-tmp-9660\Agda-2.5.3\dist\setup\Main.o )
Linking C:\Users\USER\AppData\Local\Temp\cabal-tmp-9660\Agda-2.5.3\dist\setup\setup.exe ...
Configuring Agda-2.5.3...
setup.exe: The program 'cpphs' version >=1.20.8 is required but the version
found at C:\Users\user\AppData\Roaming\cabal\bin\cpphs.exe is version
1.20.2
cabal: Leaving directory 'C:\Users\USER\AppData\Local\Temp\cabal-tmp-9660\Agda-2.5.3'
cabal: Error: some packages failed to install:
Agda-2.5.3-9MnddGMG90dKhOoB0RHfaX failed during the configure step. The
exception was:
ExitFailure 1
If that happens, run `cabal install cpphs` and try Step 3 again.
4. Download emacs version 25.3 from
http://ftp.gnu.org/gnu/emacs/windows/
The file is at the bottom of the page:
emacs-25.3-bin-i686.zip
This is currently the latest version, although the specific version likely does not matter too much.
At least one person encountered some troubles running `x86_64` version of Emacs on their Windows 7 x64, reverting back to `i686` version helped.
4'. (Japanese users who uses IME may do better with emacs-23.4-20120527.exe distributed from here.)
5. When the download is complete, extract the downloaded .zip file, by right-clicking on it, and choosing "Extract All...". As the destination for emacs, I chose
C:\Program Files (x86)
The extraction process will create a folder emacs-25.3 in that directory.
6. When the extraction process has completed, navigate to
C:\Program Files (x86)\emacs-25.3\bin
and double-click on the addpm program. This program will add emacs to the Start menu.
7. To complete the installation of the Agda emacs mode, we must next add emacs to the Windows path. To do this, right-click on the icon for your computer within Windows Explorer, and select Properties. Then click "Advanced system settings". This will pop up yet another window, with the Advanced tab highlighted. Click on "Environment Variables...", and then request to edit the PATH variable. In the text box for the PATH variable, append ";C:\Program Files (x86)\emacs-25.3\bin" (including the semicolon) to whatever text you see there (if blank, you presumably do not need the semicolon).
8. Close your existing Windows command shell, and start a new one (as in Step 2 above). This is to refresh the PATH variable now that we have changed it (Step 7).
9. From the new Windows command shell, run
agda-mode setup
This should finish almost instantly, with a message saying something about "Setup done. Try to (re)start Emacs..."
II. Installing extra fonts and configuring Agda
10. We need to install some extra (free) fonts for Agda to show Unicode more nicely. Go to
https://dejavu-fonts.github.io/Download.html
11. From the new page that comes up, select "dejavu-fonts-ttf-2.37.zip" from the list of download options (you need "TrueType fonts packed as zip archive").
12. When the download completes, open the .zip file by double-clicking on it from Windows Explorer. Navigate to the dejavu-fonts-ttf-2.37\ttf subdirectory.
13. Double-click on "DejaVuSans". This will pull up a font viewer window.
14. Click on "Install". This will install the DejaVuSans font on your computer.
If you also want monospaced font, repeat steps 13-14 with DejaVuSansMono.
15. We need to tell emacs to use the new font. To do this, run emacs (you can just select it from the Start menu), and then type
Control-x Control-f
This is the emacs "open file" command. A little text box will appear at the very bottom of the emacs window. Type
~/.emacs
into that text box, and hit enter. This will open your .emacs file, a file that the emacs program processes for your user settings, every time emacs starts up.
Cut and paste the following text into your .emacs file, to tell emacs about the new font:
(set-default-font "-outline-DejaVu Sans-normal-normal-normal-sans-*-*-*-*-p-*-iso8859-1")
If you'd like monowidth font and/or simpler looking line:
(set-default-font "DejaVu Sans Mono")
16. [Optional] If you are using the standard library, download that separately (from the Agda wiki) and put it somewhere. Then cut and paste the following into your .emacs file:
(custom-set-variables
'(agda2-program-args (quote ("-i" "C:/PATH-TO-LIBRARY/src")))
)
Note that you should use forward slashes in the path.
17. Select "Save" from the file menu, or just type
Control-x Control-s
18. Quit emacs.
III. Testing Agda
19. We need to get a sample Agda file to complete the configuration and testing. One example can be downloaded from here:
https://svn.divms.uiowa.edu/repos/clc/class/111-spring14/lib/bool.agda.
20. Right-click on the file and choose "Open". You will get a list of programs that does not include Emacs. Tell Windows that you want to select the program to use from your locally installed programs. You will get a window showing a bunch of programs, not including Emacs. Select "Browse..." and then navigate to
C:\Program Files (x86)\emacs-25.3\bin
and select "runemacs" from the list. Then click "Ok".
21. You will return to the list of programs, but now emacs will be listed. Select it (if not already selected), and tell Windows you always want to open files of this type (.agda) with this program (emacs). Click "ok".
22. Emacs should now open with bool.agda.
23. You should see a file with characters including 𝔹. If you see weird squares with numbers in them, something has gone wrong with the font installation.
24. Now type Control-c Control-l. This tells emacs to ask Agda to process the file. If this works, the text in the bool.agda file should get colored with different colors.
25. Agda installation, configuration, and testing is now complete! You have Agda on Windows, with an extra font for (some) Unicode math symbols.