[Agda] interactive mode

[Thorsten Altenkirch]

Hi Andres,

have you actually tried the emacs mode? It is becoming the standard  
way to develop Agda programs, and it is quite usable these days & I  
suspect that it is more productive then using the interactive mode.

I agree that ideally the programming language shouldn't dictate the  
development tools. Agda is doing better than Epigram, it allows you to  
use a batch mode and it's emacs interface is more flexible.  
Dependently typed languages redefine this question, because one could  
argue that the ability to batch "compile" your programs is not enough  
you also want a low-tech interface to interactive program development/

Cheers,
Thorsten

On 9 Jun 2008, at 09:16, Andres Loeh wrote:

> Hi again.
>
> Thanks for the answer ...
>
>>> I've just noticed that latest darcs versions of Agda
>>> claim that the interactive mode is no longer supported.
>>> This comes as a surprise (and shock) to me -- I use it
>>> all the time.
>>
>> I think it has been unsupported for a long time, it just has not been
>> advertised properly before.
>>
>> (Just to avoid confusion: The batch mode and the Emacs mode are still
>> supported, but not agda --interactive.)
>>
>>> Why will it no longer be supported?
>>
>> Presumably because it had few users, the Emacs mode has more  
>> features,
>> and we have limited man-power.
>
> Understandable. But is it so hard to support? Have there been many
> problems with interactive mode that make it likely it won't work  
> without
> much trouble in the future?
>
>> What kind of interface to Agda would you like to see, by the way?
>
> I was actually relatively happy with --interactive, apart from the
> fact that :r always seems to reload *all* modules, and that can take
> a long time. Is this a problem that would be fixed by switching to
> the Emacs interface?
>
> Personally, I'm a vim user, but I've used Emacs in the past. I just
> generally don't like it if a programming language dictates the editor
> I should use, and have considered the fact that Agda didn't as a
> huge advantage over Epigram so far.
>
> Cheers,
>  Andres
>
> -- 
>
> Andres Loeh, Universiteit Utrecht
>
> mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
> http://www.andres-loeh.de
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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.