[Agda] failure of cabal install Agda

[Andreas Abel]

 > 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
>