Haskell compiler fails while compiling a Modified Alonzo program

Question

I am trying to setup an ArchLinux Virtual Machine for Agda. So far, I've installed both the required dependencies and Agda itself, however I get an Haskell GHC error when I try to compile a simple Hello World program written in Agda. Here follows the scenario description.

The Virtual Machine has been arranged using Vagrant. My provisioning script performs the following package installations:

pacman --noconfirm -Syyu
pacman --noconfirm -Sy ansible vim nano unzip wget git make gcc clang dnsutils
yes | pacman -Sy virtualbox-guest-utils
pacman --noconfirm -Sy emacs
pacman --noconfirm -Sy ghc-static ghc-libs ghc
pacman --noconfirm -Sy cabal-install    
pacman --noconfirm -Sy agda
pacman --noconfirm -Sy agda-stdlib

Once the vagrant up process completes, I do a SSH login and I try to build and launch a simple Agda helloworld application, to see if everything went ok. The silly application is the following:

module helloworld where
open import IO

main = run (putStrLn "Hello World")

To compile it using Agda I am using the following command:

agda -i /usr/share/agda/lib/ -i . -c helloworld.agda

However, when the compilation runs, I come with the following error:

Calling: ghc -O -o /vagrant/helloworld -Werror -i/vagrant -main-is MAlonzo.Code.Qhelloworld /vagrant/MAlonzo/Code/Qhelloworld.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[ 1 of 78] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
Compilation error:

MAlonzo/RTE.hs:5:1: error:
    Could not find module ‘Numeric.IEEE’
    There are files missing in the ‘ieee754-0.8.0’ package,
    try running 'ghc-pkg check'.
    Use -v to see a list of the files searched for.
  |
5 | import Numeric.IEEE ( IEEE(identicalIEEE) )
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I tried to install the ieee754 using cabal, but it says that the package is already installed.

Do you know how can I get rid of it? Am I missing something?

Here it is the GitHub repo containing the virtual machine. In order to reproduce the problem it is enough to follow what is described in the readme file of the repository.

P3trur0 P3trur0 · Accepted Answer · 2018-04-09T07:34:05

As suggested on this issue on Agda GitHub page, it seems a problem related to Agda version 2.5.3.

In order to fix that I've replaced cabal-install with stack instead. I mean:

pacman --noconfirm -Sy stack

Then, after the provisioning execution, I followed the GitHub comment suggestion saying:

just tell stack to install these packages: stack exec --package ieee754 --package text agda. Executions after this can be made using just stack exec agda.

Doing so, I was able to install both the missing packages for a proper MAlonzo compilation.

Haskell compiler fails while compiling a Modified Alonzo program

1 Answers