[Agda] User-test - starting problems with Agda2

[Nils Anders Danielsson]

On 2009-08-31 09:58, Steffen Bock wrote:
> I have to say some words for getting started with the Agda system.
> Perhaps, this feedback helps the developers improve the system.

Thanks for your feedback. It would be helpful if you could be a bit more
specific, so that we can improve things; see below.

> 1. There are many instructions to install Agda. However one can manage
>    it spending some hours. I mean the install does not take many
>    hours, however to read the instructions, etc.

Are you referring to the instructions on the Agda Wiki? Can you explain
in more detail what the problem is? The "Download" link is easy to find,
and then you can choose instructions depending on which kind of computer
you have. What part of the instructions should be simplified?

> 2. After you have managed the installation, you will have problems
>    with the Agda-mode in the Emacs. There are some keystrokes
>    mentioned in many Agda documents, however, the Emacs claims that
>    they are not defined.

Which key strokes, and which documents?

> Other problems are e.g. with Restart -> Load, etc. It is really
> annoying after several attempts if the Emacs still says "first load
> file".

Could you be more explicit, please? I do not recognise your problems.

> Solution: automatic loading.

Do you mean that Agda files should be loaded immediately when they are
opened in Emacs? This does not seem like a good idea, because type
checking a large project can take quite a lot of time, and some files
are known not to be type correct (for instance because they are under
development).

> I guess Agda-mode has many bugs.

Bugs which are reported tend to get fixed pretty quickly.

> 3. If you have problem with the Agda-mode, you might then think to use
>    Agda-interpreter.

The interpreter is no longer supported. The following message should
have been printed when you started it:

  The interactive mode is no longer supported. Don't complain if it
  doesn't work.

> 4. On the whole, in general, for the family of ALF, there are many
>    documents which generate confusing and inconsistency as well as
>    many tool names and web sites belonging to this family.

Alf, Agda 1 and Alfa are separate from Agda 2. It is unfortunate that
Agda 1 and Agda 2, which are separate languages, have so similar names.

A while ago most (all?) of the web sites for Agda 1 were updated with
instructions about and links to Agda 2. I had hoped that this should be
enough to avoid problems like the ones you have had. Do any of these
instructions need to be improved?

-- 
/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.