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

[Pierre Hyvernat]

Greetings to all...


Short version:

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




Long version:

After a long time, I decided to try to actually install a recent version
of Agda, and after a looong afternoon, I gave up.

I'll probably try again in a couple of days, taking notes about my
problems to try to solve them (and post the important ones here).


Part of the problem comes from the fact that Agda and Haskell (ghc)
seem to be evolving really fast. This is a good thing.
(Several colleagues of mine have tears coming when they remember the
time when Caml came before Haskell in the "computer language benchmark
game".)

The result is that the dependencies are a PITA to get right.  For
example, in the darcs version of Agda, we need "quickcheck-2.1.0.1".



Reading Anton's guide "Installation of Agda from Source for
Non-Programmers", I wondered if the title was ironic or not...


Anyway, after cleaning my Haskell installation, I had to install:

 - binary-0.4.4,
 - Cabal-1.6.0.1,
 - extensible-exceptions-0.1.1.0,
 - haskeline-0.3.2,
 - process-1.0.1.1,
 - QuickCheck-2.1.0.1,
 - stm-2.1.1.2,
 - terminfo-0.3.0.1,
 - utf8-string-0.3.4,
 - xhtml-3000.2.0.1,
 - zlib-0.4.0.4.

(It does look horrifying...)

I was then finally able to successfully compile Agda-2.1.3. (Using the
official "runhaskell Setup.hs configure && runhaskell Setup.hs build &&
sudo runhaskell Setup.hs install")

(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)


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

I did try using an older emacs-mode, without success.

I then tried compiling agda-2.1.2, and even after modifying the
Agda.cabal file to accommodate for some changing in the packaging of
some libraries.
I gave up after another hour.



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


I could have compiled my own version of ghc to remove the warning above,
but I simply don't want to.



Now, I don't consider myself a Haskell hacker, and I haven't been
following what's happening in the Haskell community; but I really take
failing to install Agda2 on a fairly traditional and recent Unix
system (Debian unstable) as a personal failure and a step back
compared to the old agda1.



I know it's been discussed in the past, but it got me thinking...

I over-simplify a bit, and am voluntarily provocative, but:

  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?


I really think there should be 3 levels (or more):
 - minimal core (dependent products, inductive types, dependent
   records, ...)
 - "advanced features" (coinduction, sized-types, ...)
 - interface (compilation, strong optimization, line editing,
   Unicode...)

(The level 2 and 3 aren't necessarily in that order.)


A good deal of the library should only depend on the first level, if
only because it is supposed to be rock-solid and stable.
The rest is nice for:
 - research projects
 - actual real life programming



All of this is mainly wishful thinking, as I probably won't have much
time to devote to any agda-implementing stuff, but I surely would
like a move in this direction...



Comments?



Pierre
-- 
God may be subtle, but he isn't plain mean.
    -- Albert Einstein