search

mit-plv / coqutil

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

Partial compatibility with Coq 8.11 #40

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

On top of #38 and #39

Remaining errors are: File "src/coqutil/Ltac2Lib/Msg.v", line 4, characters 2-16: Error: Unbound value List.fold_left File "src/coqutil/Ltac2Lib/Constr.v", line 19, characters 4-22: Error: Constructor Unsafe.Fix expects 5 arguments, but is applied to 4 arguments File "src/coqutil/Ltac2Lib/Log.v", line 4, characters 33-47: Error: Unbound value List.fold_left File "src/coqutil/Tactics/Records.v", line 38, characters 13-24: Error: Unbound value Array.empty File "src/coqutil/Word/ZifyLittleEndian.v", line 19, characters 0-30: Error: Zify InjTyp: no table or option of this type

And also the fixable: https://github.com/mit-plv/coqutil/blob/7969ad785931cb7eb42daeefbd6fbf951ac1fea5/src/coqutil/Datatypes/List.v#L561 Error: This command does not support this attribute: export. [unsupported-attributes,parsing]

andres-erbsen commented 3 years ago

Okay, it looks like we'd need to version-gate everything that depends on Ltac2 or ZifyClasses. I don't remember knowingly using any of these, but perhaps @samuelgruetter knows from the top of the head something common that indirectly depends on them?

samuelgruetter commented 3 years ago

ZifyLittleEndian is used on my liveVerif branch branch, and the Ltac2 code was used to simplify parameter records, but since https://github.com/mit-plv/bedrock2/pull/195, it might be the case that Ltac2 is not used any more in bedrock2, but I'd still like to be able to start using it again later.