[bug#33478] [PATCH] gnu: agda: Upgrade to 2.5.4.2

[ludo@gnu.org (Ludovic Courtès)]

Hi Brett,

Brett Gilio <brettg@posteo.net> skribis:

> Ludovic Courtès writes:
>
>> Hello Brett,
>>
>> Brett Gilio <brettg@posteo.net> skribis:
>>
>>> Ludovic Courtès writes:
>>
>> [...]
>>
>>>> --8<---------------cut here---------------start------------->8---
>>>> [ 37 of 339] Compiling Agda.Utils.Memo  ( src/full/Agda/Utils/Memo.hs, dist/build/Agda/Utils/Memo.o )
>>>>
>>>> src/full/Agda/Utils/Memo.hs:10:1: error:
>>>>     Bad interface file: /gnu/store/fmq6ybv1m3yr9x2y16gv85nv30df9xw8-ghc-hashable-1.2.7.0/lib/ghc-8.4.3/hashable-1.2.7.0/Data/Hashable.hi
>>>>         Something is amiss; requested module  hashable-1.2.7.0:Data.Hashable differs from name found in the interface file hashable-1.2.7.0:Data.Hashable (if these names look the same, try again with -dppr-debug)
>>>>    |
>>>> 10 | import Data.Hashable
>>>>    | ^^^^^^^^^^^^^^^^^^^^
>>>> --8<---------------cut here---------------end--------------->8---
>>>>
>>>> Could you take a look?
>>>>
>>>> Thanks,
>>>> Ludo’.
>>>
>>> Hi Ludo,
>>>
>>> I put it through 20 rounds of building, and dumped the gc and
>>> everything. I can not replicate it on my end, can we get a third person
>>> to try it?
>>
>> I’m not sure what you mean by “20 rounds” and “dumped the gc”.  I would
>> expect such a failure to be deterministic.
>>
>> Are you testing this on ‘master’?  Which commit?  I tested it on top of
>> 63fd9f084a5e345d2edaeaf5e8f435a3130f9edc.
>>
>> Thanks,
>> Ludo’.
>
> --rounds=20 to see if it is deterministic. But as I said, I am not
>   replicating the error. Yes, I tested it on master, commit and on the
>   same commit number as you.

I’ve retried just now: applying the Agda patch alone on top of commit
0c17f72070cbfb04f311b776a080849b369aac25.  It’s the same derivation as
the one I tested above.

Are we in the exact same conditions?  I’m on x86_64.

Ludo’.