<div dir="ltr"><div>I've asked on the IRC channel and It seems like Cabal won't accept such a patch because it's not standard practice for similar tools (e.g. autotools).</div><div><br></div><div>It's still possible to customize Cabal's behaviour using a custom UserHooks in Setup.hs.</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Dec 5, 2013 at 3:10 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">That's it, thanks for finding out!<br>
<br>
So I caused this problem myself.<br>
<br>
Seems like we have to patch cabal then... Any takers?<br>
<br>
Cheers,<br>
Andreas<div class="im"><br>
<br>
On 05.12.2013 04:05, Andrea Vezzosi wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
It seems like the cause is that 'cabal install' produces a new<br>
Agda.Primitive each time, so modules importing that need to be recompiled.<br>
<br>
These recompilations might be a problem when testing modifications to<br>
agda on code with many dependencies though? I wonder if cabal can be<br>
convinced to keep the original timestamp when copying data files.<br>
<br>
-- Andrea<br>
<br>
<br>
On Wed, Dec 4, 2013 at 6:07 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div><div class="im">
<mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.<u></u>de</a>>> wrote:<br>
<br>
It seems like Agda rechecks everything (like standard library<br>
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<br>
maintain this number, or?<br>
<br>
Well, it could happen that someone uses an old agda on new interface<br>
files, and then there is a small probability that the new interface<br>
files can be deserialized without error (1), then you might be<br>
trigged into believing a wrong proposition and take your life as a<br>
consequence.<br>
<br>
The probability of (1) is likely in the same order of magnitude as<br>
getting a self-replicating Turing machine when throwing LEGO bricks<br>
into a laundry machine for the amount of time of your choice.<br>
[<br></div>
<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> <<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>><div class="im">
<br>
]<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></div>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.<u></u>de</a>><br>
<a href="http://www2.tcs.ifi.lmu.de/~__abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~__<u></u>abel/</a> <<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> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
</blockquote><div class="HOEnZb"><div class="h5">
<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>
</div></div></blockquote></div><br></div>