[Agda] using agda

[Jeremy Dawson]

Hi Caryo,

Thanks.  I've now upgraded to Fedora 30, including Agda package
Agda-2.5.4.2-17.fc30.x86_64

With this the error message I get on trying
$ agda --compile hello-world.agda
is
Checking hello-world (/home/jeremy/agda/hello-world.agda).
/home/jeremy/agda/hello-world.agda:4,13-15
Failed to find source of module IO in any of the following
locations:
   /home/jeremy/agda/IO.agda
   /home/jeremy/agda/IO.lagda
   /usr/share/Agda-2.5.4.2/lib/prim/IO.agda
   /usr/share/Agda-2.5.4.2/lib/prim/IO.lagda
when scope checking the declaration
   open import IO

When I try emacs hello-world.agda
and C-c C-x C-x
I get (sometimes)
C-c C-x C-c is undefined
and sometimes
Backend (and then a funny symbol)

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

Fedora

Agda is packaged in Fedora (since before Fedora 18).

yum install Agda

will pull in emacs-agda-mode and ghc-Agda-devel.

(does this also pull in the standard library?  I don't see how to tell.
If so, where would it be?  The instructions at 
https://agda.readthedocs.io/en/latest/tools/package-system.html
presuppose that I know where it is)

Incidentally, it doesn't also pull in emacs-agda-mode

Regards,

Jeremy

On 20/7/19 1:56 am, Caryo Scelus wrote:
> On Fri, 19 Jul 2019 01:35:24 +0000
> Jeremy Dawson <Jeremy.Dawson at anu.edu.au> wrote:
> 
>> Thanks.
>>
>> Distro is DISTRIB_DESCRIPTION="Ubuntu 16.04.4 LTS"
>>
>> version of agda seems to be Version: 2.4.2.5-1build1
> 
> And an old library; yeah, i'd say that's too old to bother fixing
> (but if you really want, check out that old thread). Perhaps the most
> balanced way is to install Agda from hackage (via cabal or stack);
> alternatively you can try installing newer debs (from fresher ubuntu or
> debian), but that obviously might run into issues.
> 
>> 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
>>
> 
> Although latest version is 2.6.x, this is more reasonably recent. Do
> you experience both errors there? (first should be solvable, as i
> mentioned in previous message, by setting up stdlib path/dependency)
> What are messages exactly?
>