installationcabalagdaagda-mode

"Could not load module `Control.Monad.Trans.Maybe'" while trying to install Agda 2.6.1.2


I'm trying to install Agda 2.6.1.2 by following the instructions in the docs, but when running the command cabal install Agda I'm receiving the following error:

src\full\Agda\Utils\Maybe.hs:13:1: error:
    Could not load module `Control.Monad.Trans.Maybe'
    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.
   |
13 | import Control.Monad.Trans.Maybe
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
cabal.exe: Failed to build Agda-2.6.1.2. See the build log above for details.

I'm running Powershell as admininstrator, I've installed GHC 8.10.3 and cabal 3.2.0.0 with Haskell Platform, and I've run cabal update and installed the packages Happy, Alex, and transformers.

I've tried to delete and reinstall everything including Chocolatey, but this did not resolve the issue. Additionally, the instructions linked mention adding Alex and Happy to PATH, but I do not know how to do this.

I've also tried to run cabal install Agda --allow-newer which is similar to a proposed solution here, but this gave me the same error.

Any help would be appreciated!

Full output

PS C:\WINDOWS\system32> cabal install Agda
Resolving dependencies...
Build profile: -w ghc-8.10.3 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.1.2 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     Agda-2.6.1.2 (all, legacy fallback)
Building     Agda-2.6.1.2 (all, legacy fallback)

Failed to build Agda-2.6.1.2.
Build log (
C:\Users\fredr\AppData\Roaming\cabal\logs\ghc-8.10.3\Agda-2.6.1.2-6a86b4da38fd320ba893c286a6f43f9d98f47bb1.log
):
Preprocessing executable 'agda-mode' for Agda-2.6.1.2..
Building executable 'agda-mode' for Agda-2.6.1.2..
[1 of 2] Compiling Paths_Agda       ( dist\build\agda-mode\autogen\Paths_Agda.hs, dist\build\agda-mode\agda-mode-tmp\Paths_Agda.o )
[2 of 2] Compiling Main             ( src\agda-mode\Main.hs, dist\build\agda-mode\agda-mode-tmp\Main.o )
Linking dist\build\agda-mode\agda-mode.exe ...
Preprocessing library for Agda-2.6.1.2..
Building library for Agda-2.6.1.2..
[  1 of 369] Compiling Agda.Interaction.Options.IORefs ( src\full\Agda\Interaction\Options\IORefs.hs, dist\build\Agda\Interaction\Options\IORefs.o )
[  2 of 369] Compiling Agda.Syntax.Builtin ( src\full\Agda\Syntax\Builtin.hs, dist\build\Agda\Syntax\Builtin.o )
[  3 of 369] Compiling Agda.Termination.CutOff ( src\full\Agda\Termination\CutOff.hs, dist\build\Agda\Termination\CutOff.o )
[  4 of 369] Compiling Agda.Termination.Semiring ( src\full\Agda\Termination\Semiring.hs, dist\build\Agda\Termination\Semiring.o )
[  5 of 369] Compiling Agda.Utils.AffineHole ( src\full\Agda\Utils\AffineHole.hs, dist\build\Agda\Utils\AffineHole.o )
[  6 of 369] Compiling Agda.Utils.Applicative ( src\full\Agda\Utils\Applicative.hs, dist\build\Agda\Utils\Applicative.o )
[  7 of 369] Compiling Agda.Utils.BiMap ( src\full\Agda\Utils\BiMap.hs, dist\build\Agda\Utils\BiMap.o )
[  8 of 369] Compiling Agda.Utils.Environment ( src\full\Agda\Utils\Environment.hs, dist\build\Agda\Utils\Environment.o )
[  9 of 369] Compiling Agda.Utils.Except ( src\full\Agda\Utils\Except.hs, dist\build\Agda\Utils\Except.o )
[ 10 of 369] Compiling Agda.Utils.Fail  ( src\full\Agda\Utils\Fail.hs, dist\build\Agda\Utils\Fail.o )
[ 11 of 369] Compiling Agda.Utils.Function ( src\full\Agda\Utils\Function.hs, dist\build\Agda\Utils\Function.o )
[ 12 of 369] Compiling Agda.TypeChecking.SizedTypes.Utils ( src\full\Agda\TypeChecking\SizedTypes\Utils.hs, dist\build\Agda\TypeChecking\SizedTypes\Utils.o )
[ 13 of 369] Compiling Agda.Utils.Functor ( src\full\Agda\Utils\Functor.hs, dist\build\Agda\Utils\Functor.o )
[ 14 of 369] Compiling Agda.Utils.Haskell.Syntax ( src\full\Agda\Utils\Haskell\Syntax.hs, dist\build\Agda\Utils\Haskell\Syntax.o )
[ 15 of 369] Compiling Agda.Utils.IO    ( src\full\Agda\Utils\IO.hs, dist\build\Agda\Utils\IO.o )
[ 16 of 369] Compiling Agda.Utils.IO.Binary ( src\full\Agda\Utils\IO\Binary.hs, dist\build\Agda\Utils\IO\Binary.o )
[ 17 of 369] Compiling Agda.Utils.IO.Directory ( src\full\Agda\Utils\IO\Directory.hs, dist\build\Agda\Utils\IO\Directory.o )
[ 18 of 369] Compiling Agda.Utils.IO.UTF8 ( src\full\Agda\Utils\IO\UTF8.hs, dist\build\Agda\Utils\IO\UTF8.o )
[ 19 of 369] Compiling Agda.Utils.IO.TempFile ( src\full\Agda\Utils\IO\TempFile.hs, dist\build\Agda\Utils\IO\TempFile.o )
[ 20 of 369] Compiling Agda.Utils.IORef ( src\full\Agda\Utils\IORef.hs, dist\build\Agda\Utils\IORef.o )
[ 21 of 369] Compiling Agda.Utils.Impossible ( src\full\Agda\Utils\Impossible.hs, dist\build\Agda\Utils\Impossible.o )
[ 22 of 369] Compiling Agda.Utils.Empty ( src\full\Agda\Utils\Empty.hs, dist\build\Agda\Utils\Empty.o )
[ 23 of 369] Compiling Agda.Utils.Bag   ( src\full\Agda\Utils\Bag.hs, dist\build\Agda\Utils\Bag.o )
[ 24 of 369] Compiling Agda.ImpossibleTest ( src\full\Agda\ImpossibleTest.hs, dist\build\Agda\ImpossibleTest.o )
[ 25 of 369] Compiling Agda.Auto.NarrowingSearch ( src\full\Agda\Auto\NarrowingSearch.hs, dist\build\Agda\Auto\NarrowingSearch.o )
[ 26 of 369] Compiling Agda.Utils.IntSet.Infinite ( src\full\Agda\Utils\IntSet\Infinite.hs, dist\build\Agda\Utils\IntSet\Infinite.o )
[ 27 of 369] Compiling Agda.Utils.Lens  ( src\full\Agda\Utils\Lens.hs, dist\build\Agda\Utils\Lens.o )
[ 28 of 369] Compiling Agda.Utils.IndexedList ( src\full\Agda\Utils\IndexedList.hs, dist\build\Agda\Utils\IndexedList.o )
[ 29 of 369] Compiling Agda.Interaction.Library.Base ( src\full\Agda\Interaction\Library\Base.hs, dist\build\Agda\Interaction\Library\Base.o )
[ 30 of 369] Compiling Agda.Auto.Options ( src\full\Agda\Auto\Options.hs, dist\build\Agda\Auto\Options.o )
[ 31 of 369] Compiling Agda.Utils.Lens.Examples ( src\full\Agda\Utils\Lens\Examples.hs, dist\build\Agda\Utils\Lens\Examples.o )
[ 32 of 369] Compiling Agda.Utils.Map   ( src\full\Agda\Utils\Map.hs, dist\build\Agda\Utils\Map.o )
[ 33 of 369] Compiling Agda.Utils.Maybe ( src\full\Agda\Utils\Maybe.hs, dist\build\Agda\Utils\Maybe.o )

src\full\Agda\Utils\Maybe.hs:13:1: error:
    Could not load module `Control.Monad.Trans.Maybe'
    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.
   |
13 | import Control.Monad.Trans.Maybe
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
cabal.exe: Failed to build Agda-2.6.1.2. See the build log above for details.

Solution

  • The current release of Agda (2.6.1.2) does not support GHC 8.10.3. You need to either use a supported version of GHC (e.g. 8.10.2) or install the development version of Agda from Github (which does support GHC 8.10.3, see https://github.com/agda/agda/issues/5109).