[Agda] User-test - starting problems with Agda2

[Steffen Bock]

Hi All,

After I have got acquainted with the Martin Löf's theory, I am interested in practical execises so I went to the Agda system. I have to say some words for getting started with the Agda system. Perhaps, this feedback helps the developers improve the system.

It is really hard to get started with it due to the following:

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.

Solution: One can make this instruction more easier and enable an-easy start with Agda.

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. I cannot reconstruct the bugs.
Other problems are e.g. with Restart -> Load, etc.  It is really annoying after several attempts
if the Emacs still says "first load file".

Solution: automatic loading. I guess Agda-mode has many bugs.

3. If you have problem with the Agda-mode, you might then think to use Agda-interpreter.
    Then you will have again a problem.
    Type "agda --interactive" and just type "module XXX  where"  and enter. Then it will come a parser error. It can be however, one can make the system more flexible. So at the end
you will have no idea how to proceed with the interpreter. There is no document about describing this interactive mode.

Solution: I think the documents available there should describe also the interactive mode.

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.

For instance, ALF, Agda1, Agda2, Alfa - there are also many agda script files available which are syntaxtically not supported by the current version of Agda, etc.
For instance, one writes module X where, others write module X: where, etc.

Solution:  Please check the documents for Coq or Isabelle - a start with these tools were really easy.

My question is why should we make our life so complicated? 
I believe that a start with a software should be really very easy!

I am happy if you could respond to some issues mentioned above. It will help me use
Agda successfully and also save many hours for the beginners.

Best regards.

Steffen.


      
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090831/0ed65653/attachment.html