The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Yes if you want to stick on 8.4-beta2. The other solution is to go for 8.4 svn branch.

Best regards,
PC

Le vendredi 25 mai 2012, Gregory Malecha <gmalecha AT eecs.harvard.edu> a écrit :
> Hi, Pierre --
> Yes, my Proof General is set to time commands (it is useful when doing automation stuff). So is the work-around for now to disable this Proof General feature?
> Thanks for your help.
>
> On Fri, May 25, 2012 at 9:47 AM, Pierre Letouzey <pierre.letouzey AT inria.fr> wrote:
>>
>> > > Time Backtrack 94 0 0 .
>> > > ^^^^^^^^^^^^^^^^^^^^^^^
>> > Error: Navigation commands forbidden in nested commands
>>
>> Hi
>>
>> I first thought that you tried this command explicitely yourself,
>> but then from your second mail I understand that it's your
>> ProofGeneral that did it for you. Is that correct ?
>> In my version of ProofGeneral, it might be so if the emacs variable
>> coq-time-commands is non-nil, maybe something wrong in your config
>> file ? I let you check the emacs side with the other Pierre (Courtieu).
>>
>> Now, concerning the Coq side, it's true that doing a "Time" on
>> a "navigation command" (i.e. Reset, Back, BackTo, Backtrack) is
>> a rather strange idea (since these commands are normally
>> instantaneous), but it is quite harmless, no reason to forbid it,
>> I've re-allowed that in the 8.4 svn branch (commmit 15365).
>>
>> Apart from this particular case, please note that navigation commands
>> are not regular commands anymore, but special ones that can only be
>> used now in certain circumstances :
>>  - not inside files given to coqc
>>  - not inside files loaded via "Load" (or via coqtop -l)
>>  - and indeed, not inside other nested commands such as Fail ...
>>
>> The reason for these restrictions is that we now maintain an
>> explicit internal stack of (regular) executed commands and
>> associated states of the system (including the state of the
>> proof engine). For a Load, the stack will be grown by *one*
>> step (the Load itself), not recording all the inner steps.
>> For a coqc compilation, for efficiency we don't use this
>> backtracking stack at all. And for nested command such as Fail,
>> it's quite hard to give a sensible semantic to something like
>> Fail Backtrack.
>>
>> In conterpart to these new restrictions, the benefit is that we
>> can properly say "go back N steps in the past" (Back N)
>> or "go back to state number N" (BackTo N) and Coq takes care
>> of everything, including proof states.
>> We don't need anymore the quite complex "Backtrack" command
>> (it is kept currently only for compatibility with Proof-General).
>>
>> Best regards,
>> Pierre Letouzey
>
>
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>