[Agda-dev] How to run and edit interaction tests?

[Ulf Norell]

There's some sed script magic in the Makefile to translate between the old
and the new syntax for interaction commands.

/ Ulf

On Mon, Jan 4, 2016 at 11:58 AM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi all,
>
> Is there a way to run a single interaction script (e.g.
> test/interaction/Long.in) manually? A change in my unification branch
> causes the output to be different from Long.out, so I want to see where
> exactly the two versions diverge. I have tried to start the interaction
> mode manually and follow the substitutions in test/interaction/README, but
> I keep getting an error "cannot read":
>
> $ agda --interaction
> Agda2> ioTCM Long.agda None (cmd_load_highlighting_info Long.agda)
> cannot read: ioTCM Long.agda None (cmd_load_highlighting_info Long.agda)
>
> cheers,
> Jesper
>
>
> _______________________________________________
> 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/20160104/90574726/attachment.html