Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Michael Soegtrop <MSoegtrop AT Michael-Soegtrop.de>
  • To: coq-club AT inria.fr, Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
  • Subject: Re: [Coq-Club] Facing Strange Error Trying to install VST
  • Date: Mon, 28 Sep 2020 15:24:38 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=MSoegtrop AT Michael-Soegtrop.de; spf=None smtp.mailfrom=MSoegtrop AT michael-soegtrop.de; spf=Pass smtp.helo=postmaster AT mo4-p00-ob.smtp.rzone.de
  • Ironport-phdr: 9a23:D+ZdNBC5nEgw5vP43YgcUyQJP3N1i/DPJgcQr6AfoPdwSP37osmwAkXT6L1XgUPTWs2DsrQY0rWQ6f6rBTVIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLF/IA+ooQjQucUbjpZuIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1kyoMKSI3/3/LhcxxlKJboQyupxpjw47PfYqZMONycr7Bcd8GQGZMWNtaWS5cDYOmd4YBEvQPPehYoYf+qVUBoxSxCguwC+3g0TJImn370Lcm3+g9HwzL3gotFM8OvnTOq9X1Mb8fX+e0zKbUzTXMde1Z2TPg44bVdRAuv/6MXa5qccrW0UkkCgTIgFKNp4ziITyV2fgNs3Kc7+p4Tu+hjG8npB1xoje12MgsjpDFiJ8Syl/a+iV53Jw1JdqgSEJhfNGrDoJduieHPIR5Xs0sWXtnuDomyrIYo567ejAHxYg6yhPQaPGKfYaF7g/9WOuQPzp1hXJodKyjixi870StyPDwW8iq3FhFsyZIj8TBu3MD2hLT5MWKSf9w81m/1DuJygvd5OZEIUUumqraLZ4s2r8wlpwJsUTCBCD6gkv2jLWQe045+eao8/zqb7b7qpOGKoN5iwXzPr4zlsGwAOk0KBUCUmmF9eikyrHs51H1TKtPg/A1j6XVrI3VKMEUq6GkDQJV3IMu5AiwAji409kVmGIIIV1BdR6ZioXkNE/CL+vlAfq6jFmjjilky+zDM73vH5nCM37Om6r7c7ln8U5T0g8zwMhf551KDrEBJ+r+Wkr2tNHXFxM5KxC4z/r+BNV6zYwSQ3mPAqqFMKPKq1OI/OMuI+6KZIALojryNuYq6+bvjX8/h1AdYbGk0JgKZHyiA/hrIkGUbWDxjtoOEGoGpBcyQe30hFGaVD5cfXeyX6Yy5jEhD4KmCJ/OSIewjryGwii7EYFWZnpBClCUCnrocoSEVOsMaC2IPMBhliUIVaOmS4A/2hGuqBX6y71/LubO5yIXq4rv1MJp6O3LiREy6Tt0AtyB3GGKVmF4h38HRzsr3K9kukF90VeC0a1gg/NCD9BT5vVJUh07NZHG1eB6BcryCUr9eYKCT0/jSdG7CxkwSMgwypkAeQI1MtqkjwvD2C/iKL8ci6CMHJU48rPVzjClLsl7ym3G06wJhFwnBMJEc2yg0P1R7Q/WUqvImEWQmqLiTqMR0zLX83/LmU+1u0xXTBR3SY3gXHsfb0bS6O/+60zeVbi2T7gqZFgSgfWeI7dHP4W6xW5NQ+3ubZGHOzroxzWAQC2Qz7bJV7LEPn0H1X+EWm0FmAAa8HLDDg8zCTu7pHqYADE8TQu+MXOpyvF3rTaAdmFxygiLa0N70L/vo0wQhPecQv4Xm6kDtSg9sTJsWlqwjYqPVoiw4jF5daAZWusTpVdK0WWD6V54OcDlN/g6w1kUNR9yo1uozQdwDIgGncV49X4=

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



Archive powered by MHonArc 2.6.19+.

Top of Page