COMP 360-1: Computer-Checked Programs and Proofs

Office Hours

Tuesday, noon to 1pm and Wednesday, 11am-noon and by appointment

Piazza

We will use Piazza for questions about the assignments, for students to discuss course materials, and to make announcements about the class. You are responsible for being current with the information and discussions that are posted there.

You will get an email from Piazza with a link inviting you to create an account within the first week of the term. If you haven't gotten one in that time, please contact course staff.

In addition to the web interface, there are Piazza apps for Android and iOS available for free through their respective app stores.

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. Run cabal install Agda. This will install a bunch of libraries that Agda depends on, and then Agda itself.
   3. Add $HOME/Library/Haskell/bin (on a Mac) or $HOME/.cabal/bin (on Linux) or ? (on Windows) to your path, so that the executables installed by cabal are in your path.
   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")))
   

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: If you have a problem with agda-mode setup not finding your 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: you may need to download some additional fonts in order to get certain Unicode characters (like \[[, for example). For example, DejaVu Sans should work.
• Windows: If you have a problem where the agda executable works at the command line, but agda interaction does not work in emacs---for example, after refining, goals don'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.

GNU emacs

The guiding principle of emacs philosophy is that you should never have to leave emacs to preform a task if you don't want to. If you're writing C, it can run your makefile, and show you GDB output internally. It even has tetris and email clients built in. Despite being extremely large in this sense, emacs scales down to the smallest of text files elegantly.

The most sane version to use is GNU emacs, although both GNU emacs and Xemacs are installed on the Andrew UNIX machines. There's a ton of good documentation for how to use it available on the web, some of which is linked here.

• Wikipedia has an article on the general history and culture of emacs, for the curious.
• One of many bare-bones tutorials on getting started with emacs
• The emacs wiki is the omnibus resource for emacs usage
• To exit emacs, type Control-X, then Control-C. A prompt may appear asking you about saving any changes you made; if this happens, you will need to answer it before exiting.

LaTeX

If we have written assignments, you may wish to use LaTeX.

LaTeX is built from Don Knuth's TeX typesetting language, and has grown through community support to be both extremely powerful and easy to use. LaTeX is installed on the Andrew UNIX servers, and can be downloaded and installed on local machines as well. There are any number of excellent resources about how to use LaTeX; a few are listed here for your convenience.

• The Wikipedia page, for more general information and history
• The excellent 251 LaTeX wiki page.
• The Wikibook on LaTeX
• A (Not So) Short Introduction To LaTeX2e
• The Comprehensive TeX Archive Network (users group)
• The TeXLive Homepage
• detexify is a learning-based symbol classifier that will help you figure out the right LaTeX command to produce a symbol you can draw but not name.

LaTeX source files can be created with any text editor, so emacs and vim are excellent choices. There are several LaTeX specific IDEs that you may find more comfortable to use, depending on your working environment:

• kile, the KDE LaTeX IDE
• TeXworks
• TeXclipse, an Eclipse plugin for LaTeX
• TeXnicCenter, an IDE for Windows