coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

coq 8.13 support #97

Closed vzaliva closed 3 years ago

vzaliva commented 3 years ago

Please add support for Coq-8.13. The current OPAM version supports up to 8.12.

vzaliva commented 3 years ago

I quickly tried to compile /master/ branch with 8.13 and it emits a lot of warnings (mostly about hints) but compiles OK.

spitters commented 3 years ago

Should work already. Maybe opam update ?

"coq" {(>= "8.11" & < "8.14~") | (= "dev")} https://github.com/coq-community/math-classes/blob/master/coq-math-classes.opam

Zimmi48 commented 3 years ago

No @spitters, the problem is that the latest release is 8.12.0, which is not marked as compatible: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-math-classes/coq-math-classes.8.12.0/opam Only the master branch is. We should:

spitters commented 3 years ago

Thanks @Zimmi48 . You can probably do that with your eyes closed. Could you do it? I'd need to look up the precise steps.

Zimmi48 commented 3 years ago

Sure, I will take care of it.

vzaliva commented 3 years ago

Anything I can help with? I am stuck as my project dependency now requires 8.13 while I am also using math-classes.

Zimmi48 commented 3 years ago

Sorry about the delay @vzaliva. I released a new 8.13.0 version (https://github.com/coq-community/math-classes/releases/tag/8.13.0). Are you used to opam packaging? If yes, then you should be able to create the PR updating the opam-coq-archive yourself.

vzaliva commented 3 years ago

thanks. yes I can prepare and submit OPAM package update.

vzaliva commented 3 years ago

https://github.com/coq/opam-coq-archive/pull/1722