search

mit-plv / coqutil

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

8.11 compat #45

Closed JasonGross closed 2 years ago

JasonGross commented 2 years ago

I'd like to keep supporting 8.11 for fiat-crypto until Ubuntu 22.04 LTS comes out in April 2022.

samuelgruetter commented 2 years ago

Aah I kind of saw this coming 🙈

This PR would break the bedrock2 compiler , because when I added support for error messages, various files now transitively Require the fwd tactic, which brings in more typeclass instances, which breaks some proofs, and fixing them looked annoying and not the right approach.

Does fiat-crypto need any of the fwd tactic files? If not, you could just add them to this exclude list that we already have:

https://github.com/mit-plv/coqutil/blob/3840130ea685f167318a1674d58b1b851b45d2e0/Makefile#L11-L13

Would that work?

JasonGross commented 2 years ago

That should work; I've updated the PR