The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Hi

Short story : if some of you are using the Suspend / Resume
commands of coqtop for proof managment, I'd glad to ear from you...


I'm currently working on improving the backtracking mechanisms
proposed by coqtop (and hence Coqide, ProofGeneral, ...).

As a side-effect of this work, a basic Show Script is about
to be restored : the tactics performed during a proof could easily
be retreived from the command history stack I'm introducing.

Other goodies of this work includes the full support by Coqide
of commands such as Restart, Abort and Undo, for instance for
pedagogical scripts or tests.

But conversely, this framework is currently incompatible with
the Suspend / Resume commands, and I'm planning to just delete
them if nobody objects : I'm currently unaware of any usage of these
commands, and they are already unsupported by both Coqide and
ProofGeneral. In ProofGeneral, you could probably put some Suspend
and Resume in your scripts, but the backtracking will not work
correctly then. It's actually quite non-trivial to correctly
handle backtracking for commands that might interleave pieces of
different proofs in a non-well-nested way, and I currently think
it doesn't worth the effort...

For the curious, the code I'm proposing is in a github repository
           https://github.com/letouzey/coq-wip
in the branch named "backtracking". Many details in the last commit
message. This code will probably land in trunk in a few days, and
hopefully in 8.4 before the stable release.

Best regards,
Pierre Letouzey