Error running the installer script about platform HOT 3 CLOSED

@Agnishom : sorry for the very long response time - we have been busy.

The root cause for this is that you at some point in the past added a Coq repository for opam 1.2 to your opam 2.X. I guess you have been following some outdated instructions to install some package.

We treat this as an exceptional case - in case it happens to other users as well we will add a sanity check with a more user friendly error message.

The solution would be to call opam repo remove coq-released, but this might have some side effects.

from platform.

Just wanting to report that I encountered a similar issue. I have had a working opam-based setup for a while, but wanted to switch to the platform instead, and ran into the problem that my coq-extra-dev repository was pointing to http://coq.inria.fr/opam/extra-dev instead of https://coq.inria.fr/opam/extra-dev (the difference is in the http vs https). It looks like an exceptional case indeed, but having some kind of informative error message would avoid having to discover this closed issue.

from platform.

@MevenBertrand : OK, I re-opened this issue. I will add a sanity check for the default repo names.

from platform.