coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit--Claudel <clement.pit AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Easy way to enter Ltac debug mode in PG?
- Date: Mon, 25 Apr 2016 16:16:09 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
- Ironport-phdr: 9a23:sfNR0BdPtnkLpQ+tUMn5TZBKlGMj4u6mDksu8pMizoh2WeGdxc6+Yx7h7PlgxGXEQZ/co6odzbGG4+a/BydZvc/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uMPU4R2GP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDuR7JBgXD8CbCX4u09wD+v/dx1S3SacbyQLU5Xyjk96Z3YBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==
On 2016-04-25 14:15, scott constable wrote:
> First, why am I getting this message? In what sense is Ltac debug
> mode not "state preserving"?
I think this is Coq Proof General being too conservative. It pretty crudely
checks that you're not setting options with ‘C-c C-v’, since it could lead to
confusing results (it's fine to issue a ‘Show’ command, for example, but not
a ‘Set Default Timeout’, or a ‘Hint’, etc.). Set Ltac Debug is special in the
sense that backtracking to a point before it doesn't disable it, so it should
always be safe to issue (unlike most other options).
I'm not aware of a good way for Proof General to check whether an option is
state preserving or not, unfortunately.
> Second, is there an easier way to enter/exit Ltac debug mode than by
> directly entering the commands into the proof script?
You could disable that check by customizing ‘proof-strict-state-preserving’.
Cheers,
Clément.
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Easy way to enter Ltac debug mode in PG?, scott constable, 04/25/2016
- Re: [Coq-Club] Easy way to enter Ltac debug mode in PG?, Clément Pit--Claudel, 04/25/2016
Archive powered by MHonArc 2.6.18.