[Agda] Compiling HelloWorld

[Philippe de Rochambeau]

Hello,

I’ve managed to reduce the executable's size to 22KB from 1.2MB with the following ghc flags:

agda --compile --ghc-flag='-O2' --ghc-flag='-dynamic' hello.agda

> Le 15 avr. 2020 à 22:51, phiroc at free.fr a écrit :
> 
>  I've noticed that the resulting executable is big too: over 1 MB on a Mac.
> 
> Le 15 avr. 2020 22:34, James Wood <james.wood.100 at strath.ac.uk> a écrit :
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200416/155cf3a0/attachment.html>