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