[Agda] Recompilation triggers rechecking?
sanzhiyan at gmail.com
Fri Dec 6 19:38:26 CET 2013
I've asked on the IRC channel and It seems like Cabal won't accept such a
patch because it's not standard practice for similar tools (e.g. autotools).
It's still possible to customize Cabal's behaviour using a custom UserHooks
On Thu, Dec 5, 2013 at 3:10 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:
> That's it, thanks for finding out!
> So I caused this problem myself.
> Seems like we have to patch cabal then... Any takers?
> 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
>> 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
>> 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.
>> 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/~
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda