search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.66k stars 632 forks source link

[8.20] Update compat infrastructure prior to branching #19026

Closed proux01 closed 1 week ago

proux01 commented 2 weeks ago

In a PR on master, call dev/tools/update-compat.py with the --release flag; this sets up Coq to support three -compat flag arguments including the upcoming one (instead of four). To ensure that CI passes, you will have to decide what to do about all test-suite files that mention -compat U.U or Coq.Compat.CoqUU (which is no longer valid, since we only keep compatibility against the two previous versions), and you may have to ping maintainers of projects that are still relying on the old compatibility flag so that they fix this.

(c.f. https://github.com/coq/coq/issues/18882 )

proux01 commented 2 weeks ago

@silene (8.20 coRM) this is ready

@JasonGross please update your review status

silene commented 2 weeks ago

I don't understand why you are removing the file CompatOldOldFlag.v instead of updating it.

proux01 commented 2 weeks ago

The script removes it because then it would become identical to CompatOldFlag.v

silene commented 1 week ago

@coqbot merge now