[Agda] Install failure

[Christoph Herrmann]

Hi Bengt

On 23 Mar 2011, at 09:27, Bengt Nordstrom wrote:

> The general situation seem to be that we have a good way to install
> Agda for (experienced) Haskell programmers.

I disagree. The installation problem has nothing to do with
Haskell programming. The skills required are shell, make, m4, configure,
the peculiarities of gcc and libraries on MacOSX (in my case)
and the ability to deal with a vast amount of side effects, which I try
to avoid; that is one reason why I program in Haskell.

> But it would be nice if it was easy for people who (like myself) know
> nothing about cabal, happy etc to install the system.
> As a naive person, I would like to have a one click install for each
> of the major operating systems. How can we achieve this?
> The current descriptions of the process takes more than a page and a
> lot of alternatives.

A one-click install is probably a high effort, but it would be nice if
the installation process was simpler, e.g., avoiding cabal.

> In fact, it would be nice to have a zero click install: You should be
> able to load and edit Agda programs in your browser. Is anybody
> working on this?

This could probably encourage people from mathematics/logics which do
not have a deep programming language background to play with Agda.
I know a few people which are discouraged by the need to use emacs;
and the batch mode is not attractive as well.

Best Regards


> 
> Best regards,
> Bengt
> 
> On Wed, Mar 23, 2011 at 3:47 AM, wren ng thornton <wren at freegeek.org> wrote:
>> On 3/22/11 4:19 PM, gallais @ EnsL.org wrote:
>>> Well, cabal info is still unable to tell me which version of happy I'm using
>> 
>> You should be able to do `which happy` and `happy --version` to find out
>> (depending on how you mean).
>> 
>> Unfortunately, cabal (actually ghc-pkg, IIRC) can't keep track of which
>> executables it's installed, it only keeps track of libraries. But then
>> cabal doesn't strive to be a general package manager for Haskell; it's
>> more of a replacement for gmake, albeit leaning in the direction of
>> package managers.
>> 
>> --
>> Live well,
>> ~wren
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532