[PATCH] gnu: agda: Upgrade to 2.5.4.2

  • Done
  • quality assurance status badge
Details
3 participants
  • Brett Gilio
  • Efraim Flashner
  • Ludovic Courtès
Owner
unassigned
Submitted by
Brett Gilio
Severity
normal

Debbugs page

Brett Gilio wrote 6 years ago
(address . guix-patches@gnu.org)(name . Brett Gilio)(address . brettg@posteo.net)
20181124042450.8500-1-brettg@posteo.net
---
gnu/packages/agda.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)

Toggle diff (24 lines)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 6bb38aac4..be82ff9ec 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -31,7 +31,7 @@
(define-public agda
(package
(name "agda")
- (version "2.5.4.1")
+ (version "2.5.4.2")
(source
(origin
(method url-fetch)
@@ -40,7 +40,7 @@
version ".tar.gz"))
(sha256
(base32
- "0bxpibsk98n9xp42d92ma5vj2fam8rsnl61fbhr3askfjdvalnbp"))))
+ "07wvawpfjhx3gw2w53v27ncv1bl0kkx08wkm6wzxldbslkcasign"))))
(build-system haskell-build-system)
(inputs
`(("cpphs" ,cpphs)
--
2.19.2
Ludovic Courtès wrote 6 years ago
(name . Brett Gilio)(address . brettg@posteo.net)(address . 33478@debbugs.gnu.org)
87bm6eyxh7.fsf@gnu.org
Hello Brett,

Brett Gilio <brettg@posteo.net> skribis:

Toggle quote (15 lines)
> ---
> gnu/packages/agda.scm | 4 ++--
> 1 file changed, 2 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
> index 6bb38aac4..be82ff9ec 100644
> --- a/gnu/packages/agda.scm
> +++ b/gnu/packages/agda.scm
> @@ -31,7 +31,7 @@
> (define-public agda
> (package
> (name "agda")
> - (version "2.5.4.1")
> + (version "2.5.4.2")

It fails to build here:

Toggle snippet (10 lines)
[ 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
| ^^^^^^^^^^^^^^^^^^^^

Could you take a look?

Thanks,
Ludo’.
Brett Gilio wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)
8736rqjglo.fsf@posteo.net
Ludovic Courtès writes:

Toggle quote (37 lines)
> Hello Brett,
>
> Brett Gilio <brettg@posteo.net> skribis:
>
>> ---
>> gnu/packages/agda.scm | 4 ++--
>> 1 file changed, 2 insertions(+), 2 deletions(-)
>>
>> diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
>> index 6bb38aac4..be82ff9ec 100644
>> --- a/gnu/packages/agda.scm
>> +++ b/gnu/packages/agda.scm
>> @@ -31,7 +31,7 @@
>> (define-public agda
>> (package
>> (name "agda")
>> - (version "2.5.4.1")
>> + (version "2.5.4.2")
>
> It fails to build here:
>
> --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’.

Sure, I am running it through 20 rounds right now. I will also check for
the Data.Hashable dependencies and see what is going on. Will report
back soon.

Brett Gilio
Brett Gilio wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)
87zhtxsyin.fsf@posteo.net
Ludovic Courtès writes:

Toggle quote (37 lines)
> Hello Brett,
>
> Brett Gilio <brettg@posteo.net> skribis:
>
>> ---
>> gnu/packages/agda.scm | 4 ++--
>> 1 file changed, 2 insertions(+), 2 deletions(-)
>>
>> diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
>> index 6bb38aac4..be82ff9ec 100644
>> --- a/gnu/packages/agda.scm
>> +++ b/gnu/packages/agda.scm
>> @@ -31,7 +31,7 @@
>> (define-public agda
>> (package
>> (name "agda")
>> - (version "2.5.4.1")
>> + (version "2.5.4.2")
>
> It fails to build here:
>
> --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?

Best,
Brett Gilio
Ludovic Courtès wrote 6 years ago
(name . Brett Gilio)(address . brettg@posteo.net)(address . 33478@debbugs.gnu.org)
8736rpxmm8.fsf@gnu.org
Hello Brett,

Brett Gilio <brettg@posteo.net> skribis:

Toggle quote (2 lines)
> Ludovic Courtès writes:

[...]

Toggle quote (22 lines)
>> --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’.
Brett Gilio wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)
878t1hgnv4.fsf@posteo.net
Ludovic Courtès writes:

Toggle quote (39 lines)
> 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.

Brett
Ludovic Courtès wrote 6 years ago
(name . Brett Gilio)(address . brettg@posteo.net)(address . 33478@debbugs.gnu.org)
87ftvo9lr1.fsf@gnu.org
Hi Brett,

Brett Gilio <brettg@posteo.net> skribis:

Toggle quote (45 lines)
> 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’.
Brett Gilio wrote 5 years ago
(address . 33478@debbugs.gnu.org)
87fthz61x7.fsf@posteo.net
Brett Gilio <brettg@posteo.net> writes:

Toggle quote (27 lines)
> ---
> gnu/packages/agda.scm | 4 ++--
> 1 file changed, 2 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
> index 6bb38aac4..be82ff9ec 100644
> --- a/gnu/packages/agda.scm
> +++ b/gnu/packages/agda.scm
> @@ -31,7 +31,7 @@
> (define-public agda
> (package
> (name "agda")
> - (version "2.5.4.1")
> + (version "2.5.4.2")
> (source
> (origin
> (method url-fetch)
> @@ -40,7 +40,7 @@
> version ".tar.gz"))
> (sha256
> (base32
> - "0bxpibsk98n9xp42d92ma5vj2fam8rsnl61fbhr3askfjdvalnbp"))))
> + "07wvawpfjhx3gw2w53v27ncv1bl0kkx08wkm6wzxldbslkcasign"))))
> (build-system haskell-build-system)
> (inputs
> `(("cpphs" ,cpphs)

This is a historical bug report and is no longer relevant. It can be
closed.

--
Brett M. Gilio
Efraim Flashner wrote 5 years ago
(name . Brett Gilio)(address . brettg@posteo.net)(address . 33478-done@debbugs.gnu.org)
20191205083441.GM15280@E5400
On Wed, Dec 04, 2019 at 06:39:32PM -0600, Brett Gilio wrote:
Toggle quote (5 lines)
>
> This is a historical bug report and is no longer relevant. It can be
> closed.
>

The easiest way to do this is to send an email to
XXXXX-done@debbugs.gnu.org and that will close the bug.

--
Efraim Flashner <efraim@flashner.co.il> אפרים פלשנר
GPG key = A28B F40C 3E55 1372 662D 14F7 41AA E7DC CA3D 8351
Confidentiality cannot be guaranteed on emails sent or received unencrypted
-----BEGIN PGP SIGNATURE-----

iQIzBAABCgAdFiEEoov0DD5VE3JmLRT3Qarn3Mo9g1EFAl3owR4ACgkQQarn3Mo9
g1EGsw//T3GUxQ6tvx85KFBR904YqtrANgV2HsKcqChriB2bHGCVMKR582jzMamT
EMAPYk8lt3gAvovkGdxOdAjXuLaw1z8av0FuD9CmjphZYxIiWw3IkdxTWdA26CSH
NdoyB/cblrIvxelg+Wz9b74ijJlBhKzsiWK8z2UZ2t9+oFbXbyXXQDpbt3NM/aL0
7aPARnEt1n0dwY1+s04Xn7u8NaQshTz7MbKODUw+rDr46d+2YqNZYCDCVU6aJ7CK
+Rexo9AtMpzy7H9RkQUxzOvi/Uz2DZuQWpsVgZdbPufPRyXF4nX31VqVoVWVGKMQ
lDOlRR0myiL0zRF9ZEi0yxqdYzIzXI4PNmpRd3zQO5hNeorJJ++82droP8U6bpUX
DFXJJ8lHs8fQin6Zmtv4lV2ASub5d/O3rqtUWnr9OKWL36lndEgKCNkOl1rflj73
+X+/q6Nsi5rGIqknhrJc1mqgSy5i+aFj5RwcPTbGluKWlJnD6uFSfHXZ56VzNKup
cpbWFhTe9XZDCqEhaiEG1w0Y/i/hLKsurkBFGSci5H/18yXYVE+18uEFQUHHqxiN
kHzqxXmvfYkBvC33wJCMQrR9/wngltAPr3/GZPTXS61FuiJjaqXk7y0nfpAuzqUV
wuqdUfxgpYW6t432bZIGCBpNJLj5r0bVTMwq8qYHR972Qh8DvLk=
=PnmS
-----END PGP SIGNATURE-----


Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 33478@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 33478
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch
You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags
mumi command -t +confirmed -t +easy
Or, remove the moreinfo tag and set the help tag
mumi command -t -moreinfo -t +help