Stream: Coq users

Topic: Getting a running version of coq.8.4.6

view this post on Zulip Yves Bertot (Jun 08 2021 at 09:53):

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.

view this post on Zulip Guillaume Melquiond (Jun 08 2021 at 09:55):

This is an official release, so you will find it in the official repository.

view this post on Zulip Guillaume Melquiond (Jun 08 2021 at 09:55):

https://opam.ocaml.org/packages/coq/coq.8.4.6/

view this post on Zulip Guillaume Claret (Jun 08 2021 at 10:24):

Indeed, the package for Coq itself is not on the Coq opam repository but on the OCaml opam repository (helping discoverability I guess)

view this post on Zulip Yves Bertot (Jun 08 2021 at 10:47):

yes but why does opam say that there is no solution to install coq.8.4.6?

view this post on Zulip Guillaume Melquiond (Jun 08 2021 at 11:01):

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]

view this post on Zulip Michael Soegtrop (Jun 08 2021 at 11:24):

@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.

view this post on Zulip Yves Bertot (Jun 08 2021 at 11:34):

Thanks @Guillaume Melquiond , you probably saved me loads of time

view this post on Zulip Yves Bertot (Jun 08 2021 at 11:43):

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