<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I got the same bug, with 2.6.1.</p>
<p>But restarting agda, I fix it.</p>
<p>Perhaps I did not install Agda in an orthodox way !<br>
</p>
<p>Cheers,</p>
<p>Pierre<br>
</p>
<div class="moz-cite-prefix">Le 25/02/2019 à 12:45, Guillaume Allais
a écrit :<br>
</div>
<blockquote type="cite"
cite="mid:67b89280-6216-1b59-0b75-e541c830d44d@ens-lyon.org">
<pre class="moz-quote-pre" wrap="">Hi Phil,
This particularly annoying bug has been fixed in 2.5.4.2:
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3199">https://github.com/agda/agda/issues/3199</a>
Cheers,
--
gallais
On 25/02/2019 00:31, Philip Wadler wrote:
</pre>
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">I am getting a strange bug.
An internal error has occurred. Please report this as a bug.
</pre>
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">Location of the error:
src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">
Relevant source files attached. The error occurs in CoercionsS.lagda.
What is the best way to report this, please? -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. <a class="moz-txt-link-freetext" href="http://homepages.inf.ed.ac.uk/wadler/">http://homepages.inf.ed.ac.uk/wadler/</a>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre class="moz-signature" cols="72">--
Cordialement,
---------------------------
Pierre Lescanne (Professeur émérite)
LIP / ENS de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
<a class="moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------</pre>
</body>
</html>