[Agda] Compiling HelloWorld

[Guillaume Allais]

It is documented in the installation part of the manual:
https://agda.readthedocs.io/en/latest/getting-started/installation.html

On 15/04/2020 21:34, James Wood wrote:
> 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://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C529b3df72677467d180a08d7e16dc7cc%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637225733929675666&sdata=qqFM%2FCGror9fAlq%2BQych4ugpzCT%2FWbBaJXFOg%2FZ2SsE%3D&reserved=0
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>