<div dir='auto'> I've noticed that the resulting executable is big too: over 1 MB on a Mac.</div><div class="gmail_extra"><br><div class="gmail_quote">Le 15 avr. 2020 22:34, James Wood <james.wood.100@strath.ac.uk> a écrit :<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">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>
https://agda.readthedocs.io/en/latest/tools/compilers.html#example.</p>
<p dir="ltr">James</p>
<p dir="ltr">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 <phiroc@free.fr<br>
>> <mailto:phiroc@free.fr>> 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 Agda.Builtin.IO open import<br>
>> Agda.Builtin.Unit open import Agda.Builtin.String postulate putStrLn :<br>
>> String → IO ⊤ {-# FOREIGN GHC import qualified Data.Text.IO 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>
>> Agda@lists.chalmers.se <mailto:Agda@lists.chalmers.se><br>
>> https://lists.chalmers.se/mailman/listinfo/agda<br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> Agda@lists.chalmers.se<br>
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C529b3df72677467d180a08d7e16dc7cc%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637225733929675666&amp;sdata=qqFM%2FCGror9fAlq%2BQych4ugpzCT%2FWbBaJXFOg%2FZ2SsE%3D&amp;reserved=0<br>
> <br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
https://lists.chalmers.se/mailman/listinfo/agda<br>
</p>
</blockquote></div><br></div>