[Agda] Recompilation triggers rechecking?

[Andreas Abel]

That's it, thanks for finding out!

So I caused this problem myself.

Seems like we have to patch cabal then...  Any takers?

Cheers,
Andreas

On 05.12.2013 04:05, Andrea Vezzosi wrote:
> It seems like the cause is that 'cabal install' produces a new
> Agda.Primitive each time, so modules importing that need to be recompiled.
>
> 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.
>
> -- Andrea
>
>
> On Wed, Dec 4, 2013 at 6:07 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     It seems like Agda rechecks everything (like standard library
>     modules I import) when Agda itself has been recompiled.
>
>     Why is that?
>
>     I thought that would only happen if the serialization stamp got updated.
>
>        currentInterfaceVersion :: Word64
>        currentInterfaceVersion = 20131109 * 10 + 0
>
>     If that is no longer the case, there is no pressing reason to
>     maintain this number, or?
>
>     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.
>
>     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.
>     [
>     http://www.minet.uni-jena.de/__fakultaet/iam/personen/__althofer.html <http://www.minet.uni-jena.de/fakultaet/iam/personen/althofer.html>
>     ]
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Theoretical Computer Science, University of Munich
>     Oettingenstr. 67, D-80538 Munich, GERMANY
>
>     andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>     _________________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/