coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [coqdev] deprecation and Coq versions

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [coqdev] deprecation and Coq versions
Date: Mon, 12 Jun 2017 08:46:25 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f175.google.com
Ironport-phdr: 9a23:xxQErx/dW0Ddov9uRHKM819IXTAuvvDOBiVQ1KB42uIcTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsVSmpPXMlfVyJPDIChYYURE+UMJvxXo5XnqlYUsReyGQuhCeXywTFInH/22qg63vw/HwHGxgsgGMoBv3fVrNXwMacdT/q1zKzSwjXFafNdxDDw6JTIch8/pvGAR7NxccvUyUkqFgPIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstg9/oj+qxsg2i4nJgJoYyl/F9SVlwIY1OMa3RFRnbt6jFZtdsTyROYhuQs46XW1kpCI3xqcFtJO7ZiQG1okryh/FZ/CacYWF4hTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG50FNQoSpEltnAr2kN1wDP5sSeRPtx40Ws1DaV2wDc7eFEJk80la7FJJI73rEwkZ8TvVzCHi/whkr2kLebels49uWs8ejqYbXrqoWCO4NpiwzyKLkil86/DOggNwgBRWmb+eCy1L35+k35Ra1HjuE2kqbHt5DWP8Uapq+8Aw9Q04Yu8Bm/DzK839QZmXkLNk5KeBWCj4TxIVHBPOj4Deujg1SriDpk2/fGPqT4DprRKnjDjazucK1m609czQoz1cpQ64hVCrEHOvLzW1X+uMbWDh8jYESIxLPMD8w1/YcDUyrbCaiAdajWrFWg5+Q1IuDKapVD6xjnLP1w2/5vikgLmFoYcLOs1J0RICSkHvlhZVeYZH/tqtgEGGYO+AE5Sbq52xW5TTdPaiPqDOoH7TYhBdfjVN+bSw==

Hi Matej,

When talking about the version number, it should be 8.7 (no v) IMHO. v8.7 is bound the become the branch name and V8.7something a tag. If we stick to this convention, it will be pretty easy to follow (small v and big V for git stuff is useful for auto-completion mostly).

Théo

Le lun. 12 juin 2017 à 10:41, Matej Košík <matej.kosik AT inria.fr> a écrit :

On 06/11/2017 02:58 PM, Gaetan Gilbert wrote:
> How about
>
> [@@ocaml.deprecated "since $version: $reason"]

I see us putting "8.7", sometimes "v8.7", sometimes "V8.7", sometimes "version 8.7" ...
It can still be processed by a human, but I was wondering whether there's a better way ...
(I've heard somebody saying: "Humans are expensive and don't scale very well."
I would say "Humans want to spend their time on more interesting things than sifting through this...")

>
> Gaëtan Gilbert
>
> On 11/06/2017 14:00, Matej Košík wrote:
>> Hi,
>>
>> I am wondering whether it would make sense to add a version information to the deprecated stuff.
>> E.g. here:
>>
>> https://github.com/coq/coq/pull/718
>>
>> I've added dozens of
>>
>> [@@ocaml.deprecated "alias of that"]
>>
>> tags.
>>
>> What's the deprecation plan?
>> How will we know when a given thing was deprecated?
>> This is an necessary (though probably not sufficient) piece of information necessary in order to decide whether given vestige can already be dropped (or not).
>>
>> Is there a precedent to follow? If not, is this an issue that need to be addressed? If yes, how do we want to go about it?
>> (Do we want to use comments? Do we want to use something more structured that can be mechanically processed?)
>

Re: [Coq-Club] [coqdev] deprecation and Coq versions, Matej Košík, 06/11/2017
- Re: [Coq-Club] [coqdev] deprecation and Coq versions, Théo Zimmermann, 06/12/2017