[Agda] failure of cabal install Agda

[Michel Levy]

Thank you really much for your help. Actually, I am not mixing the
installation of Agda from Ubuntu and from Hackage, I have tried (and
failed) successfully the two methods.

The output of

$ sudo apt-get install agda-bin
$ agda --version

is

michel at M1330:~$ agda --version
Agda version 2.5.3

Please, what other packages do I need to install to get a working Agda
prover ?

Le 18/03/2020 à 16:05, Andrés Sicard-Ramírez a écrit :
> Hi Michel,
>
> It seems you are mixing the installation of Agda from Ubuntu packages
> and from Hackage.
>
> Which is the output of
>
> $ sudo apt-get install agda-bin
> $ agda --version
>
> ?
>
> Best regards,
>
> On Wed, 18 Mar 2020 at 09:29, Michel Levy <michel.levy.imag at free.fr
> <mailto:michel.levy.imag at free.fr>> wrote:
>
>     I am lost with the installation of Agda. Below I give the log
>     created by
>     "cabal install Agda".
>
>     michel at M1330:~/.cabal/logs$ more Agda-2.6.1.log
>     cabal: Entering directory '/tmp/cabal-tmp-11975/Agda-2.6.1'
>     [1 of 1] Compiling Main             (
>     /tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup
>     /setup.hs, /tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup/Main.o )
>     Linking /tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup/setup ...
>     Configuring Agda-2.6.1...
>     Building Agda-2.6.1...
>     Preprocessing library Agda-2.6.1...
>     [  1 of 369] Compiling Paths_Agda       (
>     dist/build/autogen/Paths_Agda.hs, dist
>     /build/Paths_Agda.o )
>     [  2 of 369] Compiling Agda.Version     ( src/full/Agda/Version.hs,
>     dist/build/A
>     gda/Version.o )
>     [  3 of 369] Compiling Agda.VersionCommit (
>     src/full/Agda/VersionCommit.hs, dist
>     /build/Agda/VersionCommit.o )
>
>     src/full/Agda/VersionCommit.hs:5:1: error:
>         Failed to load interface for ‘Development.GitRev’
>         There are files missing in the ‘gitrev-1.3.1’ package,
>         try running 'ghc-pkg check'.
>         Use -v to see a list of the files searched for.
>     cabal: Leaving directory '/tmp/cabal-tmp-11975/Agda-2.6.1'
>
>     Can you help me to solve this problem ?
>
>     --
>     courriel : michel.levy.imag at free.fr <mailto:michel.levy.imag at free.fr>
>     mobile : 06 59 13 42 53
>     web : michel.levy.imag.free.fr <http://michel.levy.imag.free.fr>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     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
-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200318/fc40b845/attachment.html>