coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
Chronological Thread
- From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
- To: Pierre Courtieu <pierre.courtieu AT gmail.com>
- Cc: Coq Club <coq-club AT inria.fr>, Andrej Bauer <andrej.bauer AT andrej.com>
- Subject: Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
- Date: Fri, 13 Apr 2018 10:36:17 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=SoftFail smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT chene.dit.umontreal.ca
- Ironport-phdr: 9a23:ls9PcR1V3TEXV5WbsmDT+DRfVm0co7zxezQtwd8ZseIUKvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUNhMWSJCDIOyYYkAAOQOMulEtIT9u0cCoAGiCQWwHu7j1jlFjWL2060g1OQhFBnL0hE8H90QvnTbttP1P7oVX+CyyqnIyzTDYO1M2Tzg74XIdxchofeKXbJxb8XR01IiGQDZgFuJs4DqMTSb1uMLs2iH9epvS/igi2o9pwxvvjWi38EhgZTKiIIN0l3I6Ct0zJgvKdGmVEJ2bsSoHIVfuiybLYd6XN8uT3l1tCs01LEKo4C3cDQFxZg92RLSaeaLf5aH7x79UuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtFsipFncfKtn8TzRDc98mHSudn8ke83DaP0AbT6v1eIU8qj6XbL4QtzaIqmZYLsETDGDH5mFnugaOLeEgo5PKk5/r7brjpvJOQKYB5hwDkPqgwhsCzGeE4PRIPX2if9+S8zrrj/UjhTbVPif02lK/ZsJHEKsQBvaO5AhVV0oE55xaiCjem19IYnWUdLF1bYh2Hi5LlNE3UL/zgF/ewn0yskCt3x/DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0dYmWG+VGKLRG6TPq0OJ6/9nd/GNaZUPtXD2LOU/+//jkFc2nFYcee+i2p5BO16iGfEzGFmUb3PqyvIGF2ELsxB2GOntjluDXCR7RkyVGZ8Z4TcnEo+vCcHob9b+0/S6wC6nE8gONSh9AVeWHCKtLt3cAqZeWGepOsZk1wc8e/2kQo4l2wupsVaqmbt9KazJ/yoeqYju3dwz7OSBzkhupwwxNNyU1iS2d08xhnkBHm9k/ZpY53FYzVGfy6Vxh7pzPI4Lvq4bYkIBLZfZitdCJZXyVwbGJIvbQ1arRNjgDTAtCM80xNkSeUt0H5Oph0Kb0g==
> So trying to remember the size and places of frames of response and
> goals buffers is the best way to go. This should not be too hard to
> implement indeed, using registers. We could also have a special
> command "restart coq on this new file without killing frames". For the
> latter it would help to know in which scenario you need to restart
> coq.
If Proof-General can know in which scenario we are, then it should be
able to refrain from killing the buffers: avoiding the delete+recreate
is always a better option than trying to delete+recreate in such a way
that nothing appears to have changed (there's always some detail of the
delete+recreate which ends up seeping through for some corner case).
Stefan
- [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Merlin Göttlinger, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Gaëtan Gilbert, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
Archive powered by MHonArc 2.6.18.