Syntax notations for … Z, … are no longer available merely by Requireing the files that define the inductives. You must Import … Coq.ZArith.BinIntDef, …, respectively, to be able to use these notations. Note that passing -compat 8.8 or issuing Require Import Coq.Compat.Coq88 will make these notations available. Users wishing to port their developments automatically may download fix.py from Python script taking a log of `make` on stdin, which adds imports to fix numeral notations · GitHub and run a command like while true; do make -Okj 2>&1 | /path/to/fix.py; done and get a cup of coffee. (This command must be manually interrupted once the build finishes all the way though. Note also that this method is not fail-proof; you may have to adjust some scopes if you were relying on string notations not being available even when string_scope was open.)
But afterwords, I tried using the python script linked above, and later, just manually importing Coq.ZArith.BinIntDef but to no avail. Is there a better solution to overcome this problem than definining manual notations like I did?
Hi @kartik, my understanding of this excerpt of the release notes is that it is about notations for numerals, not about the aliases of the kind Zle := Z.le and so on.
These aliases are removed for deprecation reason and the python script has no effect on them. The intended fix is to replace every occurrence of Zle by Z.le and so on.
I’m not directly involved in this change though. Then cc to @JasonGross.
Thanks for the clarification, Hugo. I wasn’t completely sure, but this was the only relevant note I found about Z-related deprecation in 8.10 release notes. On v8.9 I only got warnings “compatibility-notation,deprecated” but on 8.10 I got errors instead of warnings. Perhaps release notes should provide some info about migration when warnings are changed to errors (I am aware there is some discussion about better deprecation support in 8.11).
Now that I see further down in release notes of v8.4beta, I realize the right solution is to switch to Z module in the code as you suggested in the PR comment. Thanks!
I must then miss something: in Scala, a feature deprecated in version X.Y must be removed in version X.Y+1 (lest it’s forgotten) — so, you need to fix deprecation warnings in X.Y before upgrading to X.Y+1. What is the Coq policy instead?
I should have read more closely, found the following in 8.10+beta1 notes:
Deprecated compatibility notations have actually been removed. Uses of these notations are generally easy to fix thanks to the hint contained in the deprecation warning emitted by Coq 8.8 and 8.9. For projects that require more than a handful of such fixes, there is a script that will do it automatically, using the output of coqc (#8638, by Jason Gross).
And tried the script by @JasonGross as well, works like a charm!
I think I need to attribute this to my being a beginner to Coq and sometimes it’s difficult to figure out what to look for (like I was looking for Z-related deprecations instead of compatibility-notation deprecation). It didn’t help that when I first started working on this issue, I was already on 8.10.
So indeed, these notations have been removed in 8.10 after being deprecated for a very long time (since 8.4) but only in the two previous versions the deprecated warning was triggered by default. This was mentioned in the release notes as you found out eventually (within the Notations section of the “Other changes in 8.10+beta1” section). The part of the release notes that you initially quoted was actually from the 8.9 release notes. You probably didn’t realize this immediately because you searched the page, and you jumped there. I would rather advise to start by skimming through the release notes, especially the categories that correspond to what you’re looking for (Notations in this case). We should probably work on improving the style of the release notes so that it is easier to spot compatibility breaking changes.
Coq’s policy is that a feature needs to be deprecated in a given version to be removed in the next, but it doesn’t mandate to do the removal immediately, especially when some users explicitly ask for more time.
Among my confusion, I also felt it will be nicer if release notes for each release were on their own webpage so the scope of search is restricted (unsure how easy it is do with Sphinx). However, for now, I will keep in mind to skim the release notes in future.
Thanks for the suggestion. I don’t know if that’s feasible in Sphinx, but I will keep that in mind. For now, I started testing the idea of annotating changelog entries with a type like “Added” / “Deleted” / “Updated”: https://github.com/coq/coq/pull/10931.