[Agda] install agda

[Andrés Sicard-Ramírez]

Hi Michel,

In this case, uninstall the Ubuntu packages and install Agda without
sandboxes using

  $ cabal install Agda

On Sat, 2 May 2020 at 14:22, Michel Levy <michel.levy.imag at free.fr> wrote:
>
> Hi Andres,
>
> No I need only the version 2.6.1. But the problem of the emacs mode agda
> remains. This mode in the version 2.5.3 was installed by the ubuntu
> package elpa-agda2-mode.  But now, without this package, where I have to
> install the files of the directory emacs-mode ? It's not explained in
> the agda doc, agda.readthedocs.io. Can you explain, how you installed
> this agda mode on your emacs ?
>
> Le 02/05/2020 à 19:46, Andrés Sicard-Ramírez a écrit :
> > Hi Michel,
> >
> > Do you really need the two versions of Agda installed?
> >
> > I as said, I'm not familiar with installing two versions of Agda in
> > your setup (Ubuntu package and from Hackage).
> >
> > Best,
> >
> >
> > 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.
> >
> >
> --
> 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