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

[Andreas Abel]

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/8631ef270c387e6639873bafba8259247d76cba0)
> 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/