[Agda] using agda

[Caryo Scelus]

On Tue, 16 Jul 2019 03:56:15 +0000
Jeremy Dawson <Jeremy.Dawson at anu.edu.au> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Hi,

First of all: what distribution (and thus agda package versions) are you
using? If your agda/stdlib packages are old, it might be better to
install new versions from source. I've only used packages from debian
sid and they were mostly fine (there is still one possible issue with
compilation, ieee haskell package is required)

The first error is likely due to need to set up path to stdlib
(perhaps Emacs sets it somehow?.. i don't know). The docs on that can
be found e.g. here:
https://agda.readthedocs.io/en/latest/tools/package-system.html

Your second error looks similar to what can be found in
https://lists.chalmers.se/pipermail/agda/2015/008270.html thread and
if that's the case, best option is indeed to update (ffi directory
mentioned there has been rid of back in 2016).

Hope that helps