coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] make proof-general/company-coq stop on warnings
- Date: Tue, 22 Aug 2023 11:54:12 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f169.google.com
- Ironport-data: A9a23:uLUKpK3ow3zaS1mS1PbD5QB1kn2cJEfYwER7XKvMYLTBsI5bpzUCz GNNDWuCb62MYWT8f9EgaYrl9k8DucDcnIBkGlFu3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn9glaYDkpOs/jY8EM15qyr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW3jmksQxXAYbBNAjosFVIEti8 swicxlYO3hvh8ruqF66Yuxlh8BmK8iyeY1G5CAmwjbeAvIrB5vERs0m5/cChGZ21p0IRKiBI ZNHOFKDbzyYC/FLEk8WBYgkkaGjgWTlbzxVtXqaoKM25y7YywkZPL3FboGEIYTUG5U9ckCwg Vn/+1/bGSMgL8Wvkj+CyHaGrfLypHauMG4VPOTgqqQCbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5Ghq5+TuK50BNHdVXFOI+5UeGza+8Dxul6nYsTTQQWYN28+IPGAdy8 X2otf/uNQY0mejAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQcaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srF/atLNOddjICFaGu 3cAlo6V6+Vm4XCxeM6lEL9l8FKBva3t3NjgbbhHQcFJG9OFpSfLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp7l/a8T4q+D6yINrKih6SdkifXrEmCgmbAjgjQfLQEzMnTx L/BIZvyUShEYUiZ5GHpF7t1PUAXKtAWnDuPH/gXPjyo1r2RYHP9dFv2GArmUwzN14vd+F+92 48HaaOikkwDOMWgOHW/2dBIdjgicyNrba0aXuQNKYZv1CI9SD9/YxIQqJt9E7FYc1N9x7qUo y/jChICoLc97FWeQTi3hrlYQOuHdf5CQbgTZETA5H75gCRxUpXl96oFaZo8cJ8u8eEpn7Y+T OAId4/ESr5DQyjOsWZVJ5Tsjp1QRDLyjyK3Pg2hfGceebxkTFf34dPKRFbk2xQPKSuVjvEAh YOc+DnVe6deeDQ6Pv3qMKqu63iToUkinPlDWhqUA9tLJ2Tp3otYCw3wqf4VJcszBw3J7WaY3 VzOADMzh+rEk6kq+vbn2IGGqIaIFbNlP0x4RmP005e/BRP4zEGCn7BScb+vVi/PcU/J44OeX PVx49CgFewYjXBInpFZEb02/Zkh5tDqmaBW/j5kEFrPcV6vLLFqeVuC4uViqYxPwa1/qyKte 0fS5ORfB6qFCPnlHHEVOgAhSOaJjtMQuzvK6MUKMFfI3zB28JWHQHdtEUG10gIFF4RMMaQh3 esFk+wV4VbmihMVb/C3vhoN/GGIdnE9Q6Ers68BO7DSiy0p9ABmQYfdASrI8p2we41yEk01E AS12ovGpZphn3TnTVRiNELwzdJ8hIsPsi9k1FUtBUqEsfubi+4V3C9+yyUWTANUxCppy+hYY 3ZiC2BpF6ejpRBT2c5JBTGqES58GSzDq1DQykQIpkLdXUKHRmzAF0xjGOevrWQy0XNQQShfx 56ckF3aaDfNeNrj+wcDQmtnlqDTdsNw/Qj8h8yXJcSJMJ0kaz7DgKX1R243hzb4IME23mvrm PJL+btuVKjFKiIgma03JI2E37A2ShrfBmhjQ+lkzZwZD1PnZzC+9jifGX+fIvoXCaTxzna5L MhyKuZkdRe0jn+Opw9GI588GeZ/mfpx6ecSfr/uG3U9jIKeiThX4bbw7Sn1gVE5T+p+yfgdL pzjTBPcM2iyq0YNpUrzgphlAESab+MARjXA58Gu0eBQF5s8oOBmKk4z9b2vvkSqCghs/jPKn QbPe57py/dGzKJylbDNCYRGPR2/cvnoZdSL8SeyktVAVszOOsHwrDEoqkHrEgBVHLkJUfF1q OipnPvo+nja5ZAafnv8mZaTM4Vov+CJQ/txIMb7CFJ4jBmycpbgzDVb8l/pNKETts1W4/eWY jeRaeyyUIUwcMhczngEUBpuOU8RJIqvZ5ixuB7nieqHDyUc9gn1LNmH03vNRkMDfw8qP6zOM CPFi8yM1Pt58rsVXAQlAst4CaBWOFXgAKsqV+PgvAmiU1WHvAmwhavApzEBtxf7U3WKKZOvq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ+sPY5L3f2J4uUyTbCiyCcWLB74JGuKMJZtpUmOL8Q1lA Yh2Fr7M0tyZzZRgROJV7fu+6Qui7u2P3WoGoCgRjOSrayvzwtw2OLhJEw9EVCiBGMbI/KkOy a7ZWkgcKHyGpYXN/QqMtpKb9Nz1fN8i8tnwURqy/Q==
- Ironport-hdrordr: A9a23:cgPHQqNyU1/n68BcTv6jsMiBIKoaSvp037BN7TEIdfU1SL3gqy nKpp4mPHDP+VMssR0b6LK90ey7MBDhHP1OgLX5X43SODUO0VHAROpfBMnZowEIcBeOkdK1u5 0QFZSWy+edMbG5t6vHCcWDfOrICePozJyV
- Ironport-phdr: A9a23:mQf7GROk9gN9kChgWLMl6nbwBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr1QWQFtyKo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6z9pHJfglEmiexbbxvI BiysA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNjzIDZe52VNONkc6/BYd8WWWhMU8BMXCJBGIO8a I4PAvIbM+ZZsYb9vUEOogWjDgSyA+Pv1yVIhmP33aIkzuQqDAbL3BQhH90QqnTUtsv6OL0OX uCy0anI1ynDb/JI1jfg84XIfRUhruuNXbJ0a8be1U4vFwbcg1iWtIfqMC+b2P4XvGiH8+pvS /ivi2g/pgxvvDShxschh5TVio8JxV7J9Th0zZo0KNCmRkN2btGqHZlMuyybM4Z4TN0uT3xqt Sg017AItp61cDUXxZkkyBPSbeGMfYuQ4h/7SuqdPTN1iGhmdb+/nRq+7Emtx+/mWsWp0VtHq ixImcTWuH8XzRzc8M2HR+N9/ki/3TaP0Bje6uReLkA1karXMpkhwr8tmpYKv0TPAy77lUHsg K+ZcUUk/eeo6+D5bbn8upCcMIp0hhn/MqQohMO/Hfw1PhYSU2Wf4+ix173u8VfkTLhLjPA6i LTVvZHeKMgDo662GQ5V0oIt6xalCDem1cwVnWEGLF1bYhKHlZbmN0vSL/D/EPe/mUiskDZ1y PDbJbDhDZDNIWLCkLflZ7py90lcyA8rwdBZ/J1bEqsBL+7rWk/tqNzYCQc0PxGsz+b9FNp9z p8eWX6IAqKBLKzStkaI6vszLOmIeY8aoy3wK+Ml5v7rlX82g0URfaiv3ZsNaXC3BO5qI0uDY SmkvtBUGmAT+wE6UebCiVuYUDcVaWzhcbg742QDCY+8F4qLbYewmqCA0TrzSoVXa3pcBxaHF mrya4SJRt8DbSuTJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBokXw1Lrm3dlxvKjIkA0qsCdzF 4Kb2n2MSGd9miUJQSU31eZxux810U+NhI5/hfEQDtlP/7VRSA5vLZ/R1fZ3Tdv1Rxjdf9qUY FmjS9SiRzo2S4F52McANn50AM7qlRXfx2yvCr4RmaaMAcks86/GxXW3LMFg0WrH2bQJgFwvQ 88JPmqj1eZk7waGIYnPng2CkrqyM6QR2CmY7GCY0W+Hp11VSiZ1WKTBGHcePw7Y9IqooEzFS LCqBPIsNQ4pJdeqDKxMZ5WpiFxHQKymI9HCeyeqnH/2Ax+Ux7SKZY6semMH3SybBlJW2wYUt W2LMwQzHELD6yrXESBuGFTzYkjt7fg2qXW1SVUxxh2LaEsp3qS8+xocj/iRA/0J2bdMtCAko jRyVFGzurCeQ8KBqhB7ceNXZs4n/FZKyErWsgV8OtqrKKUjzl8SfgJrvl//gg1tA9Yl84Bip 3crwQxubKOAhQkZJnXIgNapZOKRczejr3XNI+bM11rT0cib4PIK4fU88BD4uR2xU1El6zNh2 sVU1H2V4tPLChATWNT/SBVSlVAyqrfEby06/46R22drNPz+qj7PwcgkQuAi1wy8ftpCGKyBH Q72VcYdAoL9TY5i00jsdR8CMO1IoeQsPs68bfbA06m2JvphkS+OgmFO4YQ72UWJvXkZKKaAz 9MOxPeW2RGCXjH3gQK6s8z5rotDYCkbAmu1zSWM6Jd5XqRpZs5LDG6vJ5by3dBin9v2XGYe8 le/BlQA0cvveByIblW70xcCnUgQpHWmn2O/wVkW23kxr6eFxiGIyOP/bgYGN3NjS2xrjFOqK o+xx9wXR0mnaQE1mQDtvx6rgfgG4v0hcC+KHxYAdjOTTSkqSqaqs7uef8NDoIgltylaSqX0Y FyXTKL8vwpP1iriG2VEwzVoElPi8p79nhF8lCecNCMp9CufKZw2nEmAooWCFK00vHJOXiRzh DjJC0LpOtCo+Y7RjJLfqqWlUHrnUJRPcC7txIfGtS2h5GQsDwfs+pL70tDhDwU+1jf2ktdwU iCd5g79b5Px2uKxNv99YkhlGXfz7sN7Hsd1lY561/RykTAKw46Y+3YKizK5KdRWw7jzKnEKW CQXwtPIyAfg0UxnaHmOwsiqMxfVitskbN68bGQM3ys75M0fE6aY4otPmi5tq0a5pwbcMrBt2 y0Qwvw05DsGkvkE7UAzmz6FDOlYTiw6dWT80g6F5NekoOBLaXazJPKugVFmk4npDane8FoBH i+oItF4QXA2toIlbBrNyCGhtN2iIoKLK4tN7lvM1E6R6oodYJMpyqhU22w+YTi75Tt9jLRjx R12gcPk4s7ddzQrrPr/WlkCbnX0f59BpWur1PoYx5fMmdjoR8UEeH1DXYO0H630VmtI6LK/c V7JSWN0q2/HS+OHTUnGtxgg/zSXVMryf3CPeCtAko4kHUjBYhQZ2EdNAlBY1tY4Dlz4npSwN hckoGlLthig7UITguNwa0ulCzmZ+VfuM2ZuDsDYdUse7xketR2Mb4rEtbM1RHseptr4/WnvY iSNbgBMRwnlQ2SiAFbudvmr7NjEqK2DA/amauDJefOIoPBfUPGBwdSu1JFn9nCCLJfHOH4qF PA91kdZOBIxU83EhzUCTTAWnCPRfoaaohm74Ch+ssG49rziRgvu4YKFD7YaP89o/li6hqKKN ujYgygcS34QzpQX2XrB06QSxnYXgiBqMj6sSPEO7HCcCq3XnaBTAlgQbCYyfMpE4qQg3xVcb M7WjtSms9wwxvUxClpDSRnggpTzPZ1Mczz7bQ2YQh/VZefjR3WD2cz8bKKiRKcFiexVs0b1o jOHCwr4OSzFkTD1VhepOOUKjSeBPRUYtpvuF3QlQWXlUt/ibQW2ddFtijhji6U1i2nQOCgXN iVmb0JAs5Wf6CpZhrN0HGkLvR8HZaGU3j2U6eXVMMNcqfxwHiF9jP5X+lw/wrpRqSZFHbl7w XWD6NFppF6in6+EzT8tA38s4n5bwYmMu0tlI6DQ8JJNDG3F8Bw65mKVEx0WptFhB7UHVIhfz 9HOkOT4LzIQqro8HOMZDsnQbcWGaT8vaES4XjHTCwQBQHigMmSN3yS1ddmd83SUqt4xrZ2+w PIz
- Ironport-sdr: 64e485e1_eVyhev62nm9yd8hDi2maD9HDRIBYRliFzNIab2AVLYK9KOa bI7cbdfk0RyLnn3BAGDUZzJZ5cIwV4qkCmCSwtg==
I agree with Pierre, this is probably the best way to achieve what you
want. Mingling with pg regexp would probably allow this but would be
much more fragile.
Best.
P.
Le jeu. 6 juil. 2023 à 08:57, Pierre Roux <Pierre.Roux AT onera.fr> a écrit :
>
> 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.
- Re: [Coq-Club] make proof-general/company-coq stop on warnings, Pierre Courtieu, 08/22/2023
Archive powered by MHonArc 2.6.19+.