coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Automated creation of a sed script for replacing deprecated names

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Automated creation of a sed script for replacing deprecated names
Date: Sat, 6 Apr 2019 13:19:59 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga17.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.400.15
Ironport-phdr: 9a23:spno6xW/Z2yASydwsqgvPtrJb5DV8LGtZVwlr6E/grcLSJyIuqrYbRSEt8tkgFKBZ4jH8fUM07OQ7/m5HzRRqsvR+DBaKdoQDkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrssxhfTvndFf+tayGNrKFmOmxrw+tq88IRs/ihNp/4t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+oPM/hFoYnhqVUArhq+ChWjC+700DBEmnv70Lcm3+g9Dw3L2hErEdIUsHTTqdX4LKkeX/2yzKbWwjXDc+lW2TDl6ITQbxsvpvCMUq5wccXL10YvEw3JhUiXpIzgPjOayuQNvHKF4OpkT+6vkGknpB9+ojiz3McsjZHJi5kUylDC6SV23oI1KcekR058ZN6pCZ1dvDyUOYtxR8MtWWBouCAix70Hv567ZikKx449yx7RcfyLa4mI4hT/VOmPJTd0nm9qd6y5ih2v8kag0vXxWtSw3VpUtCZIktnBumoN2hDN8MSLV/tw8lq51TqS1g3e5PtILE46mKbBNZIszLo9moAOvUnAAyP6gFj6ga6Se0k+5OSl6+vqbq/4qpOGKYN4lwfzObk0lMOlG+Q3KA0OUnCb+eui0L3j+lX0QLBFjvIsj6XUsorWJcUdpq6lHQBV1pwv5Aq4DzejyNgYnH8HI0xZeB+fkoTkP0/CLOr4APq/mVihkClny+rbMrDhH5nBNn3Dn63gfbZ55U5c0g0zzdVH6pJRC7EOPPLzVVXvu9zcFBM5KAu0zPjoCNVhzIMeXnqPD7SYMKPUrV+H+OYvL/OQa48SvTbxM+Il6OL2jX8lhV8derGk0ocQaHChB/hpP0GZYWf3jdoaCmcLvg8+TPTwh1GYUD5TYWyyX6Mm6T0hBoKmF9SLeof4yreGxWKwGoBcTmFAEFGFV3nyPc3QUPAVLSmWP8VJkzoeVLHnRZV3hj+0swqvgYFgI+XI4CoA8drG1dN17uDX31lm8D1/D82Q1yeWSGx7gnkPXxc32rxypQp2zVLVgvswuOBRCdEGv6ABaQw9L5OJl7UrWeC3YRrIe5KycHjjR9ynBT8rSddomo0PZVpwH5OpiRWRhnP2UY9QrKSCAdkPyoyZx2L4fp8vynDa2a1nhF4jEJMWaD+Ww5Vn/g2WPLbn1kWUk6HzKvYZ0yeUqyGCy3aDuAdTVwsiCag=

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

[Coq-Club] Automated creation of a sed script for replacing deprecated names, Soegtrop, Michael, 04/06/2019
- Re: [Coq-Club] Automated creation of a sed script for replacing deprecated names, Jason Gross, 04/06/2019
  - RE: [Coq-Club] Automated creation of a sed script for replacing deprecated names, Soegtrop, Michael, 04/06/2019