[Agda] Recompilation triggers rechecking?

[Andrea Vezzosi]

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>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
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131205/1ea993c4/attachment.html