[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