Hello, I have a version of coq 8.4.6 on one of my machines, apparently compiled last december using the opam techno. I can't find how this was installed. I need this because I would like to duplicate the working environment on another machine. For the working installation, opam list gives the following:
base-bigarray base base-num base Num library distributed with the OCaml compile base-ocamlbuild base OCamlbuild binary and libraries distributed wi base-threads base base-unix base camlp5 7.13 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils coq 8.4.6 Formal proof management system. num 0 The Num library for arbitrary-precision intege ocaml 4.02.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.02.0 Official 4.02.0 release ocaml-config 1 OCaml Switch Configuration ocamlbuild 0 Build system distributed with the OCaml compil
I could not find a coq 8.4.6 opam file in the current version of
opam-coq-archive sur github.
This is an official release, so you will find it in the official repository.
Indeed, the package for Coq itself is not on the Coq opam repository but on the OCaml opam repository (helping discoverability I guess)
yes but why does opam say that there is no solution to install coq.8.4.6?
My first guess would be that your version of OCaml is too recent. I did not actually install it, but on my computer, Opam does find a solution:
$ opam install --switch=4.02.3 coq=8.4.6 The following actions will be performed: ∗ install conf-gtk2 1 ∗ install conf-findutils 1 [required by coq] ↘ downgrade coq 8.5.3 to 8.4.6 ↻ recompile coq-flocq 2.5.2 [uses coq] ↘ downgrade coqide 8.5.3 to 8.4.6 [uses coq] ↘ downgrade coq-mathcomp-ssreflect 1.6.4 to 1.6 [uses coq] ↘ downgrade coq-coquelicot 2.1.2 to 2.1.1 [uses coq] ===== ∗ 2 ↻ 1 ↘ 4 ===== Do you want to continue? [Y/n]
@Yves Bertot : I am currently working on supporting old Coq versions in Coq platform, but I didn't plan to go that far back (my plan was 8.7). Do you think it makes sense to support 8.4 as well?
The Coq platform scripts create a separate suitable opam switch, so that it is easy to install and also to switch between different Coq versions without too much detailed knowledge of opam.
Thanks @Guillaume Melquiond , you probably saved me loads of time
Thanks @Michael Soegtrop, I think your plans to stop at 8.7 are sensible. My needs for a solution for a much older version are not representative and not worth the investment.
Last updated: Dec 05 2023 at 05:01 UTC