[Agda] install agda

[Andrés Sicard-Ramírez]

Do you really need the two versions of Agda installed? If so, since we
know you can install both versions, I suggest to remove the version
installed from Ubuntu and install both versions from hackage. I would
start by doing a fresh install of 2.5.3.



On Sat, 2 May 2020 at 12:22, Michel Levy <michel.levy.imag at free.fr> wrote:
>
> Thank you really much for your help. I copied agda and agda-mode in my
> /home/michel/bin directory.
>
> But I have another problem, when I use emacs with a file test.agda :
> File mode specification error: (error The Agda mode’s version (2.5.3)
> does not match that of agda (2.6.1).)
>
> michel at M1330:~$ agda-mode locate
> /home/michel/Agda-2.6.1/.cabal-sandbox/share/i386-linux-ghc-8.0.2/Agda-2.6.1/emacs-mode/agda2.el
>
> What should I do to install the Agda mode's version 2.6.1 ? The files
> for emacs are in the above directory emacs-mode, where to put these files ?
>
> Now the files for emacs are in the directory
> /usr/share/emacs25/site-lisp/elpa/agda2-mode-2.5.3.
>
> > On Sat, 2 May 2020 at 11:05, Michel Levy <michel.levy.imag at free.fr> wrote:
> >> Hence my question: where to find the new
> >> installation in the directory Agda-2.6.1 and how to reinstall the agda
> >> command and the agda mode .
> > The new commands are in the directory `Agda-2.6.1/.cabal-sandbox/bin`.
> >
> --
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
>
> La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.



-- 
Andrés