From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:59513) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gRE7c-00055q-LM for guix-patches@gnu.org; Mon, 26 Nov 2018 05:28:09 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gRE7W-0005W4-Cc for guix-patches@gnu.org; Mon, 26 Nov 2018 05:28:08 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:43597) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gRE7W-0005Vp-8d for guix-patches@gnu.org; Mon, 26 Nov 2018 05:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gRE7W-0002pa-5Y for guix-patches@gnu.org; Mon, 26 Nov 2018 05:28:02 -0500 Subject: [bug#33478] [PATCH] gnu: agda: Upgrade to 2.5.4.2 Resent-Message-ID: From: ludo@gnu.org (Ludovic =?UTF-8?Q?Court=C3=A8s?=) References: <20181124042450.8500-1-brettg@posteo.net> <87bm6eyxh7.fsf@gnu.org> <87zhtxsyin.fsf@posteo.net> <8736rpxmm8.fsf@gnu.org> <878t1hgnv4.fsf@posteo.net> Date: Mon, 26 Nov 2018 11:27:46 +0100 In-Reply-To: <878t1hgnv4.fsf@posteo.net> (Brett Gilio's message of "Sun, 25 Nov 2018 09:47:59 -0600") Message-ID: <87ftvo9lr1.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Brett Gilio Cc: 33478@debbugs.gnu.org Hi Brett, Brett Gilio skribis: > Ludovic Court=C3=A8s writes: > >> Hello Brett, >> >> Brett Gilio skribis: >> >>> Ludovic Court=C3=A8s 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-gh= c-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.Ha= shable 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=E2=80=99. >>> >>> 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=E2=80=99m not sure what you mean by =E2=80=9C20 rounds=E2=80=9D and = =E2=80=9Cdumped the gc=E2=80=9D. I would >> expect such a failure to be deterministic. >> >> Are you testing this on =E2=80=98master=E2=80=99? Which commit? I test= ed it on top of >> 63fd9f084a5e345d2edaeaf5e8f435a3130f9edc. >> >> Thanks, >> Ludo=E2=80=99. > > --rounds=3D20 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=E2=80=99ve retried just now: applying the Agda patch alone on top of comm= it 0c17f72070cbfb04f311b776a080849b369aac25. It=E2=80=99s the same derivation= as the one I tested above. Are we in the exact same conditions? I=E2=80=99m on x86_64. Ludo=E2=80=99.