COMP 360-1: Computer-Checked Programs and Proofs

Office Hours

Dan: Thursday, 2:30pm-3:30pm, Exley 633
Joomy: Monday, 7pm-8:30p, Exley 109
Max: Wednesday, 7pm-8:30p, Exley 137

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

1. Install the Haskell programming language.
   • On a Mac, you can install Haskell for Mac OS X. If you have El Capitain, get GHC 10.7.1, and then follow the instructions at the above link (the GHC 10.7.2 version seems to have some problems with the new Mac OS).
   • On Windows or Linux, install the Haskell Platform.
2. With Haskell, you should get the cabal tool for installing Haskell packages Use cabal to install Agda.
   1. You may need to add this to your path if the Haskell installer doesn't successfully do it. On a Mac, it will probably be in /Applications/ghc-10.7.XXX.app/Contents/bin.
   2. Run cabal update to get the latest package list.
   3. Run cabal install Agda. This will install a bunch of libraries that Agda depends on, and then Agda itself. If you get an error about missing happy or alex, type cabal install happy or cabal install alex.
   4. When you're done, you should be able to do

      % agda --version
      Agda version 2.4.2.x
      

      If the cabal install agda finished but this doesn't work, that means your cabal-installed executables are not in your path.
3. Install some version of emacs, if you don't already have it (see the directions below). 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")))
   

Issues and workarounds:

• 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 specific.)
• 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.

Text Editors

Emacs

If you have Linux, you almost certainly have emacs installed. For Mac and Windows get:

• GNU emacs for Mac OS. To make it so that opening emacs by clicking on it works properly, in emacs type Control-x Control-f to open a file, and then type ~/.emacs. Copy in the following code, save, and restart.

  (defun set-exec-path-from-shell-PATH ()
    (let ((path-from-shell (replace-regexp-in-string
                            "[ \t\n]*$"
                            ""
                            (shell-command-to-string "$SHELL --login -i -c 'echo $PATH'"))))
      (setenv "PATH" path-from-shell)
      (setq eshell-path-env path-from-shell) ; for eshell users
      (setq exec-path (split-string path-from-shell path-separator))))
  (when window-system (set-exec-path-from-shell-PATH))
  

• GNU emacs for Windows

Some emacs resources:

• Start with this tutorial on getting started with emacs
• 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.
• The emacs wiki is the omnibus resource for emacs usage
• Wikipedia has an article on the general history and culture of emacs, for the curious.