Julin Shaji (Oct 15 2023 at 16:02): 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.
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
Julin Shaji (Oct 15 2023 at 16:11):Or maybe that file hasn't been updated. Last commit there was 3 years ago.
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.
Pierre Roux (Oct 15 2023 at 16:14):opam show coq-mathcomp-ssreflect.2.0.0
[...]
depends: "coq" {((>= "8.16" & < "8.19~") | (= "dev"))}
Does the dev part mean that it's a current dev version? As in a stable one is not yet in opam?
Pierre Roux (Oct 15 2023 at 16:34):No, it means that it's expected to work on the dev version of Coq.
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
Paolo Giarrusso (Oct 15 2023 at 17:30):(beyond dev)
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: Oct 13 2024 at 01:02 UTC