agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.5k stars 351 forks source link

build failure with ghc 7.8.3 and transformers 0.3.0.0 #1590

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
src/full/Agda/Utils/Bag.hs:198:43:
    Could not deduce (Eq (Identity (Bag a))) arising from a use of ‘==’
    from the context (Ord a)
      bound by the type signature for
                 prop_traverse_id :: Ord a => Bag a -> Bool
      at src/full/Agda/Utils/Bag.hs:197:21-42
    In the expression: traverse' Identity b == Identity b
    In an equation for ‘prop_traverse_id’:
        prop_traverse_id b = traverse' Identity b == Identity b
cabal: Error: some packages failed to install:
Agda-2.4.3 failed during the building phase. The exception was:
ExitFailure 1
make: *** [install-bin] Error 1

Original issue reported on code.google.com by jmchap...@gmail.com on 26 Jun 2015 at 1:00

GoogleCodeExporter commented 9 years ago
I tested using GHC 7.6.3, 7.8.4, and 7.10.1 before pushing...

I assume that you're using transformers 0.3.0.0, which doesn't have
the instance Eq a => Eq (Identity a). Is that correct? Can we drop
support for this version of transformers when we drop support for GHC
7.4.2?

Original comment by nils.anders.danielsson on 26 Jun 2015 at 1:39

GoogleCodeExporter commented 9 years ago
> Can we drop support for this version of transformers when we drop support for 
GHC
7.4.2?

No. This version of transformers is required because it was included in GHC 
7.8. In fact, there is no problem with GHC 7.4.2 and the current version of 
transformers. 

Original comment by andres.s...@gmail.com on 26 Jun 2015 at 6:42

GoogleCodeExporter commented 9 years ago

Original comment by andres.s...@gmail.com on 27 Jun 2015 at 3:18

GoogleCodeExporter commented 9 years ago
> I assume that you're using transformers 0.3.0.0, which doesn't have
the instance Eq a => Eq (Identity a). Is that correct? 

Are you, James?

Original comment by andres.s...@gmail.com on 27 Jun 2015 at 4:15

GoogleCodeExporter commented 9 years ago
I couldn't reproduce the issue with GHC 7.8.3 and the Travis builds using GHC 
7.8.4 were successful (maint: https://travis-ci.org/agda/agda/builds/68620149 
master:https://travis-ci.org/agda/agda/builds/68620174), so I'm closing the 
issue. Please reopen it if necessary.

Original comment by andres.s...@gmail.com on 27 Jun 2015 at 7:03

GoogleCodeExporter commented 9 years ago
Sorry for being slow to respond.

I am using transformers 0.3.0.0.

I don't want to make a fuss about this problem just for me, which will go away 
when I move to the next HP I expect. But, is this a problem likely to bite 
others?

Original comment by jmchap...@gmail.com on 30 Jun 2015 at 9:56

GoogleCodeExporter commented 9 years ago
Can't we use https://hackage.haskell.org/package/transformers-compat to be 
compatible with transformers-0.3.0.0 ?

Original comment by andreas....@gmail.com on 1 Jul 2015 at 8:05

GoogleCodeExporter commented 9 years ago
If I add

import Control.Monad.Trans.Except

to 

src/full/Agda/Utils/Bag.hs

then the build succeeds for me. But, I assume this would break it for others.

Should I wrap it in an #if? If so what exactly

#if !(MIN_VERSION_transformers(0,3,0))

?

Original comment by jmchap...@gmail.com on 2 Jul 2015 at 9:57

GoogleCodeExporter commented 9 years ago
I have transformers-compat-0.4.0.3 and I assume the above import is making use 
of this.

Original comment by jmchap...@gmail.com on 2 Jul 2015 at 9:58

GoogleCodeExporter commented 9 years ago
We are supporting transformers 0.3.0.0 because 
https://code.google.com/p/agda/issues/detail?id=1156#c7 .

James, can you install Agda using a more recent version of transformers? That 
is, can you install Agda using the following commands

  $ cabal update
  $ cabal install transformers
  ...
  Installed transformers-0.4.3.0
  $ make install-bin CABAL_OPTS=--constraint=tranformers==0.4.3.0

?  

Original comment by andres.s...@gmail.com on 3 Jul 2015 at 3:17

GoogleCodeExporter commented 9 years ago
I couldn't reproduce the issue in #1 using GHC 7.8.3 and transformers 0.3.0.0.

Original comment by andres.s...@gmail.com on 3 Jul 2015 at 3:32

GoogleCodeExporter commented 9 years ago
> I couldn't reproduce the issue in #1 using GHC 7.8.3 and transformers 0.3.0.0.

I meant the issue in #0.

Original comment by andres.s...@gmail.com on 5 Jul 2015 at 2:57

GoogleCodeExporter commented 9 years ago
[deleted comment]
GoogleCodeExporter commented 9 years ago
$ ghc-pkg list | grep transformers
    transformers-0.3.0.0
    transformers-0.4.3.0
    transformers-base-0.4.4
    transformers-compat-0.4.0.3

$ make install-bin CABAL_OPTS=--constraint=tranformers==0.4.3.0
cabal install --enable-tests --disable-library-profiling 
--disable-documentation --constraint=tranformers==0.4.3.0 
--builddir=./dist-2.4.3
Resolving dependencies...
In order, the following would be installed:
binary-0.7.5.0 (new version)
haskeline-0.7.2.1 (reinstall) changes: directory-1.2.2.1 -> 1.2.1.0
optparse-applicative-0.11.0.2 (reinstall) changes: process-1.2.3.0 -> 1.2.0.0
tasty-0.10.1.2 (new package)
tasty-silver-3.1.7 (new package)
unordered-containers-0.2.5.1 (reinstall) changes: hashable-1.2.3.3 -> 1.2.2.0
Agda-2.4.3 *test (reinstall) changes: binary-0.7.1.0 -> 0.7.5.0,
haskeline-0.7.1.2 -> 0.7.2.1, process-extras-0.3.3.4 added, tasty-0.10.1.2
added, tasty-silver-3.1.7 added, temporary-1.2.0.3 added,
unordered-containers-0.2.4.0 -> 0.2.5.1
cabal: The following packages are likely to be broken by the reinstalls:
idris-0.9.18.1
vault-0.3.0.4
wai-extra-3.0.8.0
wai-3.0.3.0
wai-logger-2.2.4.1
uniplate-1.6.12
cheapskate-0.1.0.4
trifecta-1.5.1.3
semigroups-0.16.2.2
void-0.7
lens-4.9.1
contravariant-1.3.1.1
semigroupoids-4.3
reducers-3.10.3.2
profunctors-4.4.1
free-4.12.1
kan-extensions-4.2.2
adjunctions-4.2.1
bifunctors-4.2.1
comonad-4.2.6
charset-0.3.7.1
parsers-0.12.2.1
aeson-0.9.0.1
Use --force-reinstalls if you want to install anyway.

Original comment by jmchap...@gmail.com on 14 Jul 2015 at 10:46

GoogleCodeExporter commented 9 years ago
From #14, could you install Agda using

  $ make install-bin CABAL_OPTS='--constraint=tranformers==0.4.3.0 --force-reinstalls'

?

Original comment by andres.s...@gmail.com on 14 Jul 2015 at 12:05

GoogleCodeExporter commented 9 years ago
I built agda, but I have been left with broken packages.

Original comment by jmchap...@gmail.com on 14 Jul 2015 at 12:39

GoogleCodeExporter commented 9 years ago
> I built agda,

Good.

> but I have been left with broken packages.

I know you can install some of these packages using the new version of 
transformers.

Other option is to install Agda using cabal sandbox.

Which command did you use for getting the error in #0?

Original comment by andres.s...@gmail.com on 14 Jul 2015 at 1:06

GoogleCodeExporter commented 9 years ago
There was a typo in 'tranformers' in the command in #15, the right command is

  $ make install-bin CABAL_OPTS='--constraint=transformers==0.4.3.0 --force-reinstalls'

so, it seems you installed Agda using transformers 0.3.0.0...

I'm testing the installation using GHC 7.8.3 and transformers 0.3.0.0... 

Original comment by andres.s...@gmail.com on 14 Jul 2015 at 1:25

GoogleCodeExporter commented 9 years ago
I could install Agda with GHC 7.8.3 and transformers 0.3.0.0 using the command 

  master$ make install-bin CABAL_OPTS='--constraint=transformers==0.3.0.0 --force-reinstalls'

Could confirm it, please.

Original comment by andres.s...@gmail.com on 14 Jul 2015 at 1:34

GoogleCodeExporter commented 9 years ago
That works too.

Original comment by jmchap...@gmail.com on 14 Jul 2015 at 5:47

GoogleCodeExporter commented 9 years ago
It seems the issue was fixed, so I'm closing it.

Original comment by andres.s...@gmail.com on 14 Jul 2015 at 6:07

GoogleCodeExporter commented 9 years ago
thanks for your help!

Original comment by jmchap...@gmail.com on 14 Jul 2015 at 6:12