[Agda] Compiling HelloWorld

[James Wood]

I'm sure we document this somewhere, given that it's a problem
absolutely everyone comes across when they try to compile anything for
the first time. But in two minutes I can't find it, and it really should
be mentioned near the “Hello, World!” example at
https://agda.readthedocs.io/en/latest/tools/compilers.html#example.

James

On 15/04/2020 19:49, Philippe de Rochambeau wrote:
> cabal install ieee754 did the trick.
> 
> This is the first time I use cabal.
> 
>> Le 15 avr. 2020 à 20:12, Philippe de Rochambeau <phiroc at free.fr
>> <mailto:phiroc at free.fr>> a écrit :
>>
>>
>> Hello,
>> compiling the following code from the 2.6.1 Agda Documentation causes
>> the below error message.
>>
>> /module HelloWorld where open import Agda.Builtin.IO open import
>> Agda.Builtin.Unit open import Agda.Builtin.String postulate putStrLn :
>> String → IO ⊤ {-# FOREIGN GHC import qualified Data.Text.IO as Text
>> #-} {-# COMPILE GHC putStrLn = Text.putStrLn #-} main : IO ⊤ main =
>> putStrLn "Hello, World!"/
>>
>>
>> /Compilation error:/
>> /
>> /
>> /MAlonzo/RTE.hs:9:1: error:/
>> /    Could not find module ‘Numeric.IEEE’/
>> /    Use -v (or `:set -v` in ghci) to see a list of the files searched
>> for./
>> /  |/
>> /9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )/
>> /  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^/
>>
>> How do you fix it?
>>
>> Many thanks.
>>
>> Philippe
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>