<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>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.</p>
<p>The output of <br>
</p>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">$
sudo apt-get install agda-bin</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">$
agda --version</div>
<p>is <br>
</p>
<p>michel@M1330:~$ agda --version<br>
Agda version 2.5.3</p>
<p>Please, what other packages do I need to install to get a working
Agda prover ?<br>
</p>
<div class="moz-cite-prefix">Le 18/03/2020 à 16:05, Andrés
Sicard-Ramírez a écrit :<br>
</div>
<blockquote type="cite"
cite="mid:CAOUWSGCLuZG4iVnC5XbOAkqWDuBLWR-Fm=dRnKAaL+dWV+Ljqg@mail.gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">Hi
Michel,<br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">It
seems you are mixing the installation of Agda from Ubuntu
packages and from Hackage.<br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">Which
is the output of</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">$
sudo apt-get install agda-bin</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">$
agda --version</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">?</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif;font-size:small">Best
regards,<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Wed, 18 Mar 2020 at 09:29,
Michel Levy <<a href="mailto:michel.levy.imag@free.fr"
target="_blank" moz-do-not-send="true">michel.levy.imag@free.fr</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I
am lost with the installation of Agda. Below I give the log
created by<br>
"cabal install Agda".<br>
<br>
<a class="moz-txt-link-abbreviated" href="mailto:michel@M1330:~/.cabal/logs$">michel@M1330:~/.cabal/logs$</a> more Agda-2.6.1.log<br>
cabal: Entering directory '/tmp/cabal-tmp-11975/Agda-2.6.1'<br>
[1 of 1] Compiling Main (<br>
/tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup<br>
/setup.hs, /tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup/Main.o )<br>
Linking /tmp/cabal-tmp-11975/Agda-2.6.1/dist/setup/setup ...<br>
Configuring Agda-2.6.1...<br>
Building Agda-2.6.1...<br>
Preprocessing library Agda-2.6.1...<br>
[ 1 of 369] Compiling Paths_Agda (<br>
dist/build/autogen/Paths_Agda.hs, dist<br>
/build/Paths_Agda.o )<br>
[ 2 of 369] Compiling Agda.Version (
src/full/Agda/Version.hs,<br>
dist/build/A<br>
gda/Version.o )<br>
[ 3 of 369] Compiling Agda.VersionCommit (<br>
src/full/Agda/VersionCommit.hs, dist<br>
/build/Agda/VersionCommit.o )<br>
<br>
src/full/Agda/VersionCommit.hs:5:1: error:<br>
Failed to load interface for ‘Development.GitRev’<br>
There are files missing in the ‘gitrev-1.3.1’ package,<br>
try running 'ghc-pkg check'.<br>
Use -v to see a list of the files searched for.<br>
cabal: Leaving directory '/tmp/cabal-tmp-11975/Agda-2.6.1'<br>
<br>
Can you help me to solve this problem ?<br>
<br>
--<br>
courriel : <a href="mailto:michel.levy.imag@free.fr"
target="_blank" moz-do-not-send="true">michel.levy.imag@free.fr</a><br>
mobile : 06 59 13 42 53<br>
web : <a href="http://michel.levy.imag.free.fr"
rel="noreferrer" target="_blank" moz-do-not-send="true">michel.levy.imag.free.fr</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
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.<br>
</blockquote>
</div>
<br clear="all">
<br>
-- <br>
<div dir="ltr">Andrés</div>
</blockquote>
<div class="moz-signature">-- <br>
courriel : <a class="moz-txt-link-abbreviated" href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr
</div>
</body>
</html>