[Agda] Recompilation triggers rechecking?

Andrea Vezzosi 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.

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

More information about the Agda mailing list