coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Roux <Pierre.Roux AT onera.fr>
- To: coq-club AT inria.fr
- Cc: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- Subject: Re: [Coq-Club] make proof-general/company-coq stop on warnings
- Date: Thu, 06 Jul 2023 08:56:57 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Pierre.Roux AT onera.fr; spf=Pass smtp.mailfrom=Pierre.Roux AT onera.fr; spf=None smtp.helo=postmaster AT briaree.onecert.fr
- Ironport-data: A9a23:wM97oqv6ehkQ4LMRMc3y7T6BwufnVClaMUV32f8akzHdYApBsoF/q tZmKWmBP6yKZGb8fNwjYYjk8E8FvJ6Ax9FkSFBu+C1nQSkXgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMsspvlDs15K6p4GxA4ARnDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJB09LasF1ssnO2dHp MI/OShVTA2dvdvjldpXSsE07igiBMPxPYoFt3wmyjfUBvs8XdbNWc0m5/cBh2t23JkUW6+PP 4xFAdZsREyojxlnAlYaEogz2t2vm2nXdDtVslvTq7BfD237klQvgemybou9ltqif+xHh3nbj 2b6omnjGQMwad7E72eK2yf57gPItXqnCdNNROLQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA47k2iVNTwGRq+rXWJpAJaVcA4//AGBB+llqHExRu1Kzg+SDcQVvs3rJcUWCIQ7 wrc9z/2PgBHvLqQQHOb076bqzKuJCQYRVM/iT84oRgtv4K9+N1u5v7bZo8/TPPt5jHgMWioq w1muhTSkJ09t6bnPY2H+k3DhC+3q/AlpSZuv12PBgpJAiteb4Wke4Wu6FWz0BqtBIyDT1Cbs XVCnM6T5+0UEdeDjkRhodnh/pn1vJ5p0xWF3zaD+qXNEBz0pxaekXh4um0WGauQGp9slcXVS EHSoxhNw5RYIWGna6R6C6roVZR6kPi5RYi4CK2LBjarXnSXXFHclM2JTRDLt10BbGB2wfxX1 WqzLZb8UylKUsyLMhLmHb1MuVPU+szO7TqPFMGkn0vPPUu2fnOTQKsIKjOzghMRssu5TPHu2 48HbaOikkwPONASlwGLqeb/23hWdylkbX03wuQLHtO+zv1ORDtwUK+One55JeSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLOOy3D6Vs52k2JzItNluO0n0uK9TnpqQGepd9OfFt+OV/xLQmB 7MIaueRMMRpEz7nwjU6aYWijYpAcB/wuxmCERD4axcCfrlhZTfzxPnaQiXV+hIjNBGH7fkFn +X41yfwY4YyeAB5PcOHNNOt1wyQuFYeqsJTXmzJAMdZfXv9wbM3Lifwr+QWJvsUIk7p3Qqq1 AexADYZq9LSooQzzsL7uKCco6qtEMp8BkB/HVSH3Y2pNCLfwHWv8bVAXMmMYzrZcmH+o4emW sl40ND+N6chsGtRko8hDYtu870y1+Hvq5Be0A5gOnfBNHavK7F4J0i5zdt9jbJMypBZqDmJd Bq2oPcCAoqwOeThDFI1DygmZL7a1fgrxx/j3c5sK0D+vCJK7L6LVHtJBCa1iQtfEupREJgky uIfqsIp+1SBqh41AO2n0AFQ1Uqxd0IlbYt2mK0eMoHRjigT9mpjer3ZUy//34GOYY5DM24sO T6lu5DBjLV9mGvHImcBJVrN+e9vlLUPpxF441sQLHuZmtf+p6EW3T8A1R8VXwhq3hF8/OYrA VdSNmpxPrSowzdkoONhTlKcMVhNKzPB83Og1mZTsnPSSneZc1DkLUo/CL6rx18Y+WcNRQpr1 uiU50i9WAm7Yfyr+DU5XHNkjPnRTdZR0Anms+L/FuSnG6gKWxbUspWMV0Ep9SS+WdgQgXfZr 9ZE5OxzMK33FRABqp0BVrW16+4idwCmFkdjH9dRpLgEDEPNSgGUgDKuEX28SulJBv7N8HK7N fBQG9JyZ0y++hqj/jE/LowQEoBwh88stYYjeKu0BGsosIm/jztOsbDR/S36hGQufdFKlJcgG Lz3czmEK3Gig1pVv0Tvr8B0HHWyTvdZRQ/73cGzqP4oEbBaus5SUEgC6JmGlFTLDxlC4DSvo xLlW6/a68dA2LZctdLgPYsbDjrlNO6pcvqD9T6CluhnbPTNAJ/ojBwUoFy2BDZmF+IddPovn IvcreOt+l3OuYs3dGXrm5OhMa1tzufqVcp1NvPHFlVrrRGgauTNvSRao3uZLKZXmuxz/sOkH gu0SPWhfO4vButy+idnVDh8IT08VYLHN6vunHbo5bDEQB0QyhfOI96b5GfkJzMTPDMBP5rlT BT4obCy79Rft55BHwIAG+ogOZJjPVv/QuEzQrUdb9VD4rWA2Ttue4cOlCbMLRnBEHiNCsv3p 5XDSxPzbgj0trugIBS1dWBtlkV/MZq/qbBYkoEhFxpejDa3FmdAI/513VAuFMRPiiKrvH3nT GilUYbhYBkRmRxDdxjm6ZLtRG9zwwDI1sjRflQUwq9fV8t66E5szlesGueMLkqaogfe8dw=
- Ironport-hdrordr: A9a23:SVv0EaqoIp+USmnD/cOddY8aV5oDeYIsimQD101hICG9Ffbo7/ xG/c5rrCMd6l4qNE3I/OruBEDuewK+yXcY2/hyAV7AZniBhILLFvAH0WKK+VSJcEeSl45gPM xbAs9D4ajLfCVHZLHBkXWF+rgbsby6GdiT9J3jJiBWPHpXgn5bgTtENg==
- Ironport-phdr: A9a23:B5U65xxmYoiRrvjXCzJIwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hKZvKUm1QeYFcWDsrQY0beQ6/ihEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba1zI RmssAnctcYajZZ+Jqs11xDFpmdEd/lMyW5nO16enwzw6tus8JJm7i9dp+8v+8lcXKr1eKg1U aZWByk8PWAv483ruxjDTQ+R6XYZT24bjBlGDRXb4R/jRpv+vTf0ueR72CmBIM35Vqs0Vii47 6dqUxDnliEKPCMk/W7Ni8xwiKVboA+9pxF63oXZbp2ZOOZ4c6jAe94RWGhPUdtLVyFZDYyyY YsBAfQfMOhFrYb9qVUBoxixBAawC+3i0SNIi3z03aEmz+gsCwPL0Qo9FNwOqnTUq9D1Ob8IX +C00qbI1y/DYO1L0jnh74jIbx8gquyLULxqcMre11MvFxnbgVmKtYLlOC6V1+sWvmic6epvS /ivhHQ9pwF/uDii38EhgZTGiYwJ0F7L7zl5wJorKt2iTk52edGpHZhMuyyeOIV4Td4uTn91t CokybALupG1cDYUxZon2RPRZfKKfouL7x/nWuucPzN1iWxldb++hhu//0qtxO36W8Kp01hKt jJInsTCu30CzRDf9NWLRuVn8ku83TuDyxrf5+5cLUwpm6fWJIQtzqAtmpYNq0jPAyv7lFnsg KKXcEgv5/Km5P79Yrr8o5+RL490hR/6MqQpgsGwGv44MgkUUGiB5+uzyqfv/Ur/QLpUkvI5j LPZsIzAKcQVvK61Gw5V0oA95BajFzqqzdoVkHYdIF5bZR6LkZLlN0zKLfzkF/uyjEygkDJxy PDHOr3hDI/NLn/GkLr5Z7h96lBTyBApzd9B/Z5aFrYBIO/8W0Lqs9zYCAE2MxauzOr9BtV9z JsSWWSUDaCBKqPdrUeI5v4zI+mLfIIZpS7xK+I56P72kX85hVgdcLG10psQcXC0B+hpI0GEY XX3mdoBCmcLvg8mTOPwklGCUDhTZ2yzX60m/D07BpimXs//QdWmh6XE1yOmFLVXYHpHAxaCC yTGbYKBDs8NZTiIL4dblSEUHeyZSoI7zxzojgjn25JgKOfO82sWr8Swh5BO++TPmERqpnRPB MOH3jTVJ4kVtmYBRjttmbt6vVQ40VCbl65xn/1fE9VXofJPSAYzc5DGnKRhE96nfAXHc5+ST Uq+BM28CGQJT98r2dJIWUFgC/2liB3Z1mykGexdjKSFUaQ96bmUxH3tP4B4wnfC2rMmigweQ 8ZVL2DgvKli5yDUAYPTmgOXjfXibrwSiQjK8mrL1m+SpAdYXQp3BL3CRmwab1DKoM7R7FnDR qWjBPIgNAZKxNSebKVQAjHwpXNBQvqreNHXYmbq3ny1GQ7N3bSUKozjZ2Qa2izZTkkCiQEau 3icZ0A4AW+6rmTSASYLdxqnal7w8eR4tHKwT1MlhwCMYUp70rOp+xkTzfWCQvIX17gAtW8vs TJxVFq62tvXDZKHqW8DNO1kYN4n+loB72XEpyR6OJG6JuZsnB9Wcgh6uV/vywQiEp9JwoAhq HInyhY3KLrNiQgdMWnBh9apa+WRdjqXnljncaPd11DA3czD/64O7K99sFD/pESyEVJk9Xx70 t5T2n/a55PQDQNUX4iiNyR/vxV8ubzeZTEwoo3O0ng5e5G1vyXY1pQTA/Y14hGmcs1Wdq2eX lyXcYVSF421JeomlkL8JCoFMfpI+egOON62X/yA1bSieuh61mHD7ywP8MV21USC8DB5Q+jD0 sMewv2W6QCAUi/1kFarts2fdZlsXTgJBSL/zCHlANUUfahuZcMQDn/oJcSrx9J4jpqrWnhC9 VflCUlUkMOufBOTaRT602gynQwvoHG9gyb+9TtpgxkuqKeF1WrA2azueQEGNWhCWGR5xQ63f c7u1opcBRnwKVRhnQDt/UvgwqlHuKlzSgubCVxFeST7NSAqU6e9sKaDf98a7ZoptStNV+HvK VueS7P7v14by3a6RDcYnmlhMWj74tOlzHkYwCqHIX1+rWTUY5R1zBbbv5nHQOJJmyEBXG9+g CXWAV61O5+o+8+VntHNqLPbNSrpW5tNfC3s1Y7FujG84DggORyyheq+3OfgDBgS1in2zdAsW z+C/3OeKsH7kr+3N+5qZBwiPF7x8dB3XLt5j5sYg5cdw3FciI/frh9l2S/jdN5c36z5dn8EQ zUGlsXU7AbS00pmNnuVxoj9WybV0o57atK9eG9TxjMl4pUAFvKP9LId13gQwBLwvUfLbPN6h DtY1fY+9CtQnbQSoAR0hiSFXuJLQRUeZ3Sw0UrVqYz2pfdQYmu1eP630kdklJavFtTg6kldQ CqrI8t+W3UosoMmbhSRmHzrttO9I4WWN4tJ8ETFy1Gcx+lTI5YsmvdYnydsI3/8oXgsyup9h htruPPy9IHVLnU2uri0CQRFNyHwbsIXvDrqiO4bl8KSlehDB71HHTMGFNvtRPOsS3cJsOj/c h2JCHs6o2uaHrzWGUme7l1npjTBCcLjMXbfP3Qfwdh4IXvVbEVCnAAZWik7lZ8lB0irwsLma kJw+jEW4BbxtBJNzutiMxS3XH3YoU+kbTI9SZ7XKxQzjEkK/0DOLcmX9f5+BQlS5JyotgGAb Gudag9FF31PVFbFT1HvM7+y5MXRpuiVAu3tSpmGKb6KqOFYS7KJ3cf2idcgpW/WcJzeZj8+X JhZkgJZUHt0GtrUgWAKQi0TzGfWatKD4Qy74mtxp9y+9/LiXETu45GOAv1cK4YKmVj+jKGdO uqXnCs8Jyxf08ZG/X7F0qISmmQVljFGcD+gC71GuzSHH8ey0udHSgUWbS9+Lp4C96UnwgxEI tLWkPv/zL9xlPM4TVBDWFfsgN3va9ZAcATffBvXQU2MMrqBPzjCxcr6NLi9RbNnh+JRrxSsu DyfHicL0RyEkTTzXlahK7MV5Ml6FBZEuYinfxsrDm7uR9/8dlu1Ko0v5dXT6boyi2nDc2AGY 2AUTg==
- Ironport-sdr: 64a665bb_NniHcfiR2dmRi6IEdGqoTgOz1vPGoXUMsX5eh7pNZac70r9 AEdqTXgciP/MUmD1xxQf0t4Llrmt932g5XPJMhw==
Le 2023-07-05 20:53, Abhishek Anand a écrit :
Is there a way I can get proof-process-buffer or proof-goto-point to stop
at warnings, similar to how they stop at errors?
Unlike errors, maybe PG can then let the user single step warnings.
Maybe not what you are exepecting but you can at least
Set Warnings "+warning_you_want_to_error".
(or "+all" for all warnings) to make a warning error and then
Set Warnings "warning_you_no_longer_want_to_error".
to make it a warning again.
- [Coq-Club] make proof-general/company-coq stop on warnings, Abhishek Anand, 07/05/2023
- Re: [Coq-Club] make proof-general/company-coq stop on warnings, Pierre Roux, 07/06/2023
Archive powered by MHonArc 2.6.19+.