[Agda] Recompilation triggers rechecking?

[Andreas Abel]

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 ]

--
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/