coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Tej Chajed <tchajed AT mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to file bugs against PG Coq mode?
Date: Thu, 15 Oct 2020 17:40:16 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f50.google.com
Ironport-phdr: 9a23:pEWP/x0ZkWn8HSrasmDT+DRfVm0co7zxezQtwd8ZseMeL/ad9pjvdHbS+e9qxAeQG9mCtLQa0KGP7/CocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalzIRi4ogndq8YbjIh/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMVdtTWSNcGIOxd4UBAeofM+hFrIfypVUOoxyxCgawC+3i0SNIi33s0KEmyektDR/K0Qo9FNwOqnTUq9D1Ob8cXeC3y6nIyzTDb/BI1jf59ofHbAssof6JXb1qcMrRzVMjGB/CjlWVp4DuIjSY1uYKs2id7upgVvygi2o5pA5vuTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV0bsKqHoFKuCGGK4t5XNkiQ2dwtSs41rAIuYO2cScExpg6yBDRZfKKfpWH7x//W+icJSp0iX17db6ihhu/70euxO3yW8e70ltEoSpLnNbMuH0RyhDe7NWMRPV6/kekwzmP1gbT5/lLIUA1iarbK4MhzaUqmpUPtkTDGyn7k1j1gq+Obkgo5PSk5uD9brjlppKQLZJ4hwD/P6g0msGzHfw0PhYPUmSH5Oix0aDv8EnlT7hPgfA7k7XVvIzfKMkVuKG0AwpY3pg/5xqjETur1cgXkmcJLFJLfR+HgZbmNEzUL/39E/uyjVahnyxtyvvbJLPuGI/NIWLGkLr5fbZy9UpcyA0rwNBa/Z1UC7UBLOvyWk/2qdDUFxE5Pgyoz+r9B9V90YQeWW2LAqCHKq/drViI5uc3L+mNYo8apir9JuA76/LyiXI1g1wQcKmz0ZcKaX21H+5qLkWFbXb0h9cOC2YKvg4wTOzwj12CVCZeZ3S1X6I65zE7C5ypDYPdSY+zm7GB0yK7EYdXZmBCEFyDDXDod4CcV/cWdC2SOtNhkiADVbW5V4Ah0giuuBbmxLpjM+rb4TYVtYnj1dhw/+3cjws+9T1yD8SH0mGCVXt4nm0SR2x+4KcqnUF/gnyD2Kp1j7QMCddT7vFEXi8/NIKawuBnXYPcQAXEK52LT1CnQdiiDDwZQdc4wttIaEF4UZ32jBfF3imnB7IYv7OODZ0wtKnb2i6idI5G13/a2fx53BEdScxVODjj3/YnrlWBN8vyi0yc0p2SW+Ec0SrKrjrRyGOPuARZV1c1X/idG38YYUTSoJLy4UaQF+b/W4RiCRNIzIu5EoUPb9ToiVtcQ/K6YYbRZmuwnyG7AhPan+rQPrqvQH0U2WDmMGZBixoapC/UOg03ByPnqGXbXmRj

On Thu, 15 Oct 2020 14:10:41 -0700
Tej Chajed <tchajed AT mit.edu> wrote:

> 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.

Thanks - done: https://github.com/ProofGeneral/PG/issues/518

>
> 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