[Agda] Recompilation triggers rechecking?
sanzhiyan at gmail.com
Thu Dec 5 04:05:27 CET 2013
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.
On Wed, Dec 4, 2013 at 6:07 PM, Andreas Abel <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 ]
> 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
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda