Closed SkySkimmer closed 10 months ago
samuelgruetter
commented
10 months ago I would be ok with increasing the minimum required Coq version for coqutil and its dependencies to 8.17 (and I'm excited about new features such as Ltac2 record update syntax and head reduction flags :smiley:) Just checking if that would work for @JasonGross as well?
JasonGross
commented
10 months ago I guess we've already dropped Fiat Crypto support for the version of Coq in Ubuntu LTS (8.15). I would've preferred to stay compatible with Ubuntu LTS and Debian stable, but I suppose it wouldn't be too bad to drop Debian stable and keep Debian testing (8.17). @andres-erbsen what do you think?
I'd also be happy to prepare a setup for versioning some small set of files, if you'd be okay with that @samuelgruetter
andres-erbsen
commented
10 months ago I have no opinion on versions as long as we keep testing against independently maintained packages.
samuelgruetter
commented
10 months ago If it becomes reeeally necessary to version some files, I'd be grateful for your help with that, @JasonGross :+1: But simplicity of the build process is also an important value to me, and here it seems we could get away without having to version any files if we just advance to 8.17, so I'll try and see if that works out
samuelgruetter
commented
10 months ago I merged this PR and propagated it all the way up to rupicola in this rupicola commit. I'll let @JasonGross handle the Coq version bumping and rupicola bumping in fiat-crypto.
JasonGross
commented
10 months ago So, uh, 8.17 and 8.18 are not on opam on Windows. https://github.com/mit-plv/fiat-crypto/actions/runs/6807702619/job/18510989331?pr=1708
8.15 doesn't support Ltac2 record
with(it's in 8.17 https://github.com/coq/coq/pull/16552) Can we increase the minimum supported version? Not sure how to do a backwards compatible patch otherwise.