The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

As described in changes (https://github.com/coq/coq/blob/master/doc/sphinx/changes.rst, https://github.com/coq/coq/blob/master/CHANGES.md), there is such a script at https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py

On Sat, Apr 6, 2019, 09:20 Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Club,

 

I thought about writing a script which automatically craeates a sed (or whatever) script from the deprecation annotations in the Coq standard library files – this should be fairly easy and probably saves a lot of time for library maintainers.

 

I have one question regarding the meaning of the annotations, e.g. in https://coq.inria.fr/library/Coq.ZArith.Zabs.html. Some are labeled (compat "8.7"), other are labeled (only parsing). Should such a script only replace the “compat” Notations, or also the “only parsing” notations. Would it possibly make sense to collect such information from various versions of Coq, since, as far as I understand, some notations are removed in the maintenance cycle?

 

And: does somebody already have such a script?

 

Best regards,

 

Michael

 

Michael Soegtrop

 

Principal Engineer

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928