UCSD-PL/proverbot9001

Some coq packages for coq 8.12 don't exist anymore? coq-smpl=8.12 coq-metacoq-template coq-metacoq-checker

brando90 opened this issue · 3 comments

can't install these:

(iit_synthesis) brando9~ $ opam switch
#  switch    compiler                    description
   coq-8.10  ocaml-base-compiler.4.07.1  coq-8.10
→  coq-8.12  ocaml-base-compiler.4.07.1  coq-8.12
   default   ocaml.5.0.0                 default
(iit_synthesis) brando9~ $ opam install -y coq-smpl=8.12 coq-metacoq-template coq-metacoq-checker
[ERROR] No package named coq-smpl found.
[ERROR] No package named coq-metacoq-template found.
[ERROR] No package named coq-metacoq-checker found.

do I need to go to the url for each and get the commit that works for coq 8.12?

It sounds like you didn't add the coq-released repository to opam, you need to run opam repo add coq-released https://coq.inria.fr/opam/released before you can install those packages.

curious, why doesn't coq instlal everything it needs in one go?

deleted switch and started agian, no issues anymore