What is the technique to know what version of math-comp one is using. I have a student who uses Coq as provided by the coq-8.12 package (installed around october 2020). I would like to know which version of math-comp he is using. What command should I tell him to perform?

Installed with opam? Or with the Windows installer?

If it is with opam, `opam list`

should give you the version of all the installed packages.

If it is the Windows installer for Coq 8.12.0 (given the date), then it's mathcomp-1.11.0 (cf. https://github.com/coq/coq/blob/558e8ea1a3c6241251919d3fde61e91e1717afe6/dev/ci/ci-basic-overlay.sh#L13)

Apparently the math-comp version I am looking for is the one that came with the windows installer. Thanks for your answer.

In the future, when your students install the Coq Platform version X, asking how they installed it won't be necessary anymore because the included package versions will be consistent everywhere (and documented in the platform's documentation).

Last updated: Sep 30 2023 at 16:01 UTC