Stream: math-comp users

Topic: Installation of mathcomp2


view this post on Zulip Julin Shaji (Oct 15 2023 at 16:02):

Can we install mathcomp2 from opam yet?

I'm not sure if I did something wrong, but when I tried with opam, it downloaded mathcomp1.

view this post on Zulip Julin Shaji (Oct 15 2023 at 16:10):

If we were to attempt to compile from source, I guess we should use a specific coq version?

Is coq 8.12 really needed though?
It's mentioned under opam section at https://github.com/math-comp/math-comp/blob/mathcomp-2.0.0/INSTALL.md#compilation-and-installation-of-released-and-current-dev-version-with-opam

view this post on Zulip Julin Shaji (Oct 15 2023 at 16:11):

Or maybe that file hasn't been updated. Last commit there was 3 years ago.

view this post on Zulip Julin Shaji (Oct 15 2023 at 16:12):

Duh.. it's mentioned in that file itself 8.12 is mentioned only as an example...
Sorry for the noise.

view this post on Zulip Pierre Roux (Oct 15 2023 at 16:14):

opam show coq-mathcomp-ssreflect.2.0.0
[...]
depends:      "coq" {((>= "8.16" & < "8.19~") | (= "dev"))}

view this post on Zulip Julin Shaji (Oct 15 2023 at 16:16):

Does the dev part mean that it's a current dev version? As in a stable one is not yet in opam?

view this post on Zulip Pierre Roux (Oct 15 2023 at 16:34):

No, it means that it's expected to work on the dev version of Coq.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:30):

But you should ignore the mention of dev. The quote says the package works with coq 8.16, 8.17, 8.18

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:30):

(beyond dev)

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:34):

As a general rule, if opam suggests a version you don't want, it's probably opam making a bad choice; just pick the ones you want explicitly, in a single command, and/or use opam pin. So for instance opam install coq.8.18.0 coq-mathcomp-ssreflect.2.0.0 coq-mathcomp-algebra.2.0.0


Last updated: Jul 15 2024 at 20:02 UTC