<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Hello,</div><div class=""><br class=""></div><div class="">I’ve managed to reduce the executable's size to 22KB from 1.2MB with the following ghc flags:</div><div class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">agda --compile --ghc-flag='-O2' --ghc-flag='-dynamic' hello.agda</span></div><div><br class=""><blockquote type="cite" class=""><div class="">Le 15 avr. 2020 à 22:51, <a href="mailto:phiroc@free.fr" class="">phiroc@free.fr</a> a écrit :</div><br class="Apple-interchange-newline"><div class=""><div dir="auto" class=""> I've noticed that the resulting executable is big too: over 1 MB on a Mac.</div><div class="gmail_extra"><br class=""><div class="gmail_quote">Le 15 avr. 2020 22:34, James Wood <<a href="mailto:james.wood.100@strath.ac.uk" class="">james.wood.100@strath.ac.uk</a>> a écrit :<br type="attribution" class=""><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr" class="">I'm sure we document this somewhere, given that it's a problem<br class="">
absolutely everyone comes across when they try to compile anything for<br class="">
the first time. But in two minutes I can't find it, and it really should<br class="">
be mentioned near the “Hello, World!” example at<br class="">
<a href="https://agda.readthedocs.io/en/latest/tools/compilers.html#example" class="">https://agda.readthedocs.io/en/latest/tools/compilers.html#example</a>.</p><p dir="ltr" class="">James</p><p dir="ltr" class="">On 15/04/2020 19:49, Philippe de Rochambeau wrote:<br class="">
> cabal install ieee754 did the trick.<br class="">
> <br class="">
> This is the first time I use cabal.<br class="">
> <br class="">
>> Le 15 avr. 2020 à 20:12, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" class="">phiroc@free.fr</a><br class="">
>> <<a href="mailto:phiroc@free.fr" class="">mailto:phiroc@free.fr</a>>> a écrit :<br class="">
>><br class="">
>><br class="">
>> Hello,<br class="">
>> compiling the following code from the 2.6.1 Agda Documentation causes<br class="">
>> the below error message.<br class="">
>><br class="">
>> /module HelloWorld where open import Agda.Builtin.IO open import<br class="">
>> Agda.Builtin.Unit open import Agda.Builtin.String postulate putStrLn :<br class="">
>> String → IO ⊤ {-# FOREIGN GHC import qualified Data.Text.IO as Text<br class="">
>> #-} {-# COMPILE GHC putStrLn = Text.putStrLn #-} main : IO ⊤ main =<br class="">
>> putStrLn "Hello, World!"/<br class="">
>><br class="">
>><br class="">
>> /Compilation error:/<br class="">
>> /<br class="">
>> /<br class="">
>> /MAlonzo/RTE.hs:9:1: error:/<br class="">
>> / Could not find module ‘Numeric.IEEE’/<br class="">
>> / Use -v (or `:set -v` in ghci) to see a list of the files searched<br class="">
>> for./<br class="">
>> / |/<br class="">
>> /9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )/<br class="">
>> / | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^/<br class="">
>><br class="">
>> How do you fix it?<br class="">
>><br class="">
>> Many thanks.<br class="">
>><br class="">
>> Philippe<br class="">
>><br class="">
>> _______________________________________________<br class="">
>> Agda mailing list<br class="">
>> <a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a> <<a href="mailto:Agda@lists.chalmers.se" class="">mailto:Agda@lists.chalmers.se</a>><br class="">
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
> <br class="">
> <br class="">
> _______________________________________________<br class="">
> Agda mailing list<br class="">
> <a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">
> <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" class="">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 class="">
> <br class="">
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</p>
</blockquote></div><br class=""></div>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>