[Agda] using agda

[Jeremy Dawson]

Thanks for that.  I've done that, downloading the library version 0.17 
since it says that works with agda version 2.5.4.2, which is what I have 
installed.

Now agda --compile hello-world.agda

produces a great deal of output, but finally

Calling: ghc -O -o /home/jeremy/agda/hello-world -Werror 
-i/home/jeremy/agda -main-is MAlonzo.Code.QhelloZ45Zworld 
/home/jeremy/agda/MAlonzo/Code/QhelloZ45Zworld.hs --make 
-fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[ 1 of 70] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[ 2 of 70] Compiling MAlonzo.Code.Agda.Primitive ( 
MAlonzo/Code/Agda/Primitive.hs, MAlonzo/Code/Agda/Primitive.o )
Compilation error:

MAlonzo/Code/Agda/Primitive.hs:4:1: error:
     Could not find module ‘Data.FFI’
     Use -v to see a list of the files searched for.
   |
4 | import qualified Data.FFI
   | ^^^^^^^^^^^^^^^^^^^^^^^^^

MAlonzo/Code/Agda/Primitive.hs:5:1: error:
     Could not find module ‘IO.FFI’
     Use -v to see a list of the files searched for.
   |
5 | import qualified IO.FFI
   | ^^^^^^^^^^^^^^^^^^^^^^^

and trying emacs hello-world.agda gets the same result as before

Thanks

Jeremy

On 22/8/19 7:56 pm, Nils Anders Danielsson wrote:
> On 18/08/2019 15.51, Jeremy Dawson wrote:
>> I've looked at the page
>> https://agda.readthedocs.io/en/latest/tools/package-system.html
>> but it says Let’s assume you have downloaded the standard library
>> but I haven't found anything to tell me how to do that, or, indeed,
>> whether I have in fact done so by following the instructions at
>> https://agda.readthedocs.io/en/latest/getting-started/installation.html
>> which says […]
> 
> You can download the standard library from the following page:
> 
>    
> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
>