[Agda] Good old times... (install trouble)

[Nils Anders Danielsson]

On 2009-02-15 12:53, Pierre Hyvernat wrote:

> Installing Agda seems to require a PhD from Chalmers.
> Something should be done about that...

Thanks for letting us know about your problems. We do strive to make
Agda easy to install; mainly by providing precompiled packages, though.
(However, we are still waiting for someone to package Agda for MacOS.)

> Using the precompiled packages didn't work either...

Why? A bug report would be helpful.

> Anyway, after cleaning my Haskell installation, I had to install:
> 
>  [many packages]

If you decide to install manually, then I suggest that you use
cabal-install, which automatically downloads and installs prerequisites
for you. If you have installed recent versions of darcs, GHC, Alex and
Happy, then running the following commands should hopefully be enough (I
have not tested the commands thoroughly, though):

  wget http://www.haskell.org/cabal/release/cabal-install-0.6.0.tar.gz
  tar xzf cabal-install-0.6.0.tar.gz
  cd cabal-install-0.6.0
  . bootstrap.sh
  cd ..
  darcs get --partial http://code.haskell.org/Agda
  cd Agda
  ~/.cabal/bin/cabal install

Then you can install the Emacs mode or the command-line program,
depending on your preferences.

> (There was a warning:
> Warning: This package indirectly depends on multiple versions of the
> same package. This is highly likely to cause a compile failure.
> package haskell98-1.0.1.0 requires process-1.0.0.0 package Agda-2.1.3
> requires process-1.0.1.1)

This is a GHC problem. I think that the problem could have been avoided
by using cabal-install.

> Except that it didn't work... Trying to load even the simplest file
> under emacs freezes emacs (which starts using 80% of my CPU).

My guess is that GHCi has died because of the problem above, with Emacs
still waiting for output from GHCi.

>   what about a minimal Agda2, something like a beefed-up agda-core /
>   agda-light, something like Haskell98 with minimal dependencies,
>   something which could be distributed independently, something we can
>   prove things about, something ... elegant?

It would be nice to have a well-understood core theory, which full Agda
could be compiled into. Preferably with a type-checker written in Agda
itself (using some form of stratification to avoid circularity).
However, this is a separate issue.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.