coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Facing Strange Error Trying to install VST

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: Michael Soegtrop <MSoegtrop AT michael-soegtrop.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Facing Strange Error Trying to install VST
Date: Mon, 28 Sep 2020 08:34:02 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:u1/YAROiBg0oN68L2mkl6mtUPXoX/o7sNwtQ0KIMzox0I/TyrarrMEGX3/hxlliBBdydt6sbzbCI+Py5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMhm7rArdu8YLjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVQTlgzkbOTEn7G7Xi9RwjKNFrxKnuxx/2JPfbIWMOPZjYq/RYdYWSGxGUchMSixBGZu8YJUTAOodM+hYqIz9qEEPrRu4GAKgAOzixztNinLwwKY00fkuERve0QMvEdIBsnTaotv2OqkPT+660LLFwi/fY/5Mwzrx9JTEfxInrPqRXbxwa83RyUw3Gg7ZgVWQr43lPyiV1uQKtmiQ8vRtVeK1hG47twFxpSCvyd0xhYnJhoMa0FDF/jh+zYkvKt24Tk97YcWkEJtXsiGXLJd5QsYjQ21yoik11qcKuZ+9fCUTzpks2hHQZeCdfYeS/hLjSPieIS1+hH99ZL6zmxS//Eu8x+D/Wce50lZHozRLn9TMuH4D2QHe59WaR/Zy/kmtxDaB2g/P5uxKIU46m6nWJpA9z7MuipcesELOFTL4lkXxia+ZbEQk+u6w5uToY7Xmup+cN5JvhQ3kM6QundSzAeU+MggUXmiU4/6w1LP5/UD/Xb5EjeU2n7HEvJzHJckXvLC1DgBW34o59RqzEi2q3MkbkHUbNF5JZg6LgozzN1zNIP30F+qzjlWtnTtxyP3LPbvsCYjXIHfZirfuZ7N95lZcyAUtydBf4IpZCrQbL/LyXk/9rsDXDho4MwCu2enoFM9x1oIYWW6XA6+ZNr3dsUOQ6+4yPuWBZJUZtCjyJvUm/fLik2I1lUUAcaSqwZcbcHW4Ee5nI0Wdb3rsmNABEWISswUkQ+zqjlyCUSVTZ3a1WqIx/S00CIenDYvZXI+inKaN3Ca9HpFOfGBJFkiMEWv0d4WDQ/oDdCWSItZ4njMYUbihVpQu2Aq1tA76zrpnNvDb9jcZtZLlzth15vfcmQs89TxuXIyh1DSoTmp0l24MDwQx0a9ju0tlggOm6q91jOBCEsR74vJCUg43MdvHyOF1F8r1QkTNc4HaZkyhR4CPDjcwVdI2xpclY09hB9K6hxzDziO7S+scmLqKH5wz94rX2nm3Ls07ynCQh/pptEUvXsYabT7uvaV47QWGQtOQyhjLp+ORba0ZmRX12iKDwG6J5R8KVQdxVePOWHFZb0CQrNKrvhqTHY/rMqwuN0568eDHL6JLbtPzilAfHaXoPdWYamn3mmHiXE/UlIPJV5LjfiAm5AuYEFINyllB9nOHcwE1QCan8TrT

Thanks for following up.

It was pointing to https://coq.github.io/opam-coq-archive/released-opam1.2

I am not quite sure how I got that. I must have set it up while trying to install some package.

On Mon, Sep 28, 2020 at 8:25 AM Michael Soegtrop <MSoegtrop AT michael-soegtrop.de> wrote:

Dear Agnishom,

> By the way, I re-ran the installation script after running `opam
> repository remove coq-released --all` and this time it worked fine.

you mean the Coq platform 8.12.0+beta1 setup script?

It would indeed fail, likely with an unspecific error, in case a
repository with name "coq-released" is registered to opam with an URL
which is not the usual one:

https://coq.inria.fr/opam/released/

I will add a check for this. Can you still tell to what URL the
coq-released repo was set on your computer? Also do you remember from
where you got the URL to which you set the coq-released repo? I guess
you followed some instructions ...

The same is btw. true for the "default" repo.

Best regards,

Michael

[Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/27/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Andrew Appel, 09/27/2020
  - Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/27/2020
  - Re: [Coq-Club] Facing Strange Error Trying to install VST, Michael Soegtrop, 09/28/2020
    - Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/28/2020
      - Re: [Coq-Club] Facing Strange Error Trying to install VST, Michael Soegtrop, 09/28/2020
        
        Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/28/2020