search

agda / agda

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

Failed to build Agda 2.6.1.2 using GHC 8.10.5 #7198

Closed nad closed 3 months ago

nad commented 3 months ago

I tried to build Agda 2.6.1.2 using GHC 8.10.5 and encountered the following error:

src/full/Agda/Utils/Update.hs:23:1: error:
    Could not load module ‘Control.Monad.Trans.Identity’
    It is a member of the hidden package ‘transformers-0.5.6.2’.
    Perhaps you need to add ‘transformers’ to the build-depends in your .cabal file.
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.

I used the following command:

cabal install Agda-2.6.1.2 --program-suffix=-2.6.1.2 -fenable-cluster-counting -foptimise-heavily --with-compiler=<ghc-8.10.5>

The problem seems to come from the following part of Agda.cabal:

https://github.com/agda/agda/blob/022d31c96d7e37edacf05a89bca06fb7592f877f/Agda.cabal#L242-L246

I think we should try to ensure that if Cabal manages to satisfy all constraints, then Agda builds. In this case Cabal started building Agda, but failed when building module 147. If constraints like impl(ghc < 8.10.3) are included, then I think we should also ensure that Cabal does not even try to build Agda for GHC 8.10.$n$, where $n ≥ 3$.

andreasabel commented 3 months ago

I tried to build Agda 2.6.1.2 using GHC 8.10.5

Agda-2.6.1.2 is explicitly deprecated. So we do not fix it. In 2.6.1.3 the problem seems fixed.

if impl(ghc>8.10.3) transformers (>=0.5.6.2) if impl(ghc>=8.6.4) && impl(ghc<=8.10.3) transformers (==0.5.6.2) if impl(ghc>=8.4) && impl(ghc<8.6.4) transformers (==0.5.5.0) if impl(ghc<8.4) transformers (==0.5.2.0)

I think we should try to ensure that if Cabal manages to satisfy all constraints, then Agda builds.

I agree.

Current Agda.cabal does not have the problem of minor GHC version bounds that get outdated by new GHC releases anymore. I dimly remember there was a discussion with @asr that this would be brittle.

andreasabel commented 3 months ago

I think you rediscovered this issue:

nad commented 3 months ago

I searched for things like impl ghc, 'impl(ghc' and transformers 0.5.6.2, but that issue was not part of the results. Could it be that if one links to code in an issue, in such a way that the code is displayed inline, then that code is ignored by the search feature? Is there a way to get the search feature to include the code?

andreasabel commented 3 months ago

I am using search only naively, and I am usually puzzled by the search results.