search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Fix an error for coq >= v8.12.2 and other cleanup #19

Closed Columbus240 closed 3 years ago

Columbus240 commented 3 years ago

This adresses the most important incompatibility with coq v8.12.2 (see issue #18). There are still some anomalies and other problems that appear, but large parts of the library build now. I’m pretty certain that the change is backwards compatible with older coq versions, but I haven’t verified.

Columbus240 commented 3 years ago

Hooray for opam switch. I found out that the patch for Isomorphism.v fails for coq v8.10.2 and corrected it.

paulcadman commented 3 years ago

Thank you for sharing this 🥇

Columbus240 commented 3 years ago

Sorry for the mess, I tried to rename the branch for aesthetic reasons. So I could continue working on a branch called master while not affecting this PR. But that didn’t work.

Anyway. I included the patches that add CI, and closed the other PR, because I think CI is absolutely vital for this library.

jwiegley commented 3 years ago

I don't know why I never saw this PR until now, but thank you so much for the work! Independently, this week I fixed the build for all versions of Coq between 8.10 to 8.13, and committed that version to nixpkgs master for those versions.

I will still pull in your CI changes, as that is something I've been wanting, so thank you again for your work, it is very much appreciated.

Columbus240 commented 3 years ago

You're welcome. I'll merge your changes onto mine and maybe propose a new PR.