Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Agda fails to build due to equivalence-0.3.3 dependency failing to build #53396

Closed
canndrew opened this issue Jan 4, 2019 · 7 comments
Closed
Labels
6.topic: agda "A dependently typed programming language / interactive theorem prover"

Comments

@canndrew
Copy link
Contributor

canndrew commented Jan 4, 2019

Issue description

As stated in the title, I can't build haskellPackages.Agda because one of its dependencies fails to build.

Steps to reproduce

  • Add haskellPackages.Agda to my environment.systemPackages in configuration.nix
  • run nixos-rebuild build

Technical details

nix-info output:

 - system: `"x86_64-linux"`
 - host os: `Linux 4.19.12, NixOS, 19.03.git.201d739b0ffM (Koi)`
 - multi-user?: `no`
 - sandbox: `yes`
 - version: `nix-env (Nix) 2.1.3`
 - channels(root): `"nixos-16.03.1299.a8e0739"`
 - nixpkgs: `/home/shum/src/nixos/nixpkgs`

nixos-rebuild output:

building '/nix/store/y02f980xlrkgpn673pl83szfn8xld88m-equivalence-0.3.3.drv'...
setupCompilerEnvironmentPhase
Build with /nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3.
unpacking sources
unpacking source archive /nix/store/frafd3mhl01yqkfwnjzgzj4s4ispmr1i-equivalence-0.3.3.tar.gz
source root is equivalence-0.3.3
setting SOURCE_DATE_EPOCH to timestamp 1537694683 of file equivalence-0.3.3/testsuite/tests/Data_Test.hs
patching sources
compileBuildDriverPhase
setupCompileFlags: -package-db=/build/setup-package.conf.d -j8 -threaded
[1 of 1] Compiling Main             ( Setup.hs, /build/Main.o )
Linking Setup ...
configuring
configureFlags: --verbose --prefix=/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3 --libdir=$prefix/lib/$compiler --libsubdir=$abi/$libname --docdir=/nix/store/v1ikgmvhf800m1vqdl72ji49f4h9brlq-equivalence-0.3.3-doc/share/doc/equivalence-0.3.3 --with-gcc=gcc --package-db=/build/package.conf.d --ghc-option=-j8 --disable-split-objs --enable-library-profiling --profiling-detail=exported-functions --disable-profiling --enable-shared --disable-coverage --enable-static --disable-executable-dynamic --enable-tests --disable-benchmarks --enable-library-vanilla --enable-library-for-ghci --ghc-option=-split-sections --extra-lib-dirs=/nix/store/1knlbapiimgav7kr6kzcz7p404qvydx2-ncurses-6.1-20181027/lib --extra-lib-dirs=/nix/store/9yb6gizxpll4l6gf7md75kbii6b1dvjc-gmp-6.1.2/lib
Using Parsec parser
Configuring equivalence-0.3.3...
Dependency STMonadTrans >=0.4.3: using STMonadTrans-0.4.3
Dependency base ==4.*: using base-4.12.0.0
Dependency containers -any: using containers-0.6.0.1
Dependency mtl >=2.0.1: using mtl-2.2.2
Dependency transformers >=0.2: using transformers-0.5.5.0
Dependency transformers-compat >=0.3: using transformers-compat-0.6.2
Dependency QuickCheck >=2: using QuickCheck-2.12.6.1
Dependency STMonadTrans >=0.4.3: using STMonadTrans-0.4.3
Dependency base >=4: using base-4.12.0.0
Dependency containers -any: using containers-0.6.0.1
Dependency mtl >=2.0.1: using mtl-2.2.2
Dependency template-haskell -any: using template-haskell-2.14.0.0
Dependency test-framework -any: using test-framework-0.8.2.0
Dependency test-framework-quickcheck2 -any: using
test-framework-quickcheck2-0.3.0.5
Dependency transformers >=0.2: using transformers-0.5.5.0
Dependency transformers-compat >=0.3: using transformers-compat-0.6.2
Source component graph:
    component test:test
    component lib
Configured component graph:
    component equivalence-0.3.3-L2YQHanjvulGeqUdzT8s3O-test
        include QuickCheck-2.12.6.1-2neFyIv0PQcKVFUR4jOgvi
        include STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        include base-4.12.0.0
        include containers-0.6.0.1
        include mtl-2.2.2
        include template-haskell-2.14.0.0
        include test-framework-0.8.2.0-BE66rxkgm8MVq2rZNrTFn
        include test-framework-quickcheck2-0.3.0.5-5SWSE9sJmErF53OTJaRnWj
        include transformers-0.5.5.0
        include transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
    component equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK
        include STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        include base-4.12.0.0
        include containers-0.6.0.1
        include mtl-2.2.2
        include transformers-0.5.5.0
        include transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
Linked component graph:
    unit equivalence-0.3.3-L2YQHanjvulGeqUdzT8s3O-test
        include QuickCheck-2.12.6.1-2neFyIv0PQcKVFUR4jOgvi
        include STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        include base-4.12.0.0
        include containers-0.6.0.1
        include mtl-2.2.2
        include template-haskell-2.14.0.0
        include test-framework-0.8.2.0-BE66rxkgm8MVq2rZNrTFn
        include test-framework-quickcheck2-0.3.0.5-5SWSE9sJmErF53OTJaRnWj
        include transformers-0.5.5.0
        include transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
    unit equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK
        include STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        include base-4.12.0.0
        include containers-0.6.0.1
        include mtl-2.2.2
        include transformers-0.5.5.0
        include transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
        Data.Equivalence.Monad=equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK:Data.Equivalence.Monad,Data.Equivalence.STT=equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK:Data.Equivalence.STT
Ready component graph:
    definite equivalence-0.3.3-L2YQHanjvulGeqUdzT8s3O-test
        depends QuickCheck-2.12.6.1-2neFyIv0PQcKVFUR4jOgvi
        depends STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        depends base-4.12.0.0
        depends containers-0.6.0.1
        depends mtl-2.2.2
        depends template-haskell-2.14.0.0
        depends test-framework-0.8.2.0-BE66rxkgm8MVq2rZNrTFn
        depends test-framework-quickcheck2-0.3.0.5-5SWSE9sJmErF53OTJaRnWj
        depends transformers-0.5.5.0
        depends transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
    definite equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK
        depends STMonadTrans-0.4.3-Lp5Nsw9KC54HLvWhUpER4s
        depends base-4.12.0.0
        depends containers-0.6.0.1
        depends mtl-2.2.2
        depends transformers-0.5.5.0
        depends transformers-compat-0.6.2-JV1ddSnlm3mL2xw4J4K8Kw
Using Cabal-2.4.0.1 compiled by ghc-8.6
Using compiler: ghc-8.6.3
Using install prefix:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3
Executables installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/bin
Libraries installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/lib/ghc-8.6.3/x86_64-linux-ghc-8.6.3/equivalence-0.3.3-HFtHJ0LmiaG8xUvDyDhuwK
Dynamic Libraries installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/lib/ghc-8.6.3/x86_64-linux-ghc-8.6.3
Private executables installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/libexec/x86_64-linux-ghc-8.6.3/equivalence-0.3.3
Data files installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/share/x86_64-linux-ghc-8.6.3/equivalence-0.3.3
Documentation installed in:
/nix/store/v1ikgmvhf800m1vqdl72ji49f4h9brlq-equivalence-0.3.3-doc/share/doc/equivalence-0.3.3
Configuration files installed in:
/nix/store/w8p8dhdhwbdzbnch709vz3xb9qp6f45j-equivalence-0.3.3/etc
No alex found
Using ar found on system at:
/nix/store/jdlb06c0kp6sms277xcclfr3gdl8pb9r-binutils-2.30/bin/ar
No c2hs found
No cpphs found
No doctest found
Using gcc version 7.3.0 given by user at:
/nix/store/klci955kxil7q32ggran6lnhpnkk8yjz-gcc-wrapper-7.3.0/bin/gcc
Using ghc version 8.6.3 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/ghc
Using ghc-pkg version 8.6.3 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/ghc-pkg
No ghcjs found
No ghcjs-pkg found
No greencard found
Using haddock version 2.22.0 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/haddock
No happy found
Using haskell-suite found on system at: haskell-suite-dummy-location
Using haskell-suite-pkg found on system at: haskell-suite-pkg-dummy-location
No hmake found
Using hpc version 0.67 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/hpc
Using hsc2hs version 0.68.5 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/hsc2hs
Using hscolour version 1.24 found on system at:
/nix/store/cgvcwjzxyaqxs3d5mxg29g894zmbavi4-hscolour-1.24.4/bin/HsColour
No jhc found
Using ld found on system at:
/nix/store/4m3l2rv3gdyaqmx19mxskd1cgxzgc7dd-binutils-wrapper-2.30/bin/ld
No pkg-config found
Using runghc version 8.6.3 found on system at:
/nix/store/ksbwy0z47ql0mjlqvcrk563viwvngxr2-ghc-8.6.3/bin/runghc
Using strip version 2.30 found on system at:
/nix/store/jdlb06c0kp6sms277xcclfr3gdl8pb9r-binutils-2.30/bin/strip
Using tar found on system at:
/nix/store/9ci8vzqdc2vs7byxm3pfdclh89lbn7hn-gnutar-1.30/bin/tar
No uhc found
building
Preprocessing test suite 'test' for equivalence-0.3.3..
Building test suite 'test' for equivalence-0.3.3..

<no location info>: warning: [-Wmissing-home-modules]
    These modules are needed for compilation but not listed in your .cabal file's other-modules:
        Data.Equivalence.Monad Data.Equivalence.STT
[1 of 4] Compiling Data.Equivalence.STT ( src/Data/Equivalence/STT.hs, dist/build/test/test-tmp/Data/Equivalence/STT.o )
[2 of 4] Compiling Data.Equivalence.Monad ( src/Data/Equivalence/Monad.hs, dist/build/test/test-tmp/Data/Equivalence/Monad.o )
[3 of 4] Compiling Data.Equivalence.Monad_Test ( testsuite/tests/Data/Equivalence/Monad_Test.hs, dist/build/test/test-tmp/Data/Equivalence/Monad_Test.o )

testsuite/tests/Data/Equivalence/Monad_Test.hs:79:3: error:
    • No instance for (Control.Monad.Fail.MonadFail
                         (EquivT s (Set Int) Int Data.Functor.Identity.Identity))
        arising from a do statement
        with the failable pattern ‘[cx, cy]’
    • In a stmt of a 'do' block: [cx, cy] <- getClasses [x, y]
      In the second argument of ‘($)’, namely
        ‘do [cx, cy] <- getClasses [x, y]
            combine cx cy
            d <- desc cx
            return (d == Set.fromList [x, y])’
      In the expression:
        runInt
          $ do [cx, cy] <- getClasses [x, y]
               combine cx cy
               d <- desc cx
               return (d == Set.fromList [x, y])
   |
79 |   [cx,cy] <- getClasses [x,y]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

testsuite/tests/Data/Equivalence/Monad_Test.hs:90:3: error:
    • No instance for (Control.Monad.Fail.MonadFail
                         (EquivT s (Set Int) Int Data.Functor.Identity.Identity))
        arising from a do statement
        with the failable pattern ‘[cx, cy, cz]’
    • In a stmt of a 'do' block: [cx, cy, cz] <- getClasses [x, y, z]
      In the second argument of ‘($)’, namely
        ‘do [cx, cy, cz] <- getClasses [x, y, ....]
            combine cx cy
            combine cy cz
            cx === cz’
      In the expression:
        runInt
          $ do [cx, cy, cz] <- getClasses [x, y, ....]
               combine cx cy
               combine cy cz
               cx === cz
   |
90 |   [cx,cy,cz] <- getClasses [x,y,z]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

testsuite/tests/Data/Equivalence/Monad_Test.hs:109:3: error:
    • No instance for (Control.Monad.Fail.MonadFail
                         (EquivT s (Set Int) Int Data.Functor.Identity.Identity))
        arising from a do statement
        with the failable pattern ‘[cx, cy]’
    • In a stmt of a 'do' block: [cx, cy] <- getClasses [x, y]
      In the second argument of ‘($)’, namely
        ‘do let l1 = x : l1'
                l2 = y : l2'
            cls1 <- getClasses l1
            cls2 <- getClasses l2
            [cx, cy] <- getClasses [x, y]
            ....’
      In the expression:
        runInt
          $ do let l1 = x : l1'
                   l2 = y : l2'
               cls1 <- getClasses l1
               cls2 <- getClasses l2
               [cx, cy] <- getClasses [x, y]
               ....
    |
109 |   [cx,cy] <- getClasses [x,y]
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

testsuite/tests/Data/Equivalence/Monad_Test.hs:172:18: error:
    • No instance for (Control.Monad.Fail.MonadFail
                         (EquivT s (Set Int) Int Data.Functor.Identity.Identity))
        arising from a do statement
        with the failable pattern ‘[cx, cy]’
    • In a stmt of a 'do' block: [cx, cy] <- getClasses [x, y]
      In the second argument of ‘($)’, namely
        ‘do cls1 <- mapM getClasses l1
            mapM combineAll cls1
            cls2 <- getClasses l2
            mapM remove cls2
            ....’
      In the expression:
        runInt
          $ do cls1 <- mapM getClasses l1
               mapM combineAll cls1
               cls2 <- getClasses l2
               mapM remove cls2
               ....
    |
172 |                  [cx,cy] <- getClasses [x,y]
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^
builder for '/nix/store/y02f980xlrkgpn673pl83szfn8xld88m-equivalence-0.3.3.drv' failed with exit code 1
cannot build derivation '/nix/store/3p4q9lj7zr762cyvk9qb35mzfwqghnb8-Agda-2.5.4.2.drv': 1 dependencies couldn't be built
@michaelpj
Copy link
Contributor

I've opened pa-ba/equivalence#4 upstream.

@michaelpj
Copy link
Contributor

Agda itself has a bunch of problems compiling with GHC 8.6, we should probably just pin the version of Agda to an 8.4 version until they do a new release.

@michaelpj
Copy link
Contributor

Hm, although we don't seem to do that anywhere, so maybe it's frowned upon.

@pschuprikov
Copy link
Contributor

A new version of Agda seems to be on its way to release agda/agda#3391

@turion
Copy link
Contributor

turion commented Dec 13, 2019

I believe this is fixed now?

@turion
Copy link
Contributor

turion commented May 15, 2020

@canndrew I'm pretty sure this is fixed since #76653. Can you revisit and close?

@veprbl veprbl closed this as completed May 15, 2020
@veprbl
Copy link
Member

veprbl commented May 15, 2020

This should be fixed on master.

@veprbl veprbl added the 6.topic: agda "A dependently typed programming language / interactive theorem prover" label Feb 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
6.topic: agda "A dependently typed programming language / interactive theorem prover"
Projects
None yet
Development

No branches or pull requests

5 participants