<div dir="ltr">It seems like the cause is that 'cabal install' produces a new Agda.Primitive each time, so modules importing that need to be recompiled.<div><br><div>These recompilations might be a problem when testing modifications to agda on code with many dependencies though? I wonder if cabal can be convinced to keep the original timestamp when copying data files. </div>
<div><br></div><div>-- Andrea</div>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Dec 4, 2013 at 6:07 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It seems like Agda rechecks everything (like standard library modules I import) when Agda itself has been recompiled.<br>
<br>
Why is that?<br>
<br>
I thought that would only happen if the serialization stamp got updated.<br>
<br>
currentInterfaceVersion :: Word64<br>
currentInterfaceVersion = 20131109 * 10 + 0<br>
<br>
If that is no longer the case, there is no pressing reason to maintain this number, or?<br>
<br>
Well, it could happen that someone uses an old agda on new interface files, and then there is a small probability that the new interface files can be deserialized without error (1), then you might be trigged into believing a wrong proposition and take your life as a consequence.<br>
<br>
The probability of (1) is likely in the same order of magnitude as getting a self-replicating Turing machine when throwing LEGO bricks into a laundry machine for the amount of time of your choice.<br>
[ <a href="http://www.minet.uni-jena.de/fakultaet/iam/personen/althofer.html" target="_blank">http://www.minet.uni-jena.de/<u></u>fakultaet/iam/personen/<u></u>althofer.html</a> ]<br>
<br>
--<br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>