search

mit-plv / coqutil

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

coqutil.Z.bitblast not found in 8.13 #65

Closed JasonGross closed 1 year ago

JasonGross commented 2 years ago

Fiat Crypto no longer builds with the newest version of coqutil. What happened?

samuelgruetter commented 2 years ago

I guess it's this commit: https://github.com/mit-plv/coqutil/commit/7f87ccb1af3893dce6164a07e0108b50c90489cb I got tired of getting build failures on each push, so I switched from exclude-list to include-list, and treated all legacy versions the same. Which Coq versions are you trying to support in fiat-crypto?

JasonGross commented 2 years ago

8.11 -- master. I'd be willing to bump it up to 8.12 (Debian Stable), since the newest Ubuntu LTS now has 8.15. Could you make sure that the includes list has enough to build everything in fiat-crypto that's in src/Assembly/*.v (don't worry about the subfolders)? That's the only place where we use coqutil on versions of Coq older than what bedrock2 supports

samuelgruetter commented 2 years ago

Does it work with https://github.com/mit-plv/coqutil/commit/aca2540de09587d3a6d2ce999f875058a4578a56 ?