[Agda] Compiling HelloWorld

[Herminie Pagel]

Thank you for the discussion, I will add this to the update proposal of the
Hello World example:
https://github.com/agda/agda/projects/8

Am Do., 16. Apr. 2020 um 12:13 Uhr schrieb Guillaume Allais <
guillaume.allais at ens-lyon.org>:

> 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
> >
> _______________________________________________
> 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/8e59ec9f/attachment.html>