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

[Anton Setzer]

Pierre Hyvernat wrote:
> Greetings to all...
>
>
> Short version:
>
> Installing Agda seems to require a PhD from Chalmers.
> Something should be done about that...
>
>
>
>   

Please feel free to update the Agda Wiki (including pages
originally created by me) with anything
you have learned (even if you failed to get the whole thing
running).

Anton
> 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
>   


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------