Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ensuring .v files have no query commands

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ensuring .v files have no query commands


Chronological Thread 
  • From: Ana Borges <ana.agvb AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ensuring .v files have no query commands
  • Date: Mon, 21 Feb 2022 16:56:10 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ana.agvb AT gmail.com; spf=Pass smtp.mailfrom=ana.agvb AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f174.google.com
  • Ironport-data: A9a23:mM3FwagIP5pDlR+LD06+qj76X161XhYKZh0ujC45NGQN5FlHY01je htvWTqOOPaKZWWkfNwlO4+2o04Bu5eBnIVmHlBvri4yFnljpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKidUsxIbVcMpB0J0HqPoMZkxN446TSFK1nV4 4mq+ZeGYAXNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ Npln7yaDiMYEaj1m/lHDkdpL39sHPB9weqSSZS/mZT7I0zudnLtx7B3DxhzM9RHpqB4BmZB8 fFeIzcIBvyBr7jukfTrF6823J5ldZa3VG8ckikIITXxBPAvB5nMXa/i6tpR3TN2jcdLdRrbT 5REN2UzPUyojxtnBxQMEcpkscaTr17adwBUqWq8nfVo7D2GpOB2+OG1bIC9lsaxbc5ShwOTo n/M13/oBwkTct2Z0zuMtHy27tIjhgv+UYMWUaS7r7tk2QLPgGMUDxISWB2wpvzRZlOCt8x3A Ww+vQ4fgq0L91HxE4fMY0OqgSO/h0tJMzZPKNES5AaIw6vSxg+WAGkYUzJMAODKUudmG1TGM XfZz7vU6SxTXK69Ei3Cq+/Fxd+mEW1Ecj9YPH5soR4tuoG7+OkOYgTzosGP+ZNZY/XwEDD0h imJ9W0w3upPy8EM0Kq/8BbMhDfESnn1ouwdtlq/soGNtFsRiGuZi2qAtAizARFoct7xc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd9qm/9oi77JdsOuFmSwXuF1O5UJ1cFh 2eD6WtsCGN7YRNGkIcrOdvqU51ypUQePY29CaiFBjaxXnSBXFbfoHsGib+40Gfqn0wh+ZzTy r/KGftA+U0yUPw9pBLvH7l1+eZynkgWnDqPLbimkUnP+efBPBa9FOZdWHPTP7tRxP7V8G39r YwCX+PUkE43eLOlMkHqHXs7dw9iwY4TXsCo9aS6t4erfmJbJY3WI6WPmeh4I9Q9xcy4VI7gp xmAZ6OR83Kn7VWvFOlAQikLhGrHUcktoHQlEzYrOFr0iXEvbZz+vqgafpozO7Ig8bU7n/JzS vAEfeSGA+hOGmyXoWRDMcGlodwwbgmviCKPIzGhP2oycptmcArDpY3pcw7pwy8RA3flrsA5u bChiljWTMNbFQRvBcrbcty1yFa1sSRPke5+RRqaLdxaeUGq+49vcnSjgvgyKsAKCBPC2jrKj 1bMUUlE/bHA+tZn/sPIiKaIq5aSP9F/RkcKTXPG6buWNDXB+jXxzIJFVtGOd2+PWW7x/pKke rwJnfzxNfswnGFKvZB5JLBlwP9s/NDovbJbkl1pEXiXPVSmDrRsfiuP0cVV7PEfw7ZYvU6vW RvK9IAFZfOGP8TqFFNXLw0gN7zR2fYRkzjUzPI0PESqu3MtreTfCR1fb0uWlShQDLppK4d5k +0vj8gbtl6kgR0wP9fa0y1ZqzaWInobX/l1v50WGtW32A8iy1UHeJ+FTyGvv83JZNJLPU0nZ DSTgfOa1bhbw0PDdVs1FGTMjbUB38VQ4EgSwQ9QPUmNl/rEmuQzgE9b/wMxQ1kH1R5Aye9yZ jVmOkAdyX9iJNu0aBWvnlxAGj2twDWc8031jkIKzSjXFhb0EGPKK2I5NKCG+0VxH6ewuNRE1 Onw9YoneW+CkALNMu8aVktsqvilRtt0nuEHsN7yBNyLRvHWfhK86pJDpgM0R9/PDsY4hUmBr u5vlAq1hWsXKgZIy5AG50KmOXj8hfxKyKGugR2swU/RIVzhRQ==
  • Ironport-hdrordr: A9a23:DNkxxKCPLICF+dblHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqy nApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPG RbH5SWyuecMbG3t6nHCcCDfeod/A==
  • Ironport-phdr: A9a23:kZLuSxVbqpmRY0vqy/8sOWu6y+XV8KylXzF92vMcY1JmTK2v8tzYM VDF4r011RmVB9+du6wP1LuempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffRtEiCC+bL5zI xm7rwHcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2Q rJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6 apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b 4wKD+cZIetYqZPyrEYToBu5HwmsC/3gyiRVjXLxx6I61f4uHRvc0wwvAdIBq2/ZrNrwNKgIU OC1yLPEwinEb/NTwDrw7pXDfR89r/+WR71wbdbRxlc1FwPDllidqoLoMjKb2+kNr2WW8fZsW Pyxh2AntQ1/rSWiy8kyh4XXmI4YykzI+ytlzYs2O9C1SlN3bN+kHZZUqi2WK4V7T8U/SG9mv yY6z6cJuZ+9fCUSx5QnxgLfa/yac4eT+B7sSOGRITJ+iXl4e7y/nw6//Va8xuD4TMW501ZHo jBbntXSqHwBzQHf58qIR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5ocq0XDHivvlEXvj 6+aa1wo+ua15+nlbbjqvJCcN4hzigHxNqQhhNazDvg/MggLR2Sb+OK826P//UDhXrlGkvk7n rPavZ3aP8gXuLC1DxFP3oo+6RuyAC+q0NECknkGKFJFdgiHj4/sO1zWOv/4C+2wj062nzdk2 fDJJabsAprILnfZkbfheaxx5FJbyAo21dxf4YlbBakbIP3vQk/xqMDYDhghPgCp2+rnEsly1 psCWWKTBa+UKL/dsViR5u42P+aMYJIVty3mJvg+5//uiGc5lkUHcamo25sXcnG4Ee58L0WXe 3q/yusGRGwNp081SPHgoFyESz9aIXioDIwm4TRuIYSvRa3EXI+gm/TV1SGyWJRZeGpuBVWFE HOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEnGXG7SzrNmKrGR4SgErdf408Az4eTPlBY0/DgyD sKH0mjLQXsn1ngQSWoQ26Zy6Vd41k/FybJx1vVeHJpa6O1Degg/PJ/Yied9DoO6QRrPK++AU 03uWdC6GXc0R9M1zcUJZhN0Hdzkhx/d1QKlBrYUk/qAA5lnurnE0S3XIMBwg23DyLFnj1QiR Z5XMna6g6dk6wXJL4vAkkHcjqXzMKpFg3KL+2CEwm6D+kpfVWacSI3jWnYSLgvTpNX9vQbZS qO2TK8gKk1HwNKDLa1Dbpvoi09HTbHtIoaWZWX5gGq2CRuSo9HEJIP3Z2UQ2jncA0kYgkgS+ 3iBLw03GiampSrXEjVvEVvlZ06k//N5rTu3SUo9zgfCaEMEtfL98xgcw/WTVfk70bcNuSNno DJxXR6809/QF9uctl95ZqwPKdg54VpBySfYr1knZs3mf/0k3ARENV0o4xCLtV0/EIhLnMk0o Wl/yQNzLfndy1Zdb3aD2oi2PLTLK2709RTpaqjM21iY3szFn8VHoPk+tVjnuxmkU0Q49HAym dBT2j2V6YvAJAUXWJP1FE0w8lIpwtOSKjl4/I7S2XB2ZOO9tDaE0t03DsMqzx+he5FUN6bOR 0fiVsYdAcapMukjnVOkOwkFMO5l/6kxJ8q6dvGC1cZHJc5YlSm9xSRC6YF5iQeX8jZkD/XPx 9ADyu2Z2Q2OU3H9ik2gu4b5g9IMaTYXF2u5gS/qYewZLqR0dMACBnmkC8Kyz9R6wZXqXjZU+ UWiCFUPxMKyMUDKPhqtgEsKjx5R+CP70SKjhyR5iTQosraS0Emsi6z5eRwLN3QKDGhugFHwI JSl2tUTXUymdQ8sx1Ou4Uf3wbQepbwqdTGCBxcVOXKsdSc7Dffj09jKK9RC454pryhNBeG1Y FTBD6X4vwNfyCT7WW1X2DE8cTiu/JT/hR1zzmyHfxMR5DLUf999wRDH6ZnSX/lUi3APQiA+g DbJDHCzOtCo+ZOfkJKJ4YXcHyqxE4ZedyXm19bKvS2yo2RlHxeXkPW6m9mhGg8/m3yzx5xhU iPGqwz5a4/g2vGhMO5pSUJvAUf198twHowt9+l4zIFVw3URgY+ZuGYWiWqme8sOwrrwNTBeD S5O2dPe5xLpnVFuPm7cjZysTW2Tm64DL5G7ej9EgX97tpESTv3Is/oc2nEp6lug8VCPPb4nx WxbkKV2riZd2rBBuRJxnHvDROlKRw8Ae3SrzUztjZj2rb0LNjjxN+LshQwuxZb5S+va6gBEB CSmINF7QWkpv585aBWVgDXy8t22J4WWNIhO8EXSy1CZ0Y03YNowjqZY3HI3fzui4jt1jbZ81 0Um3Inm7tHYcCM0rf7/WlgAcWSrL8ILpmO31fcYzpvQhtr/WM0mQ2puPtOgTOr0QmhL67K6Z 0DXQWd68jDCSPLeBVPNsh446SiUQtbwbTfPYyBIhcNrQB3XTKBGqCYTWjhy3pswFwTxgdfkb F88/TcJoFjxthpLzOtscRj5SGbW4gmyOH8yT9CEIRxa4xsnhQ+dONGC7u91AyBT/4Gw5A2LJ GuBYg1UDGYPEkWaDlHnN7Oq6JHO6e+dTua5KvLPZ/2Jp4k8H7+Qwomz14J94zuWHsCGP30nF v5in0QaAiw/FMPelDECDScQkmOFbsKWogu95jwirs2796eOOkqn7o+OBr1OdNR3rkru0OHTa qjK3nw/cGkEhfZujTfSxbMS3UAfkXRrfjipSvEbsDLVCbnXgulRBgIabCV6MI1J6bg9109DI 52+6Ju927hmg/oyE1oAW0bmn5TjbMoDZWiyKlnvC0OCNbDALjrOiZKSA+v0WfhLgeNYugfl8 y6cCFPmNy+fmiPBUhmuNaRVj3jeMkUB5MeydRFiDWWlR9XjIE7eUpc/nXg9xrs6gWnPPGgXP G1nck9DmbaX6DtRnvR1H2EpBp9NIuyNmiLf5O7deM5+WRpDBy11k6dD4y1/xeIKsGdLQ/t6n CaUpdlr8QnOeganxT9uUR4IoTFO1tvjgA==
  • Ironport-sdr: LMnHJaEjfADJS+wF+5TLfv4BgY+BgUZqDYeoRw8m7zt2oWabFXUis4IrFpPTctIyFRRxE32/UC W3d6UwXNKoWcOZqvbeHq0wqdCZ4PPdhTT7hDlgBsUQFo6BwwKpYrkIzQ/YNCUKyGrXwvP05MdE AZFPLTkyDNO/UE0TogY4QP/kTDXKkulsfxRKnSK5BQOEK3kjOrYdsoNL6oNYyFOJJz9xD9ljEs Q+M1yKwVuiY0JqD+fi8Tafzu7yvFvU5q5u2PelQkBxfO41++ErZHVj3To8Hk4eMf/HDhVx4ayB 9wG2Ol/ueyXUuQMlj1rO2slB

After speaking with Freek, I have opened the following issue/wish: https://github.com/coq/coq/issues/15722

On Mon, 21 Feb 2022 at 15:50, Ana Borges <ana.agvb AT gmail.com> wrote:


On Mon, 21 Feb 2022 at 15:10, Freek Wiedijk <freek AT cs.ru.nl> wrote:
Dear all,

>"hate" is not a word I would use (nor has anyone used it in this thread I
>think), but my main issue with them is that they clutter the output of
>`make`, making it harder to see actual warnings or other diagnostics one
>should care about.

What (because of this) would be nice if coq had some
"--silent" flag, that would surpress the output of these
commands.

This sounds awesome. Would you open an Issue with this wish?

Best,
Ana
 

Freek



Archive powered by MHonArc 2.6.19+.

Top of Page