search

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

Adapt w.r.t. coq/coq#16004. #111

Closed ppedrot closed 2 years ago

ppedrot commented 2 years ago

Should be backwards compatible.

ppedrot commented 2 years ago

Not sure what is the policy for older versions. I'm a bit surprised that mathclasses still compiles with 8.6, is this really true?

spitters commented 2 years ago

I don't recall dropping support for 8.6 to 8.10, but it looks like the nix file only tests from 8.11, which would be fine with me.

ppedrot commented 2 years ago

I've pushed a patch to be more compatible with older versions, by deactivating the unknown attribute warning. Let's see how it fares, if it compiles up to 8.11 it should be good to go.

spitters commented 2 years ago

Thanks! It works from 8.11. We should probably disable the other builds in CI.

ppedrot commented 2 years ago

OK, so I consider this ready to merge. Deactivating the broken CIs should be performed in its own PR, instead.

Zimmi48 commented 2 years ago

We had dropped compatibility with Coq versions < 8.11 in 8.13.0, but it was reintroduced by a contributor in 8.15.0. It's fine to remove it now. Removing the tests with Coq 8.6-8.10 should amount to reverting #103 (except that there will be a conflict in meta.yml and the opam file).

ppedrot commented 2 years ago

AFAICT even in master these tests are broken. If you look at the output of the CI in this PR, there is already an issue with the Automatic Introduction flag which is unrelated to the patches from here.

ppedrot commented 2 years ago

@spitters ping

spitters commented 2 years ago

Thanks! I'll merge this, @Zimmi48 if you have time, could you send a PR to reverse #103 ?