The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/27/2015 10:12 AM, Pierre-Marie Pédrot wrote:

On 27/02/2015 16:06, Jonathan Leivent wrote:

Or, perhaps you are suggesting that Ltac is better off without any
exception-like mechanism?

I think I'm suggesting Ltac is better off without any Ltac.

Isn't OCaml itself a product of the evolution of a proof scripting language? ;-)

But, that said, as a former developer whose customers were always creating devious hacks that were quite troubling from the knowing-how-things-work-internally point of view, I sympathize. 

More seriously, your hack is legitimate, but I just wanted to warn you
not to rely too much on the current semantics of tactics-in-terms. The
only use case where the semantics is fully specified is when:

1. The tactic is totally solving the current hole (so always writing
$(solve [tac])$ is a good idea).

It looks like that is already enforced.  For instance, something truly degenerate like:

let x:=constr:($(shelve)$ : sometype) in ...

fails apparently because tactic-in-term requires that all newly introduced evars - including its own goal and subgoals - must be solved.  In other words, tactic-in-term appears to prevent "evar leakage" - the often convenient but sometimes nasty habit of some tactics to shelve subgoals that one only finds out about later.

2. The tactic does not mess with the global evars of the current proof
state (do not try to do $(instantiate (i := foobar))$)

I mentioned in enhancement request 3872 that being able to enforce the above two rules in some form might be helpful.

3. The tactic do not rely on global side-effects (that currently
includes the abstract tactical).

I'm not a user of abstract.  But, maybe people who do use abstract for cases such as the archetypical "abstract omega", if they also were using tactic-in-term to help write definitions, would think it useful to be able to write $(abstract omega)$ for the very same reasons.  Although, there is no "Defined export...".

If you comply with these three conditions, you should be safe regarding
the potential evolutions of the implementation. Still, be careful.

PMP

It is hard to know what "careful" is here.  Perhaps catch has some unsafe details.  It is exploiting two undocumented features of tactic-in-term: tactic-in-term returns a normal proof term - not some internal reference or placeholder (as if it had done abstract on its own), and that proof term isn't automatically part of the proof term of the ongoing proof.  The first enables catch to search for "raised".  The second helps prevent the ongoing proof from becoming dependent on "raised".

Should exploiting these two features of tactic-in-term raise (pun unintended) any concerns?

-- Jonathan