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

Jesper Cockx Jesper at sikanda.be
Mon Jan 4 11:58:30 CET 2016


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160104/9f4e3ae8/attachment.html


More information about the Agda-dev mailing list