[Agda] using agda

Jeremy Dawson Jeremy.Dawson at anu.edu.au
Tue Jul 16 05:56:15 CEST 2019


Hi,

I believe I have successfully installed Agda as per the instructions at
https://agda.readthedocs.io/en/latest/getting-started/installation.html
namely
  sudo apt-get install agda-mode
    sudo apt-get install agda-stdlib
but trying it out as per
https://agda.readthedocs.io/en/latest/getting-started/hello-world.html
ie by running
agda --compile hello-world.agda
gives the error
Failed to find source of module IO in any of the following
locations:
   /home/users/jeremy/agda/IO.agda
   /home/users/jeremy/agda/IO.lagda
   /usr/share/libghc-agda-dev/lib/prim/IO.agda
   /usr/share/libghc-agda-dev/lib/prim/IO.lagda
when scope checking the declaration
   open import IO

In fact /usr/share/libghc-agda-dev/lib/prim
exists, as follows:
jeremy at cecs-042179:~/agda$ cd /usr/share/libghc-agda-dev/lib/prim
jeremy at cecs-042179:/usr/share/libghc-agda-dev/lib/prim$ ls
Agda
jeremy at cecs-042179:/usr/share/libghc-agda-dev/lib/prim$ ls -l
total 4
drwxr-xr-x 2 root root 4096 Feb  8  2018 Agda
jeremy at cecs-042179:/usr/share/libghc-agda-dev/lib/prim$ ls -l Agda
total 8
-rw-r--r-- 1 root root  885 Jan 13  2016 Primitive.agda
-rw-r--r-- 1 root root 2269 Jan 13  2016 Primitive.agdai

trying alternatively in emacs, doing  emacs hello-world.agda
and then C-c C-x C-c
creates a directory MAlonzo and puts a mass of stuff in it (totalling 
15MB) then gives this error message
Compilation error:

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

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

What seems to have gone wrong?

Thanks

Jeremy


More information about the Agda mailing list