Programming and Proving in Agda, OPLSS 2013

    
Dan Licata Ian Voysey
drl+www at cs.cmu.edu i...@andrew.cmu.edu

Course Materials

Getting Agda

Please try to install Agda version 2.3.2.1, which is the latest stable release, but the course materials will likely work with other recent versions (2.3.2, the development version from darcs) if for some reason those are easier to install. We recommend trying to install Agda according to the following directions:
  1. Install the Haskell Platform. The latest version, 2013.2.0.0, will definitely work for Agda 2.3.2.1, though other versions may also work. This is available for Windows, Mac OS, and Linux.
  2. Use cabal to install Agda.
    1. Run cabal update to get the latest package list.
    2. Add $HOME/Library/Haskell/bin to your path, so that the executables installed by cabal are in your path.
    3. Run cabal install Agda. This will install a bunch of libraries that Agda depends on, and then Agda itself.
    4. When you're done, you should be able to do 
      % agda --version
Agda version 2.3.2.1
  3. Install some version of emacs, if you don't already have it. On a Mac, I use Carbon Emacs, but Aquamacs should also work.
  4. Run agda-mode setup to add Agda to your emacs configuration. If, for some, reason agda-mode setup fails, you can add the following lines to your .emacs manually: 
    (load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
  5. Get the course material below and open an Agda file.

If that fails, more information is available here. For Agda 2.3.2.1, there are some pre-built packages for linux distributions, but do not use the Windows installer (it is out of date), and there is no pre-built package for Mac. If you do not install Haskell using the Haskell Platform, then watch out for this performance issue with the hashtable package: make sure you get hashtable version 1.1.2.x (the Haskell Platform has an appropriate version).

Issues and workarounds:

  • Mac OS 10.6.8: If cabal install Agda leads to an error like 
    cabal: Error: some packages failed to install:
Agda-2.3.2.1 failed during the building phase. The exception was:
ExitFailure 11
    then you may have better luck with cabal install --global Agda-executable
  • Ubuntu 13.04: The Haskell platform is not packaged. Get Agda 2.3.2 by doing sudo apt-get install agda-mode.
  • Windows: Several people had a problem with agda-mode setup not finding their install of emacs on Windows. If you have followed the above directions to the point where agda-mode and agda are in your %PATH%, you can manually edit your ~/.emacs to include the text mentioned above 
    (load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
    Note that emacs seems to resolve ~ correctly, in that if you do C-c C-f to open a file and type in ~/.emacs, emacs will later find the definitions in that file. (It actually puts the file somewhere bizarre that's os / emacs / phase of the moon dependent.)
  • Windows: many people had a problem where the agda executable worked at the command line, but agda interaction did not work in emacs---for example, after refining, goals didn't appear. A solution is as follows:
    1. Create a file named agda.bat with the following text 
        chcp 65001
  "c:\wherever\your\agda\is\installed\agda.exe" %*
    2. Tell emacs to use this file to run agda by
      1. open an Agda file (otherwise, the variable will are about to edit will not be available)
      2. type M-x customize-variable and hit enter
      3. type agda2-program-name
      4. change the value of the field to the path to the .bat file you made (C:\...\agda.bat)
      5. Apply and save.
      6. Restart emacs and try again.
If you can't get this to work, let us know!

Other Agda Documentation