[Agda] failure of cabal install Agda

[Michel Levy]

I have try this

michel at M1330:~$ cabal install gitrev
Resolving dependencies...
All the requested packages are already installed:
gitrev-1.3.1
Use --reinstall if you want to reinstall anyway.

And reinstall is not a command for cabal.

Le 18/03/2020 à 17:15, Andreas Abel a écrit :
> > There are files missing in the ‘gitrev-1.3.1’ package,
> >    try running 'ghc-pkg check'.
>
> Have you tried this?  If the gitrev package is broken, try to install
> it with
>
>   cabal gitrev
>
> or
>
>   cabal gitrev-1.3.1
>
> On 2020-03-18 17:08, Michel Levy wrote:
>> 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
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr