coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 15:50:42 +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-f176.google.com
- Ironport-data: A9a23:2G3uFaLmERQE9sg2FE+R4pMlxSXFcZb7ZxGr2PjKsXjdYENSgWMCz DdKUW3Ub67YMDTxLowgbNy39BhV75PVyYM2TwQd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefRLlbFILas1hpZHGeIcw98z0Iz8wIFqtQw24LhWVnU4 YmaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhnMxT9 5Z/7reMDlkqYfbyyPZBdhpUDHQrVUFG0OevzXmXtMWSywjfcCKpzawxUgc5OooX/usxCmZLn RAaAGpVP1bT2qTsmuj9E7Yy7iggBJGD0Ic3s3dpizjWE/wOTpXKQqGM7thdtNs1rp4TQKaHP pZxhTxHSTqcPCBIKFIrIrkyu9/0qnf7VR9XtwfAzUYwyzGLkFYZPKLWGNHSY5mBQdhftl2Jo 3rPuWX/GBATctKFoQdp6Vqpj+7L2Dr4AcccTeLmsPFth1KXyyoYDxh+uUaHTeeRiVKcZJFtc GcovXQt8vMMpF73a9rxQEjtyJKbhSI0V91VGuw8zQiCzKvI/gqUblToqBYRNrTKU+dmFVQXO k+1c8DBXmMw7eXEIZ6J3vLF8mPoYHl9wXoqPHdcFWM4D8/fTJbfZy8jo/5mGa+xy8T2QHT+m m/U6ic5gLoXgIgA0KDTEbH7b9CE9sehou0dvF2/soeZAuVROd7Ni2uAtwCz0Bq4BNzFJmRtR VBd8yRk0MgADIuWiAuGS/gXEbei6p6taWOA3AU/Rsl5r2/zoxZPmLy8Bhkuei+F1e5UKVfUj LP75Gu9GbcPZiLxNfYvC25PI51ykvCxfTgaahwkRoMWPsIZmP6v8yZpakqdt10BY2B9+ZzTz ayzKJ72ZV5DUfoP5GPvH481iOZ3rghjmz67bc2kl3yPjOvGDFbIGOxtGAbfPogRsvjfyC2Lq IY3Cid/408AOAEISnKHr9B7wJFjBSRTOK0aXOQNKLbYe1I+QDtJ5j246epJRrGJVp99zo/gl kxRkGcDoLYmrXGYewiMdF55b7bjAcR2oX4hbH4jOF+p3z4oZoP2tPUTcJ4+fL8G8u1/zK4sH 6NVJZnYWvkfGC7a/zk9bIXmqNMweRmugzWINXX3bTU6ealmWAGUqMTveRHi9XVVAyfu7Zk+r rSs2xn1W50GQwg+Xs/aZOj+nVy0tHkZ3ul1WhKQcNVUfUzt9qlsKjDw3qdneZFSdU2by2LDh QiMABoeqe3cmKMP8YHE1fKesoOkM+piBU4FTWTW6LCBMyOFrGeuxIl3VvnRIWLQWWbyz6WVZ etPysb6PvBazk1BtJBxEuoywK8zu4nvqrtdwlg2FXnHdQ73WLZpI33DxMoW86MUmeEftgyxV UaCvNJdPOzRas/iFVcQIisjb/iCha5IwGiMtaxtLRWo/jJz8ZqGTV5WY0uGhhtbIeYnK4gi2 +og5JMb5lDtkBYsKdra3ClY+37Wci4FWqQj84gZWcrl01V1jF5FZpPYB2n955TWM4dANUwjI zm1gqvehuQDmhCTLSJrTXWdj/BAgZkuuQxRyANQLVq+nNeY1OQ82wdc8GhqQwlYpvmdPzmf5 oS224xJyaSyE/NAgcFCWyW1GFgECkTGpAr+zFwGkGCfRE6tPoAIwKvRJs7VlH31MUoFFtSYw F1c4GngWDfuOsr220PenGZ7/uf7Q4UZGhLqwaia8gfsI3X+STXgi66qI2EPrnMLxC/3aFLv/ YFXwQq7VUE32eP8bUH250l2GIn8kCy5GVE=
- Ironport-hdrordr: A9a23:dfRGm6rnncbgHwS7Z1wdsicaV5oSeYIsimQD101hICG9E/bo7v xG+c5w6faaskd1ZJhNo6HjBEDEewK+yXcX2+gs1NWZLW3bUQKTRekI0WKh+V3d8kbFh4lgPM lbAs5D4R7LYWSST/yW3OB1KbkdKRC8npyVuQ==
- Ironport-phdr: A9a23:DusnxxPbY8qi9hYLMKAl6nZ2BxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv68r3AGCA9mTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf6+94fQbghJizawYLx/J wiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjU LxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4 LpxSBLwhygHOTw2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc 4YPCfAONvtFoon6vVsOogWxBRKxD+7o0DBIgGX50bcg3OQuDwHJxxctH90LsHvOrdX1ML0eX vyyzKnN1DjOae5d1jjh5obSaB8hve2MUqxqccrX0UQhGB3Ig1uOpIH7PT6Zy/kAvmib4ediW +yil2Eppx9/rzWgyMoglIbHi5wVxF3a6yl0zoc4KNOmREN/fdOpE5lduieHPIV1WsMvW39kt Do+x7EcupO2fDIGxIo5yxLBcfCLboqF7xPlWe2MOzl3nmhld6i6hxuq8Uiv1On8Vs6s3VZPt CVFk93MumkU1xzQ98SLU/V98lqj1DuOzQzT5eZEIUc7larfNZEt2KI/lp0WsUjbHy/2nlv5j LOOe0k65uSl7/7rb7bmq5OGKYN4lB/yPr4zlsG9AOk0Kg0OUHKa+eS42r3j50r5QLBSg/Isl KnWqorWKt4Upq6nGABYyYkj6xOlADen1NQUh2UILFVAeB6fiYjmIEnBIOrkAvenn1SsjDBry ujbMrH5GJXCMmDDkKv9fbZ680NT1A0zzclG651IDrEBPen8V1TqtN3YCx85Kxa7z/zmCNV7z IMeWHiADrWXMKPI4he04bckJPDJb4sIsh78LeIk7rjglywXg1gYKICv1NM9b2q3E+8ud0yfa DzljckLOWgPtws6CuftjQvRAnZoe3+uUvdktXkAA4W8ANKbLmjMqLmI3SPgW4ZTengDEVeUV 3Hha4SDXf4ILiOUOM5o1DIeBvC6U4F08xaouUfhzqZ/aPLO83gRs5ul3ddr7cXckBgz8Xp/C MHOm3qVQTRMl3gTDyQzwLg5pEV8zlmZ1q0tivpRU9Vc+flhXQIzNJqaxOt/WJjpQgyUWNCPR R69R8m+RzE8StVk29gVf0N0AMmvlDjG1iuuRqYWzvmFXcNqtK3b2Hf1KoB2zHOuOLAJqV4gT 4MPMGSngvU67A3PH8vSlF3fka+2dKMa1SqL9WGZzGPIslsKGAh3Gb7IW3wSfC605Zzw+1/CQ rmyCL8mLhoJyMiMLbFPY8HoilMOTenqOdDXaWa802mqAhPAyrSJZYvsM2ITuUeVQEECmkYa8 miMHQc7Dyal5WnZCX0mFF7iZV/t7fgrsGmyHQc/ywCHaVEk1qLgoEZEw6zBDalJhPRd53lyz lc8VEyw1N/XFdea8g9ofaEHJMg4/E8CzmXB8Qp0Ip2nKalmwF8YaQV++U30hHAVQs1Nl9Ynq HQywU98M6WdhRlIcTre1J/uMJXYL2Dz+FakbKuciTS8mJ6Gv7wC7vg1sQCptQegUEMt7X9P3 Nxc0n/a7ZLPRllaQdf6VUA58AJ/rrfRb3wm5o/a4nZrNLG9rj7I399B6PIN8h+7ZJ8fNaqFE FS3CMgGH421L/RsnVG1bxUCNeQU9aguPsrgeeHUkKKsOe9hmnqhgwElqMh01EvK/iViQMbH2 p8Ex7eT2Q7PWzrnjVinu9z6gsgePWBUTjf5k3K+QtcOOOV7Zs4TBH2rItGry9kb5dalQHNe+ FO5RhsH1MKvZRuOfgn41AxU214QpC/vki+5wjpo1jAx+/DHjWqenqK4LkBBYzEVFwwAxR/2L IO5js4XRh2tZgktz16+4FrigrNcvOJ5JnXSRkFBe273KXtjW+2+rOnnAYYH5ZU2vCFQSOn5b 0qdT+u3qh0TlSrsAWF2yzUydjXssZL81U8f6irVPDNooXzVdNsljx7Z7ZrVSuBb9jUDTSh8z zLQAxLvd8ns9tKSmZDZt+m4XG/0TZxffx7gyoaYvTe672lnUnjd17ij38fqGg8g3WrnxsFnA G/W+Q3kbNChhOyqdPhqdU5yCBrg5tpmT8tgx5Aoish1uzBSh43JryFa1z6iaZMBhf24ND1XG XYK24KHvlSjghY4aCvXn8ShESzMisp5O4vkPCVPgnh7t4YST/3Mid4M1Spt/gjm80SLPak7z m9bkbx0sDYbm71b51Brl3nbW+FIWxEfZHyklgzUvY/i6vwNOSD3N+D3jRQb/5jpDane8FgEC DCgJchkTWkoqZ8meFPUjC+qtdqiIYiMK4pV7lrNzV/Bl7QHcspg0KpXw3M9aSSl+iR6roxzx R12gcPg5dbBdjUrpfPjREYfb2y9ZttPqGu00+AExZfQhNrpRtI4S30dVZ/sB5pECRo0svLqf 0aLGTw48TKAHKbHWBSY8AFgpm7OFJaiMzeWImMYxJNsXkvVIksXmw0SUDgg+/xxXgm32Mzsd lt47TEN9xb5rBVL0OdhKxj4VC/Wug6pbj4+TJXXIgBR60lO4ELcMMrW6ewWfWkQ5pq6sAmEM XCWfSxNBGANH1WHXhXtZ+bwo9bH9OecC6y1KP6PKbSCpOpCVuuZkJKi1ow1mlTEfs6LP3RkE 7g6wh8ZBSE/S5mfwW9VDXVIyXGoDYbTvhq39yxpo9rq9f3qXFmq/o6TE/5JNs0p/RmqgKCFP urWhSBjKD8e2IlfoB2AgLUZwlMWjDljMje3FrFV/yfLReTZlbFdJxEeYiJ3csBP6uhvu2sFc d6ekd7z2rNi27QtDExZUFX6hsyzTckDImX4LVCeQUjSa+rAKjrMzMX6J6i7TPcD6Ycc/w31s jGdHUj5Oz2FnDS8TBGjP9ZHiySDNQBfsoWwGv6MIW3qTdajcx7iddEu0mNwzroziXfHc2UbN GokG6uihrKV5CJcxP54Hj4YhpKABeaBkiedqeLfL8RO2cY=
- Ironport-sdr: Q1O5htugPKtF3uVbll5Bon/ZSe7zAnVvQVsx6XfmdruCn8mg77wsXb7JydIIYSlrNWROajKG8g pxKZhz/hatJBmGMF2bwUNcnAT5dh/gZ6zc6LQq1tETfjdeGIr3QcxhuxE/etKu7QYJu1ReKz2H HafvWl9j9TWFp6rpVqha6P7ck9VGJd1WLJ2Ntng5QWGI8VPbm38AHfNNZ5Pj9sBsqkPR8X8hgj 2weYdQEk2VbiSaTv/ohBwbEZAjxbcGq2hBcaG6t6ogTLb5mTY6W+en99Tv0xyfgxyuUZ7k1+hg xNr1o7TdNOY65HXR1DsrF0pB
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
- [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Timothy Carstens, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Tej Chajed, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Vedran Čačić, 02/19/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ralf Jung, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Freek Wiedijk, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ana Borges, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ana Borges, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Freek Wiedijk, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Ralf Jung, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Pierre Courtieu, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Vedran Čačić, 02/19/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/21/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Tej Chajed, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/18/2022
- Re: [Coq-Club] ensuring .v files have no query commands, Timothy Carstens, 02/18/2022
Archive powered by MHonArc 2.6.19+.