[Agda] using agda

[Jeremy Dawson]

Thanks.

Distro is DISTRIB_DESCRIPTION="Ubuntu 16.04.4 LTS"

version of agda seems to be Version: 2.4.2.5-1build1

I've just tried here at home, getting a similar error, distro is Fedora 
27, agda version is Agda-2.5.2-9.fc27.x86_64

Thanks

Jeremy

On 07/19/2019 06:21 AM, Caryo Scelus wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>