[Agda] Recompilation triggers rechecking?

[Andrea Vezzosi]

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
in Setup.hs.


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?
>
> Cheers,
> Andreas
>
>
> 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
>> 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<
>> 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 <mailto:andreas.abel at ifi.lmu.de>
>>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~
>> abel/>
>>     _________________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/__mailman/listinfo/agda
>>     <https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>>
>
> --
> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131206/08c1c912/attachment-0001.html