coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.9+beta1 is out!

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Ralf Jung <jung AT mpi-sws.org>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.9+beta1 is out!
Date: Fri, 16 Nov 2018 16:07:34 +0100
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-wm1-f45.google.com
Autocrypt: addr=theo.zimmi AT gmail.com; prefer-encrypt=mutual; keydata= xsFNBFP+V00BEADi9eGxuXfvs0HxaYDxrOBpCJWakA4+lCi3KUGqNS5Xq0V7q+BWZZmF/pOO x4EemIickFV+DA/Yp9542XWw1vMK3uGAUpnB4sUvD+qPDnRFHDZH60p1b8rRzukHRdukW33g QsEjDdNp9iVebuBMe+IU2gdpdZxjgxzxShQMIHOX1Az65oC81eEV37XJ7b89WjArEEe0Hxcg 9+jFH3P3pNdlVaxMgEaYxeepTEfBIhWJjobr299gkgUm2a79vYnci0VONNk3crZqpNvrDK9h bqBgsEUv7t8JnIDQOJTncuoeZA+YFkceYKysO4tyDgNPgXSuI8tUfo7eU1uacNvX7LoKH1nT d4Gr26nPUyj8ntnvnT88LK+CxrrfYkUxtK5pYIQLzJSnCaCuoxOu4WJn+6PPtMhUNWC50fmA +HBt3v8YhheNEEbBZPqEGE9O1A0xB5oJJ3UCsf2VpxiEc3qCTzZHPbw5hYsS96MRysJ3gl9Z OG/u8M5r/JlyiDbVOj6WEcjgMYhuowbEX45UCCufgMWlVFDqKj685zCwhPxYSKvW2+Pkvw1K YmM4tQuF3bH2oQXe8W791N39JXQU/LHD7EHnmoJW/6ySc7Mv2f9cId/HY/DeM1U1TTTEEr1Q j6o/6PdRHGWT5PZpbNDy9+sdBieF1JWuXx24KHbhbN/OCebiewARAQABzSdUaMOpbyBaaW1t ZXJtYW5uIDx0aGVvLnppbW1pQGdtYWlsLmNvbT7CwX0EEwEIACcFAli5dBUCGyMFCQlmAYAF CwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQ8XRKCUL1Nsf97A//QpWey31m7X20iHRRO833 BPyziP9QbIQveB8BofZfjWXBJoGExP2EZdb10UMwU0tsnD6NT5E8nKr9rRRTtnwXOcqaQHGd Y4mVLEyJYwZ8g4uZglMyTCHx6k064Ik4c5DysS/15AB72SZm+fJFayIzSY1syvTnTPxTnNx7 l697IbjS3aq3/W+vQ6MwnDgnQqggGMiA0+Tmp5VPCZX9deLmXWC1zeXe/PdCstPzeHTiIHgD wQW+0edCBELbJdhoVBKsQ3OfBK7uMJBXug7zqI3wAoywvd/E12tFzZJhLZiq8arDIimeccf4 bFZUIy17ApiFfAZJU5Rm71H29IFFMTyQxi4QFFiPjWKwtUTDB/Xv6V8nGgdhOHkNgjnRpPn4 jNxSnvr3/f1OW2yGFYyxTUlmYg72eTkSNlPAwd+WA5K3aQQtwUERzhPsK2l4Smjqr7NcI+5X 0aHBVRyRGrTmtTRz/hdyoGoxx4ts1TacquKHx88YH9GZhEng9h+Ak70oQYD9u+atp93wTyTo tghwB5Ewm3O9oruIdQtWx2H4PtP4Y3V1O/DjK42D3wKwikiHisCTKtbuIsgLTnxebWC7wN0q X9nln3KJkEnxZ/6pjLQ3XZB5YeUq58bBnr06VTZYjjYM5aZ6cQrOrnWXvrsrTh367cPKesk5 G5h/itHB0UQc+eXOwU0EU/5XTQEQAL7skL+t5KvE/j2zAzuUFtwjIA+GPBcwOJnITdT3fddN S18gCBx+EH/YPbCphKXOxRFeaD+EDuC1Ls5XK+lYu9hR7rurW7RQI+1XKO7KHQvp4i2I8J4C C+kmMw9K7fysHFG9ckiw1G5WrwiiPZHLadRIAfXwMLoDfRRNu/W8ogjm1m+UWm88DISrkIbE BYEw/fWX8QGGcFvExrFAgXyXXn4vVG90XNre+wJwIADcCqQJXCfzNF/tyetcGEwc3BZiUe/Q Ha/3xLDSm19rDkVWSpWGUr0uSziPSR9kYw6q4F1gKdvex6hnduRMEJLwFRfiHKnHZO2uN8Zj MsB1EklGvkockjkThQfFjeU3zysxfsl4tQRROpglgs1MhiMZpvCdnNTn+Gr+YHQ0sueBxpk0 6GHMmE4C4jcrLFXwfEWOnk6ISHluZS1f9qRnNZzj9ICJItT7cn1KE54jZjmVudi4kOSbihaZ 70PrXMhwphz4nVxSRMIsXdNwSkpCrcOatDS4E7EjRgHW5+CP5WON2aJPD8htAtKNej5nPbTD NFJKz6nG4jdDpxtY0PEkMHarrBpWaIdPEPgdCew5Ns5cAZC0vMkJU8uuSoEumGqzUwdVIWaV p0iZ7MTaWSZeifx7Y6x5YkYR5dMGGzKW5GeLQ7emG0I1BTcFeP+VAGewLA5xWjnhABEBAAHC wWUEGAECAA8FAlP+V00CGwwFCQlmAYAACgkQ8XRKCUL1NscXDRAAx5Y5fyDX/HvFD2Sp4E1h HbtNsPfDQ076U3qvg31e7d5560fW5hwSgZ3++3kGRO7QFTq3edo3oEEWiHuHBJxT7eXSPhXY vsM/atDyQ7Zy6fEUVuv77b3TEDHuWvn4A2kBI+ApCzXohscTuCc/PvVCoDrRQ++be2hIlxsq M7DnRr3/6FI8chCUHj3bXeXtPp8M74/3RGCiwvPZ7825NU0JP6jj1yeEuy6ts/GaZFsDj3sz TxCeZxbdARFxqmT0lf3yF2uQWj35jwqBUC/S+07fZfRRRFXwHTSSzsTTg4JKvsEpq6v0/ryc ETXqwstze+nvPvZ/bLlkiFulLFajYdIky+t5JmjmMEW0/NpK4nRo/QNuTyF1vG1/tjg/q5CZ gW++ZBoYuOR/+roFRPEKIu6Aa843e+QXvpHv4WHN1viH7ufY3D389hKkkhtnEvUu1Mv7ITDD ryw3ok6KFBrjvMQVOp0L7yZc9RYtJ0mXH9n1wWJL94q4hbUJ7fqz2rv8RbTGQoqKfDQVuVuo gH36yLP9s+RKxePuqaTn6DOOHF0/hhMCwes9pWs6ObrEPUVG1YtM6TwopIUJtuLZFWWb3X1Q 4W8EyZElzlCZhLTVhJT7p2k8xBEjpdMpsHhBMjOMljCUeRdJX55g2DVAwx3fvhdOJkuXY5Tl nCgw1L3/lCt46SU=
Ironport-phdr: 9a23:UBGuwBSllgvFu1XlMymmG693N9psv+yvbD5Q0YIujvd0So/mwa6yYBWN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRcDI2iYYsBD+kPM+hWoIbypVQBsQCzBQawCO71zTFEmnH70K883u88EQ/GxgsgH9cWvXrKrNXyLqASXvi2w6nJyDXDau1Z2S346IfSdBAhp+yHULVsccrR10YvEBnJj1SRqYzgOjOV1/8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiIwSylDB7yp5wYA1KMW3SE56fd6kEIZQuDqAO4RqRcMiRmdlszs5xL0eoZO3YjQGxZA9yxPca/GLaZWE7gzgWeqLLjp1hGppdbGiixqo7EStzuLxWtOq3FtItCZJj9nBu3ML2hfO8MaIUOF98V2k2TuX1wDc9OVEIUcsmKreMZEhw7owmoMdsETGAyP6gUv2gaCWe0k+9eio7OPnYrrippCCLYN7lgb+MqE2lsy+B+Q3LBQOUnCF9eig0LDv5070TbVQgvErjKXUs4rWKMsbq6KhBg9ayIcj6xKxDze819QYmGEKLE5FeB2ZiIjlIVDPIPH9Dfe6glShizhrx/XcMb3gBpXBNGTMkLDkfbpl8U5T1BIzzcxD55JTErwOPPXzWlbouNPECh85Lhe7zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK0f7vrgxV0kn1BVKau025Q/bWi5W+95OAOee3W6xp8KFn5PtQ4jRsTrjkeDWHhdfSWcRaU5sw07iYWRP4bGQ423hbWH2m/vAp1bYSZUC1WJEF/ncoyFX7EHbyfEcZwpqSANSbX0E9xp7hqprgKvjuM/drOFqB1djorq0Z1O38OWkBgz8TJuCMHEijOCSmh1miUDQDpkhfkj83w48U+K1O1Du9IdDcZavqobXQIzNJqaxOt/WYirB1DxO+yRQVPjee2IRDE8StVrno0Lakd5Xsqn11XNg3fsDLgSmLiGQpcz9/CE0g==
Openpgp: preference=signencrypt

Hi Ralf,

Yes, that's right, it is #[deprecated(...)] that is meant here. There is
a debate though whether this mention of this experimental feature
belongs to the release notes:
https://github.com/coq/coq/issues/8027#issuecomment-436724533

(although I have been said that I shouldn't discourage users from using
the feature: https://github.com/coq/coq/issues/8027#issuecomment-436196797)

In any case, some clarification is needed.
Théo

On 16/11/2018 15:59, Ralf Jung wrote:
> Hi,
>
>>> What is |#[local]|? Why is there now support for a deprecated thing?
>>
>> Guillaume, could you upload the manual so that we can point people to it?
>> Essentially #[local] is the same as Local and we advise not to rely on
>> it as the feature is completely experimental and the syntax may change.
>> Support for the deprecated attribute means that a deprecated attribute
>> may be attached to tactics defined with Ltac or Tactic Notation to mark
>> them as deprecated. Again, this is documented in the manual (but it is
>> not online yet).
>
> Do you mean a #[deprecated] attribute? What you wrote ("a deprecated
> attribute") makes it look like deprecated here is an adjective referring to
> attribute... Hence me and I guess Beta as well were confused by that
> changelog
> statement.
>
> Kind regards,
> Ralf
>

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Coq 8.9+beta1 is out!, Guillaume Melquiond, 11/06/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
  - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Clément Pit-Claudel, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Ralf Jung, 11/16/2018
      - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/16/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/08/2018