[Agda-dev] Proposal: Remove the --interactive option

[Ulf Norell]

I remember that some people objected when I tried to get rid of it a few
years ago.

/ Ulf

On Thu, Feb 12, 2015 at 8:35 PM, Andreas Abel <abela at chalmers.se> wrote:

> Well, so far it still seems to work, even though it says it is no longer
> maintained.  I see no need to remove it now.  But we can wait for the
> results of the poll...
>
>
> On 12.02.2015 20:30, Andrés Sicard-Ramírez wrote:
>
>> Hi,
>>
>> After showing a nice Agda logo in ASCII, the command
>>
>>    $ agda --interactive
>>
>> says
>>
>>    The interactive mode is no longer supported. Don't complain if it
>> doesn't work.
>>
>> ​
>> I propose to remove the --interactive option and its associated module
>> Agda.Interaction.CommandLine.CommandLine (actually, I propose to comment
>> out the related code).
>>
>> Why? While fixing new bugs (e.g.
>> https://github.com/agda/agda/commit/8631ef270c387e6639873bafba8259
>> 247d76cba0)
>> and supporting various versions of GHC and libraries, why lost time
>> maintaining a option whose functionality is not maintained?
>>
>> ​My idea is remove the option from both branches (I know it isn't a
>> bug-fix).
>> ​
>> I will also ask in the Agda mailing list before removing the option.
>>
>> ​Comments?​
>>
>> --
>> Andrés
>>
>>
>> _______________________________________________
>> Agda-dev mailing list
>> Agda-dev at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda-dev
>>
>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150212/84494822/attachment.html