[Agda] Poll: Remove the Agda interactive mode

[Håkon Robbestad Gylterud]

Hi,

I am currently using Agda interactive mode.

Although it is not supported, it is a natural part of my workflow as I
don't use Emacs. I mostly use it to normalise terms and check the type
of terms in contexts. I find it a great support to have a session of
--interactive open in my editor. Since the history of my terminal is
editable, I use it as a sort of scratch pad with terms and their types.
Then I can evaluate terms and check types as I go along.  Sometimes I
use :give with new holes as a way to search for proofs, without
cluttering the original file, and just copy over to the main file if the
search leads to anything.

I know these things could be done in Emacs as well, but I really prefer
my current editor (Acme from Plan 9). My use would however be covered
80% if there was just a way to show the type and context of unsolved
metas and evaluate terms from the command line.

Best regards,
Håkon R. Gylterud