Installing Agda
From PBDN
Contents |
Installing Agda
I needed to intall Agda on Ubuntu for the AMD-64 architecture. No binary was available, so I had to build from source.
For x86 machines running Debian or Ubuntu, installing the packages listed below should enable a binary download of Agda to run. However, you may still have problems with your installation: see the Installation section, below for more detail.
Ubuntu/Debian Packages
The configure script does not identify "up-front" the libraries that it requires (as it should). By trial and error, attempting to compile and finding packages to match unresolved dependencies, I found the following packages sufficient (i.e. their dependencies enabled me to build Agda from source):
- ghc6, the Glasgow Haskell Compiler
- libghc6-mtl-dev for the Control.Monad.Reader module (at least)
Although I haven't checked, I would be very surprised if this didn't work for Debian as well.
Building from Source
I then built Agda as directed, but specifying the install prefix, with:
$ ./configure --prefix=/usr/local --enable-newsyntax $ export LANG=C $ make
Agda uses the GNU Autotools build-chain.
Warnings During Build
During the build, I got several warnings. I've got it working, so they appear (so far) to be harmless enough.
The following warnings cropped up during compilation:
Typechecking.hs:50:22:
Warning: {-# SOURCE #-} unnecessary in import of `External'
Alfa/UAbstract.hs:1:44:
Warning: The export item `MetaVar(..)'
suggests that `MetaVar' has constructor or class methods
but it has none; it is a type synonym or abstract type or class
[ 1 of 108] ...
PreStrings.hs:10:306:
Warning: `fsHypTypeVar' is exported by `fsHypTypeVar' and `fsHypTypeVar'
[ 44 of 108] ...
ISyntax.hs:40:10:
Warning: Pattern match(es) are overlapped
In a case alternative: (_) -> ...
[ 56 of 108] ...
CSyntax.hs:308:4:
Warning: Pattern match(es) are overlapped
In the definition of `identifiers': identifiers _ = ...
[ 76 of 108] ...
Typechecking.hs:50:0:
Warning: Unnecessary {-# SOURCE #-} in the import of module `External'
[ 95 of 108]
AgdaPluginKit.hs:2:8:
Warning: `MetaSubst' is exported by `module ProofState' and `module ProofMonad'
AgdaPluginKit.hs:2:8:
Warning: `Constraint' is exported by `module ProofState' and `module ProofMonad'
AgdaPluginKit.hs:2:8:
Warning: `Constraint' is exported by `module ProofState' and `module ProofMonad'
[104 of 108]
During linking, only one warning was observed, although it didn't list all the steps (presumably, it only does this after the first error or warning, the first warning occurred in step 1, above, causing all of the compilation steps to be listed):
Typechecking.hs:50:22:
Warning: {-# SOURCE #-} unnecessary in import of `External'
[31 of 81]
Testing
Usually, packages using GNU Autotools have a check make target, so I tried:
$ make check
— even though the Agda compilation page doesn't mention it. Unfortunately, the tests seem to be broken and make check fails on the first test.
Installation
I proceeded with a make install and noted that it installs emacs elisp files providing an Agda mode for editing (presumably with syntax-highlighting, etc.) Agda files.
Unfortunately, there are four problems with the installation:
- Incorrectly installs agda-mode.el and its two supporting files to /emacs/site-lisp rather than $prefix/share/emacs/site-lisp
- Incorrectly sets all execute bits on those files
- Fails to set the correct permissions on emacsagda-070924
- Uses deprecated functionality from cl-extra.el
To fix these problems:
Move *.el from /emacs/site-lisp to /usr/local/share/emacs/site-lisp, fix the permissions, and patch agda-mode.el as follows (ignoring the MediaWiki "offsite link" icon in the second-last line):
$ sudo mv /emacs/site-lisp/*.el /usr/local/share/emacs/site-lisp $ sudo rmdir /emacs/site-lisp /emacs $ sudo chmod 644 /usr/local/share/emacs/site-lisp/*.el $ sudo chmod 755 /usr/local/lib/EmacsAgda/bin/emacsagda-* $ wget -P /tmp http://polacksbacken.net/pub/ecam.patch $ sudo patch /usr/local/share/emacs/site-lisp/agda-mode.el < /tmp/ecam.patch
If you don't want to (or can't) obtain and apply the patch using the last two lines above, you can apply the patch manually or copy and paste it into a text editor:
--- agda-mode.el~ 2007-09-24 18:19:53.000000000 +0200 +++ agda-mode.el 2007-09-24 20:13:20.000000000 +0200 @@ -87,6 +87,10 @@ (or (fboundp 'cl-simple-expr-p) (load "cl-macs")) (or (fboundp 'common-lisp-indent-function) (load "cl-indent")) (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function) +;; Added to fix use of deprecated cl-push and cl-pop further down. EC20070924 +(defmacro cl-push (x place) (list 'setq place (list 'cons x place))) +(defmacro cl-pop (place) + (list 'car (list 'prog1 place (list 'setq place (list 'cdr place))))) (require 'comint) (require 'font-lock) (require 'haskell-mode)
Emacs Mode
I enabled autoloading of Agda-mode by adding the following to my .emacs file.
(autoload 'agda-mode "agda-mode.el"
"Major mode for Agda files" t)
(unless (assoc "\\.agda" auto-mode-alist)
(setq auto-mode-alist
(nconc '(("\\.agda" . agda-mode)
("\\.alfa" . agda-mode)) auto-mode-alist)))
Running
Having done all of the above, I was able to type the following successfully:
$ emacs first.agda
This caused emacs to start with the split window described in the Agda tutorial, and I was able to start with the tutorial.