<div dir="ltr"><div dir="ltr"><div>Thank you for the discussion, I will add this to the update proposal of the Hello World example:</div><div><a href="https://github.com/agda/agda/projects/8">https://github.com/agda/agda/projects/8</a></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Do., 16. Apr. 2020 um 12:13 Uhr schrieb Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org">guillaume.allais@ens-lyon.org</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">It is documented in the installation part of the manual:<br>
<a href="https://agda.readthedocs.io/en/latest/getting-started/installation.html" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/latest/getting-started/installation.html</a><br>
<br>
On 15/04/2020 21:34, James Wood wrote:<br>
> I'm sure we document this somewhere, given that it's a problem<br>
> absolutely everyone comes across when they try to compile anything for<br>
> the first time. But in two minutes I can't find it, and it really should<br>
> be mentioned near the “Hello, World!” example at<br>
> <a href="https://agda.readthedocs.io/en/latest/tools/compilers.html#example" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/latest/tools/compilers.html#example</a>.<br>
> <br>
> James<br>
> <br>
> On 15/04/2020 19:49, Philippe de Rochambeau wrote:<br>
>> cabal install ieee754 did the trick.<br>
>><br>
>> This is the first time I use cabal.<br>
>><br>
>>> Le 15 avr. 2020 à 20:12, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" target="_blank">phiroc@free.fr</a><br>
>>> <mailto:<a href="mailto:phiroc@free.fr" target="_blank">phiroc@free.fr</a>>> a écrit :<br>
>>><br>
>>><br>
>>> Hello,<br>
>>> compiling the following code from the 2.6.1 Agda Documentation causes<br>
>>> the below error message.<br>
>>><br>
>>> /module HelloWorld where open import <a href="http://Agda.Builtin.IO" rel="noreferrer" target="_blank">Agda.Builtin.IO</a> open import<br>
>>> Agda.Builtin.Unit open import Agda.Builtin.String postulate putStrLn :<br>
>>> String → IO ⊤ {-# FOREIGN GHC import qualified <a href="http://Data.Text.IO" rel="noreferrer" target="_blank">Data.Text.IO</a> as Text<br>
>>> #-} {-# COMPILE GHC putStrLn = Text.putStrLn #-} main : IO ⊤ main =<br>
>>> putStrLn "Hello, World!"/<br>
>>><br>
>>><br>
>>> /Compilation error:/<br>
>>> /<br>
>>> /<br>
>>> /MAlonzo/RTE.hs:9:1: error:/<br>
>>> / Could not find module ‘Numeric.IEEE’/<br>
>>> / Use -v (or `:set -v` in ghci) to see a list of the files searched<br>
>>> for./<br>
>>> / |/<br>
>>> /9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )/<br>
>>> / | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^/<br>
>>><br>
>>> How do you fix it?<br>
>>><br>
>>> Many thanks.<br>
>>><br>
>>> Philippe<br>
>>><br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="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" rel="noreferrer" target="_blank">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</a><br>
>><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>