Stream: math-comp users

Topic: OrdinalOrder


view this post on Zulip Pierre Jouvelot (Dec 17 2021 at 14:44):

I'm able to perform an Import Order.NatOrder., but this doesn't seem to work with Import Order.OrdinalOrder.Is this because I'm still using Coq/ssreflect/mathcomp 8.13? I didn't manage to locate the log for changes.

view this post on Zulip Laurent Théry (Dec 22 2021 at 15:01):

it seems lots of things have been added to order.v in 1.13. (see changelog). Which version of mathcomp are you using?

view this post on Zulip Pierre Jouvelot (Dec 22 2021 at 15:13):

Thanks for the log URL. My default.nix file mentions pkgs.coqPackages_8_13.mathcomp. What would be the best way to test the version this corresponds to?

view this post on Zulip Pierre Jouvelot (Dec 22 2021 at 19:59):

Pierre Jouvelot said:

Thanks for the log URL. My default.nix file mentions pkgs.coqPackages_8_13.mathcomp. What would be the best way to test the version this corresponds to?

Haha, I see that Print LoadPath mentions a mathcomp-all-1.12.0!

Now, I just need to upgrade my nix installation to support 1.13. Any suggestion on how to do this as painlessly as possible? ;)

view this post on Zulip Karl Palmskog (Dec 22 2021 at 20:00):

switch to opam, or use the Coq Nix toolbox? https://github.com/coq-community/coq-nix-toolbox

view this post on Zulip Pierre Jouvelot (Dec 22 2021 at 20:32):

I'm already using nix, which I find really convenient on my Mac. I'll look at the toolbox to see how I can do the upgrade, then. Thanks.


Last updated: Feb 08 2023 at 04:04 UTC