coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Freek Wiedijk <freek AT cs.ru.nl>
To: coq-club AT inria.fr
Cc: Vedran Čačić <veky AT math.hr>
Subject: Re: [Coq-Club] ensuring .v files have no query commands
Date: Mon, 21 Feb 2022 15:06:33 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=freek AT cs.ru.nl; spf=Pass smtp.mailfrom=freek AT cs.ru.nl; spf=Pass smtp.helo=postmaster AT smtp3.science.ru.nl
Ironport-data: A9a23:anrnjqhQW0Dme79PZ8MUlD43X161tRYKZh0ujC45NGQN5FlHY01je htvDGzSOaqKNzanedwgaYjnoB4FucPcnYA3SwJpqCA2ECNjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKidUsxIbVcMpB0J0HqPoMZkxN446TSFK1nV4 4mq+ZeGYAbNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ Nplj82tRw43bqv1nsczFAlKKxBlPLwBweqSSZS/mZT7I0zuaH7w264oF0o3MIsT96BtHCdI8 ZT0KhhUNUnF3r3qhunjDLA93azPL+GzVG8bkn96wDzaJf09B4reBaPOjTNd9G1q2p0fTK2GD yYfQSVTQknPSAUUBn0SCLMwkMejl2KuWCIN/Tp5ooJsvzeMkVEouFT3C/LefcXPTsFIlG6Dt 2fe9iL4BAsbPZqR01K4HmmEnerThXi9Q4kTGbuz+7hwnRuVwgT/FSH6S3OB8OS3g1DuXetZC GJT6jgWnLMz5QuSG4yVswKDnFaIuRsVWtx1GuI86R2Qxqe83+p/LjNdJtKmQIB93PLaVQDGx XfUxoOwVG0HXKm9FCLCr+r8QSaaZEAowXk+iTgsay9tDzPLhoAxix/AQ9AL/EWd0ICvRFkcL xiloSwyiq8XhMgHv5hXEHjchi60/d7SRQ844A7aGHi4qAV9DGJEW2BKwQWEhRqjBN/HJrVkg JTis5LEhAzpJcvc/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB43bptfKWa5O BWO4185CHpv0J2CMPMfj2WZVpVC8EQcPY29D5g4k/IePsIgKVHXlM2QTR7MhDCFfLcQfVEXY svELpvxVB72+Ix80SC4D+1bz/lD+8zN7T27eHwP9Dz+ieD2TCfMEd8taQLeBshkvPLsiFiEq L53aprVoz0BC7eWSneMruYuwaUicCJT6Wbe8ZIHL4Zu42NORQkcNhMm6el/I9c8x/wNzI8lP BiVAydl9bY2vlWfQS3iV5ypQOqHsU9XoS1pMCoyE0yv3nR/M4+j4L1PJZAsO6M6supnlKYmQ /4AcsSGI/JOVjWWoGtAN8eh9NRvJEaxmAaDHyu5ezxuLZdvSjvA9sLgYgaypjIFCTC6tJdmr rD5jlHbTJMPSh5MFsHTbP7znVq9sWJNyulpGVHVZN9XIR2+/I9vIi33r/k2P8BdckqenGXGj 16bWE5Kq/PMrok59MjyqZqF94r5QfFjGkd6HnXA6efkPCbXyWOv3ItcXbvaZjvaTm71pP2va OgJnfHxNPoLwARDv4ZmSuc51qci/4CpvLRbwwJvETPRchKtDuo4cHWB2MBOsIxLx6NY6FDpB xjRpoECNOXbIt7hHX4QOBEhMLaJ28YUrSaMv/47F0XN4iIqrqGMVl9fPkTShXUFfqd1Ko4s3 cwopNUSt16kkhMvP9va3DpY8X+Aci4JX6k978BIG4r3klFt0VpDbJrXB2ns/deJb4wUYEUtJ zaVgovEhqhdlxGdLiBtSSCV0LoPn4kKtTBL0EQGeQaDlO3FseBpjhdfxjQASAkInA5M1Ph+O zU1OhQtd7mO5TphmONKQ3uoR1NaHBSc90H8o7fTeLY1k6V8uq3xwGwB1SKl50UF6zkaZTNa8 beTxSD/THDseKkdGwMsDFV9paWLocNZr2X/dAKPRqxp3KXWpRLumem0eCwOr3MLxOsv0Vbfq 7ACEPlYMMXG2O15n0H/I4KBk64NDhaATICHrTeN44tRdVzhlPqONfRi5qx/lg6h5xAHzKNgN /FTGw==
Ironport-hdrordr: A9a23:QjuBxqMoadjPqcBcTsSjsMiBIKoaSvp037Dk7SFMoDhuA6ulfq GV7ZAmPHrP4gr5N0tNpTntAsa9qDbnhPhICOoqTNKftWvdyQiVxehZhOOIrgEIWReOlNK1vp 0BT0ERMrPN5BRB/L/H3DU=
Ironport-phdr: A9a23:BtX2bBz0x7n6rojXCzJ6wVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z haZtasm0Q+BdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR 5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdq72/qx9pDSbAlFhDmwaq5uI RurqgncqtMYipZ4JKYrzRvJrHpIe+BIym5tOFmegRXy6Nqu8ZB66yhftO4v+MBGUaXhYqQ3V qdYAyg8M2A0/8Lkqx/ORhaS63QGU2UWlh1IAxXZ7Bz/Q5z8vDf2uvZ71SKHO8D9ULI6Vim47 6pzRhHmiDkJOSM6/mHZhcN/kL9UrxCvqBFk347YfJuYOOZicq7HY98XQ3dKUMZLVyxGB4Oxd 4sBD/AfMulGrIn2ulsBrRqgCgaxBePvyDxIjWLx0K00yeQuDx/J3A87Et0Sq3TYts/1NLoIX eCzyKnF1DPOZO5Z1jnh8obHaAwhoe2SUrJqd8rc0VciGx3Gg1iRqYLoPy+Y2vkRvmWG4ORtU f+ih3M7pgx/rTaj2Mkih4fGi48a1lzI6Th0zoY1KNGlVEN2Y9+pHZtWuiqHNIV2WtsvT3xmt Son0LEKpJy2cScQxJkp2xLTceGLfoyG7x77V+udPy10iXZqdb6liRu/8VKsxvPiWsS31ltBs zBLncPWtn8X0hze8siHReV5/kemwTuPzAXT6v1cIU06j6bbMIIuwr8umZoVrUvMADX6mF/rj KOMcEUk/vCk6+XhYrr4up+RL5J4hw/jPqg0h8CyA+s1PhIAUmSH4+iwybnu8EPhTLVPlPI2k 63ZsJ7AJcQco660GwFV0pw95BmhDDery8gXnWIdIFJfZRKLlY7pO1XWLPD+Fviwm06snytzx /DaIr3hBY3AImXbnLf7Ybl981JcyBY0zd1H+51UDagBLOvvVU/1qdzXFQQ0Mxe0wubiENVyz JkSWWOJAq+DMaPdq0WE5uw1I7rEWIhAszHkbvMh+vTGjHkjmFZbc7P684EQbSWWBPlrIA2mY Hfgg9UCWTMEpAczT8ThkxuYTHhVYyDhDOoH+jgnBdf+Xs/4TYe3jenZtM/aNphfZ2QcT0uJD W+tbYKPHfEFdCOVJMZl1D0CT7moDYE7hlm1rAGv7b1hI6LP/zEA84r53Y17/eDeljk57npuE oKb1zLFVHl6y1sBXCR+x6VjuQp4w1aH37J/hqlWD9Fe5NtCSUEgKNjay78yEMj8DzrIZczBU 1O6WpOmDDU2G8o22MMLal1hFs+KlRXfx3HsGLQUmrqACdou7+Ta2xAdPu5bzHDLnOkkhlgiG I5UMHG+w7R4/E7VDpLIlEOQk+Crc74d1WjD7jXLy23Gp0xeXANqNMeNFXkCekvbq8j47ULeX vevD7ogKA5I1c+FLONDdNToiVxMQPqrNs7ZZiq9nGK5BBDAwb3pDsKidX8Q0Sb1A1NCiR1V+ 3LHfQkyCyG9on7PWSR0HAGnaEft/O9i7XKjGxZvlkfTMBEnjOLzo09O1pn+A7sJ07kJuTkss WBxFVe5hZfNDsaY4hBmd+NaaM8851FO0STYsRZ8N9quNfMH5BZWfgJpskfpzxgyBJ9HlJ1go mknwQlaIrneyk4HcTfSjtjgf6baLGX/5kXlZbTb11L2283Q4LpJ7vBy+DCB9Em5U0El9Xtgy dxc1XCRs47LAAQlWpX0Sk8r9hJ+qtk2ewEF7pjPnT1pOKiw6HrZ3s4xQfEiwVCmdsteN6WNE EnzFdcbDo6gMr5il1+sZxMCdOdckcx8d828evaF8KWwevx92jSixWhK+4Fy1EuQ+jE0E7WRm c9an7fDhk3eBmy0hUzpqs3tnIFYeTweVnGyzyTpHs80BOU6fIoGD3uvP9ziw9x/g5D3XHsLv FWnBl4AxIqoYU/LNAW7hFIMkx9P5yX2wnjdrXQ8iTwio6uB0Tabxu3jcEBCIWtXXCx4ilyqJ 4GojtccVUzubg4zlRLj61yposoT7Kl5MWTXRl9FOibsKGQ3GKWqu7eBS8VUrok19yNTGrf0c RWBR7jxrgFPmS35EmZd7DsgMSu3/JP91U8f6irVPDN4q3zXftt1zBHU6YnHRPJf6TEBQTFxl TjdAlXvd8ns59ifkI3P9/yvT2/0HIMGajHllMnT0UnzrX0vGxC0mOq/38HqARRvmzGuzMFkD G3JtEquO9Kykf3lbaQ8Jg8wQwWgjqgyUoBmztlp38hWgCdGwMzLuyNdwSCpb51awfysNiJVH GxVmoaHuVS8iB86dyrXldC+CCnV1MJlY5PSjno+4ism9IgKDa6V6OYBhi5puh+iqgmXZ/Fhn zAbwP9o6XgAguhPthB/himaB7kTGwFfM0mO31yQ6MuiqaxMeGu1WaO1yFIl28uqDbyEqQwaQ mu/fJNqESJr78p5OU7ByzWqsdiiIYaMK4lL8ETFyF/JlI03YNopm+APhDZ7NG61pnAjx+Mhz FRv0Zy8oImbOjBt8aa+UVZTMjz4Yd9W+ym41P0H2J/Jg8b0RtM4S25YOfmgBeilGz8Tq/n9Y gOHETlm72yeBaKaBwiUrkFvs3PIFZmvcXCRPngQi9t4F3z/bARShh4ZWDIik9s3DAevkYbva kp05Rga/Rjit11Kzqg7Unu3GneavwquZjouHdKHKwFK6whZ+0rPGdeb8vooWTpT/5CnpwHLM HHdYQACXgRrEgSUQlvkOLep/9zJ9eOVU/G/I/X5arKLseVCVv2MyMHnws588j2LLMnKImh6A qhxxB9YRX4gUZe8+X1HW2kNminKdcLeuBqs5ng9sJWk6PqyEAP3udnWUOIUaIozvUvux//Eb bL15m4xKC4EhMpXnDmRl+RZhQBU0ns+MGPzWbUY63yXFPqJyPEOV0xCN3ojZpIRt/xujE4TZ YbNg9fxnNaQb9YuDktdDhr6kcCkY8cHZXugclXDVh/j3FuuLiaN2dyxZ6fuENW4ac1frFuqp HCdFx27Vgk=
Ironport-sdr: 988c0+sauM3QxvgiATMi9+rOT3md1arrHQpjB9kyXtKs54S8fyLj0/hXnuRHLaZR1NM22T1udE dA8y445Nu+iV+riw9F8HxvZOBa6Q+6cxb/TjJ8mvySI251DNKiSaCyc+FNR8Ig5ycY2LaApEcQ Esr4RVAQsJHOeP60AvmlLllnzPNW0AJZdmJvH7u0S6LZg1HoUV4WOTwAb1xSObc5WwRyqySoEn x/jNivjXDRvNp+kbPiIPWSSDGEdXALj1QaYMqxsrDYKkbrxUW5pxcpht9TFdzciiAyTy4NZe72 YuA6PCQANPb+eP+rR0Rxplpc

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.

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, Pierre Courtieu, 02/21/2022
      - Re: [Coq-Club] ensuring .v files have no query commands, Abhishek Anand, 02/21/2022