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.
it seems lots of things have been added to order.v
in 1.13. (see changelog). Which version of mathcomp are you using?
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?
Pierre Jouvelot said:
Thanks for the log URL. My
default.nix
file mentionspkgs.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? ;)
switch to opam, or use the Coq Nix toolbox? https://github.com/coq-community/coq-nix-toolbox
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: Oct 13 2024 at 01:02 UTC