coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to file bugs against PG Coq mode?

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to file bugs against PG Coq mode?
Date: Thu, 15 Oct 2020 14:10:41 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT outgoing.mit.edu
Ironport-phdr: 9a23:lmwRyhz8zeN0OSnXCy+O+j09IxM/srCxBDY+r6Qd2+oSIJqq85mqBkHD//Il1AaPAdyErawfwLOK4+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhjexe7J/IRu5oQnMucQbgpZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/gqJUohKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAoofjuVQOrwa1CBesBOz1yD9HmGL51rA93uQ9DQ7G3BYvH9AQv3vJt9j1MaYSUfyvwKbW0DrDcupb1DHg44fHbh4vu+uDXa5sccXP00kvERvIgFuOpYHqIT+Y2foBvmyb4ud9VO+ij2Eppx9+rDah28ohiZXFiI0bx13Y9ih13Ic4KMG7RUJmYNOpFIdcuj+YOoZwX8gsTWZouCMgxb0Hv562ZCcKyJU7xx7fdvyIaJKE7Q7kVOaUJzpzmXFreKqnihqv8kWs0OnxWtOq3FtJtCZJj8TAumgT2xDP7sWLUPhw80e71TqS1g3f9vtILV02mKbGLZMq36Q+mYAJsUvZGy/7gEX2g7GSdkUj4uWo7PnnYqnppp+bNo90jA7+Pr4rmsy+HeQ0KBYBUHWG+eik1b3j+1P2QKlSg/ErkaTVqpTXKd4FqqO6GQNZz5sv5w66Dzi80dQYmXcHLEhCeBKCl4XpJ03BIPDiAve9nVujjSxmx/XHPr39GJnCMGXMkKr5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4zoMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FaLkfRSnrlgNoNWTMWtQo3TuHmoFiDTXhea2vkDPF03S0yFI/zVdSLfYuqmrHUhH7mTK0TXXhPDxW3KVmtd4iAXK5cOiWPPsBmkzoLE72gV8ks2Qz87FarmYoiFfLd/2gjjbym0dF04+PJkhRjpzl1E4KQ33zfFjgozFNNfCc/2eVEmWI40k2KgPp9guAeGNBOtatE

Thanks for reporting a bug! Best way to get it to the PG developers is to open an issue at https://github.com/ProofGeneral/PG.

On Oct 15, 2020 at 4:04:27 PM, jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I've hit a bug in Proof General's Coq mode. To whom do I report it?

The bug is that, when "Proof using" mode -> Always is set, and one has
started a proof with "Proof with tac", this will be corrupted to "Proof
using ith tac" (w gets deleted, and using improperly inserted before
with) instead of "Proof with tac using". And, because this alteration
happens in the locked region withou undoing the proof, it can go
unnoticed until one attempts to reparse the file.

[Coq-Club] how to file bugs against PG Coq mode?, jonikelee AT gmail.com, 10/15/2020
- Re: [Coq-Club] how to file bugs against PG Coq mode?, Tej Chajed, 10/15/2020
  - Re: [Coq-Club] how to file bugs against PG Coq mode?, jonikelee AT gmail.com, 10/15/2020