Programming and Proving in Agda, OPLSS 2013
|
|
Dan Licata |
Ian Voysey |
drl+www at cs.cmu.edu |
i...@andrew.cmu.edu |
Course Materials
-
Lecture notes (final)
-
Code for Friday's lecture/hands-on session:
[tgz]
-
New files for Saturday's lecture/hands-on session:
new files only [tgz].
You should unzip this on top of your code from yesterday: it has the
same directory structure, and assumes the files from yesterday will
exist. This zip only contains new files, so it shouldn't overwrite any of
your code, but it can't hurt to use tar --keep-old-files in case I made a mistake.
Or get
lecture/Lecture2Start.agda,
lecture/Lecture2Finish.agda,
lecture/ExtrinsicBoth.agda,
lecture/IntrinsicWellRed.agda,
handson/Lab1Sol.agda,
handson/Lab2.agda
-
New files for Monday's lecture/handson:
lecture/Lecture3Start.agda,
lecture/Lecture3Finish.agda,
handson/Lab2Sol.agda,
handson/Lab3.agda [data description languages],
handson/Lab3-LR.agda [logical relations]
-
New files for Tuesday's lecture/handson:
lecture/Lecture4Start.agda,
lecture/Lecture4Finish.agda,
handson/Lab4.agda,
handson/Lab3Sol.agda [note: this is used by Lab 4],
handson/Lab3-LRSol.agda.
-
New files for Wednesday's lecture:
lecture/Lecture5Start.agda,
lecture/Lecture5Finish.agda,
PreliminariesHoTT.agda,
handson/Lab5.agda
[programming in HoTT],
handson/Lab5-Circle.agda
[fundamental group of the circle],
handson/Lab4Sol.agda,
handson/Lab5Sol.agda,
handson/Lab5-CircleSol.agda.
- Browse individual Agda files. Make sure to
keep the same directory structure, because Agda is file-system-sensitive.
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:
- 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.
- Use cabal to install Agda.
- Run cabal update to get the latest package list.
- Add $HOME/Library/Haskell/bin to your path, so that the
executables installed by cabal are in your path.
- Run cabal install Agda. This will install a bunch
of libraries that Agda depends on, and then Agda itself.
- When you're done, you should be able to do
% agda --version
Agda version 2.3.2.1
- Install some version of emacs, if you don't already have it. On a
Mac, I use Carbon Emacs, but Aquamacs should also work.
- 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")))
- 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:
- Create a file named agda.bat with the following text
chcp 65001
"c:\wherever\your\agda\is\installed\agda.exe" %*
- Tell emacs to use this file to run agda by
- open an Agda file (otherwise, the variable will are about to
edit will not be available)
- type M-x customize-variable and hit enter
- type agda2-program-name
- change the value of the field to the path to the .bat file you made
(C:\...\agda.bat)
- Apply and save.
- Restart emacs and try again.
If you can't get this to work, let us know!
Other Agda Documentation
|