GNU bug report logs - #35178
Agda doesn't build

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 35178 in the body.
You can then email your comments to 35178 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Pronaip <pronaip <at> protonmail.com>
To: "bug-guix <at> gnu.org" <bug-guix <at> gnu.org>
Subject: Agda doesn't build
Date: Sun, 07 Apr 2019 02:05:56 +0000

Partial build log below. Ran right after a guix pull && guix package -u.


starting phase `set-SOURCE-DATE-EPOCH'
phase `set-SOURCE-DATE-EPOCH' succeeded after 0.0 seconds
starting phase `set-paths'
environment variable `PATH' set to `/gnu/store/564215v4ma3jqxai20hf1ymcrn60nm44-ghc-8.4.3/bin:/gnu/store/xn6qx2p58rcswdy7ffv098dqagvabgnp-cpphs-1.20.8/bin:/gnu/store....
....
....
Configuring Agda-2.5.4.1...
Warning:
    This package indirectly depends on multiple versions of the same package. This is very likely to cause a compile failure.
      package network-uri (network-uri-2.6.1.0-AstEwZoXrlUJQq4VkxaVo9) requires parsec-3.1.13.0
      package regex-tdfa (regex-tdfa-1.2.3.1-4XsUntSXxH4A4zhCaXNDfb) requires parsec-3.1.13.0-Hto2wUzKFiH7SbmR1p2aoH
      package uri-encode (uri-encode-1.5.0.5-1EgYr8HkM9wD6gdpghyroU) requires text-1.2.3.0
      package parsec (parsec-3.1.13.0-Hto2wUzKFiH7SbmR1p2aoH) requires text-1.2.3.0
      package parsec (parsec-3.1.13.0) requires text-1.2.3.0
      package Agda (Agda-2.5.4.1) requires text-1.2.3.0
      package hashable (hashable-1.2.7.0-E92h8KGCxs9nEzqMyfi2y) requires text-1.2.3.0-AuQn1iHCodxHdm3cybaJfm
      package blaze-markup (blaze-markup-0.8.2.1-G01IErgxGnm2gnQBZJnf22) requires text-1.2.3.0-AuQn1iHCodxHdm3cybaJfm
      package blaze-html (blaze-html-0.9.1.1-GAgExUjjwqJ3ccn0WMIpSn) requires text-1.2.3.0-AuQn1iHCodxHdm3cybaJfm
      package blaze-builder (blaze-builder-0.4.1.0-Bxpj8zQZx6hE2zSu9Go0jT) requires text-1.2.3.0-AuQn1iHCodxHdm3cybaJfm
phase `configure' succeeded after 3.2 seconds
...
...
[ 63 of 338] Compiling Agda.Utils.FileName ( src/full/Agda/Utils/FileName.hs, dist/build/Agda/Utils/FileName.o )

src/full/Agda/Utils/FileName.hs:42:28: error:
    • No instance for (Hashable Text)
        arising from the 'deriving' clause of a data type declaration
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
      There are instances for similar types:
        instance Hashable text-1.2.3.0:Data.Text.Internal.Text
          -- Defined in ‘hashable-1.2.7.0:Data.Hashable.Class’
        instance Hashable text-1.2.3.0:Data.Text.Internal.Lazy.Text
          -- Defined in ‘hashable-1.2.7.0:Data.Hashable.Class’
    • When deriving the instance for (Hashable AbsolutePath)
   |
42 |   deriving (Eq, Ord, Data, Hashable)
   |                            ^^^^^^^^
Backtrace:
           4 (primitive-load "/gnu/store/j0nza4gsz3fkcxz2g85jp47063p…")
In ice-9/eval.scm:
   191:35  3 (_ _)
In srfi/srfi-1.scm:
   863:16  2 (every1 #<procedure 7c2020 at /gnu/store/79jn1m4ax1zr5…> …)
In /gnu/store/79jn1m4ax1zr5hlf3q7aalnb4vhx17ac-module-import/guix/build/gnu-build-system.scm:
   799:28  1 (_ _)
In /gnu/store/79jn1m4ax1zr5hlf3q7aalnb4vhx17ac-module-import/guix/build/utils.scm:
    616:6  0 (invoke _ . _)

/gnu/store/79jn1m4ax1zr5hlf3q7aalnb4vhx17ac-module-import/guix/build/utils.scm:616:6: In procedure invoke:
Throw to key `srfi-34' with args `(#<condition &invoke-error [program: "runhaskell" arguments: ("Setup.hs" "build") exit-status: 1 term-signal: #f stop-signal: #f] 56d440>)'.

Message #8 received at 35178 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Pronaip <pronaip <at> protonmail.com>
Cc: 35178 <at> debbugs.gnu.org
Subject: Re: bug#35178: Agda doesn't build
Date: Sun, 07 Apr 2019 18:28:35 +0200

Hello,

Pronaip <pronaip <at> protonmail.com> skribis:


[...]

> [ 63 of 338] Compiling Agda.Utils.FileName ( src/full/Agda/Utils/FileName.hs, dist/build/Agda/Utils/FileName.o )
>
> src/full/Agda/Utils/FileName.hs:42:28: error:
>     • No instance for (Hashable Text)
>         arising from the 'deriving' clause of a data type declaration
>       Possible fix:
>         use a standalone 'deriving instance' declaration,
>           so you can specify the instance context yourself
>       There are instances for similar types:
>         instance Hashable text-1.2.3.0:Data.Text.Internal.Text
>           -- Defined in ‘hashable-1.2.7.0:Data.Hashable.Class’
>         instance Hashable text-1.2.3.0:Data.Text.Internal.Lazy.Text
>           -- Defined in ‘hashable-1.2.7.0:Data.Hashable.Class’
>     • When deriving the instance for (Hashable AbsolutePath)
>    |
> 42 |   deriving (Eq, Ord, Data, Hashable)
>    |                            ^^^^^^^^

That looks a lot like <https://issues.guix.info/issue/34227>.

Could check whether it systematically fails to build?

Thank you,
Ludo’.

Message #11 received at 35178 <at> debbugs.gnu.org (full text, mbox):

From: Pronaip <pronaip <at> protonmail.com>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: "35178 <at> debbugs.gnu.org" <35178 <at> debbugs.gnu.org>
Subject: Re: bug#35178: Agda doesn't build
Date: Tue, 09 Apr 2019 02:59:32 +0000

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Sunday, April 7, 2019 6:28 PM, Ludovic Courtès <ludo <at> gnu.org> wrote:
> Could check whether it systematically fails to build?
>
> Thank you,
> Ludo’.

I've tried it a few times, it always gives the same result. The --rounds thing stops after the first failed build, so maybe I'm doing something wrong?

Message #14 received at 35178 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Pronaip <pronaip <at> protonmail.com>
Cc: "35178 <at> debbugs.gnu.org" <35178 <at> debbugs.gnu.org>
Subject: Re: bug#35178: Agda doesn't build
Date: Tue, 09 Apr 2019 12:58:02 +0200

Pronaip <pronaip <at> protonmail.com> skribis:

> ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
> On Sunday, April 7, 2019 6:28 PM, Ludovic Courtès <ludo <at> gnu.org> wrote:
>> Could check whether it systematically fails to build?
>>
>> Thank you,
>> Ludo’.
>
> I've tried it a few times, it always gives the same result. The --rounds thing stops after the first failed build, so maybe I'm doing something wrong?

‘--rounds’ will try several times only as long as building succeeds.

So in this case, you can simply run “guix build agda” several times.

Let us know how it goes.

Thanks,
Ludo’.

Message #17 received at 35178 <at> debbugs.gnu.org (full text, mbox):

From: Pronaip <pronaip <at> protonmail.com>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: "35178\\@debbugs.gnu.org" <35178 <at> debbugs.gnu.org>
Subject: Re: bug#35178: Agda doesn't build
Date: Sat, 25 May 2019 21:58:16 +0000

Oh I forgot to update this. The build seems to work fine now for some reason.


Sent with ProtonMail Secure Email.

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Tuesday, April 9, 2019 12:58 PM, Ludovic Courtès <ludo <at> gnu.org> wrote:

> Pronaip pronaip <at> protonmail.com skribis:
>
> > ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
> > On Sunday, April 7, 2019 6:28 PM, Ludovic Courtès ludo <at> gnu.org wrote:
> >
> > > Could check whether it systematically fails to build?
> > > Thank you,
> > > Ludo’.
> >
> > I've tried it a few times, it always gives the same result. The --rounds thing stops after the first failed build, so maybe I'm doing something wrong?
>
> ‘--rounds’ will try several times only as long as building succeeds.
>
> So in this case, you can simply run “guix build agda” several times.
>
> Let us know how it goes.
>
> Thanks,
> Ludo’.

Message #24 received at 35178-done <at> debbugs.gnu.org (full text, mbox):

From: Andreas Enge <andreas <at> enge.fr>
To: Pronaip <pronaip <at> protonmail.com>
Cc: 35178-done <at> debbugs.gnu.org,
 Ludovic Courtès <ludo <at> gnu.org>
Subject: Re: bug#35178: Agda doesn't build
Date: Mon, 27 May 2019 08:10:00 +0200

So closing this bug. Thanks,

Andreas

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.