<div dir="ltr"><div>I&#39;ve asked on the IRC channel and It seems like Cabal won&#39;t accept such a patch because it&#39;s not standard practice for similar tools (e.g. autotools).</div><div><br></div><div>It&#39;s still possible to customize Cabal&#39;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">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That&#39;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 &#39;cabal install&#39; 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 &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div><div class="im">
&lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.<u></u>de</a>&gt;&gt; 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> &lt;<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>&gt;<div class="im">
<br>
    ]<br>
<br>
    --<br>
    Andreas Abel  &lt;&gt;&lt;      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> &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.<u></u>de</a>&gt;<br>
    <a href="http://www2.tcs.ifi.lmu.de/~__abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~__<u></u>abel/</a> &lt;<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a>&gt;<br>

    ______________________________<u></u>___________________<br>
    Agda mailing list<br>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
    <a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
    &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;<br>
<br>
<br>
</blockquote><div class="HOEnZb"><div class="h5">
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      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>