[Agda] guidelines for reporting internal errors

[Ulf Norell]

It does help a lot. Any nontrivial internal error is almost impossible to
debug without a small test case. If you don't reduce the test case we have
to do it, so anything you can do is much appreciated.

/ Ulf

On Sat, Aug 19, 2017 at 4:41 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> How much does it help the Agda developers to have a small test case when
> given a report about an internal error? A lot or a little?
>
> I recently submitted an issue <https://github.com/agda/agda/issues/2709>
> reporting an internal error and linked to a fairly complex 300-line
> program. I spent considerable time reducing the program even that far and
> could have gone further, but I found myself running out of steam, unsure if
> my efforts were worth it. My question here is not about that issue
> specifically but in general aimed towards answering how I should go about
> reporting an internal error.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170819/bd3987cc/attachment.html>