search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

Compatibility with older versions of Coq #41

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

If we want to use coqutil in fiat-crypto, we need some subset (and target) of it that builds with Coq 8.9.

In Coq 8.12, build failures are documented in https://github.com/mit-plv/coqutil/pull/38 In Coq 8.11, build failures are documented in https://github.com/mit-plv/coqutil/pull/40 In Coq 8.10, there's at least one issue with lia in List.v, Ltac2 does not exist, and neither does Coq.micromega.ZifyClasses In Coq 8.9, skipn_cons and Z.div_mod_to_equations don't exist

cc @andres-erbsen @samuelgruetter

andres-erbsen commented 3 years ago

Why do we need to support 8.9 in fiat-crypto again? Debian stable seems to have 8.12, Ubuntu LTS seems to have 8.11, and I didn't spot 8.9 in any place I would recognize in https://repology.org/project/coq/versions either.

JasonGross commented 3 years ago

Oh, hey, Debian released Bullseye as stable on August 14th, 2021. So we can finally bump the minimal version of fiat-crypto to 8.11!

andres-erbsen commented 3 years ago

21dbf3bcda2e61ad92a9a0e48e0f3c27b9e09034