Make [abstract] nodes show up in the Ltac profile

[JasonGross]

This closes #5082 and closes #5778, but makes #6404 apply to abstract as well as transparent_abstract. This is unfortunate, but I think it is worth it to get abstract in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to ltac_call_kind for TacAbstract, but I think it's better to just deal with #6404 all at once.

The "better" solution here would have been to move abstract out of the Ltac syntax tree and define it via TACTIC EXTEND like transparent_abstract. However, the STM relies on its ability to recognize abstract and solve [ abstract ... ] syntactically so that it can handle par: abstract.

Note that had to add locations to TacAbstract nodes, as I could not figure out how to call push_trace otherwise. I was mostly cargo-culting surrounding code for this (actually, for most of this PR), so I've requested @ejgallego's comments on Loc.tag et al, since I seem to recall him doing things with Loc.ghost recently.

[ejgallego]

Loc.ghost is gone. If you have a location at hand you do Loc.tag ~loc obj otherwise Loc.tag obj will add the empty one.

[JasonGross]

@ejgallego I've cargo-culted doing Loc.tag ~loc:!@loc and then later pattern matching on it as a pair.

[ejgallego]

It is a bit of a pain, I think 8.8 should provide record-based patterns which are easier to use IMHO.

[ejgallego]

So I approve this, but why not to go the full route and add instead a location to tacs as it is done in the rest of the codebase:

and 'a gen_tactic_expr_r = ...

and 'a gen_tactic_expr = 'a gen_tactic_expr CAst.t
....

then you can just handle locations (and other stuff would you need it) as:

match tac with
| { loc; v = TacAbstract ... } -> ...

In fact this is in my TODO, but pretty low I'm afraid.

[ejgallego]

I approve this, however if @JasonGross things that handling all tactics in a uniform way could be worth the extra effort let's delay this. I'm ready to help with the porting.

[JasonGross]

@ejgallego I'd rather get this in and not spend the extra effort, at the moment. I was aiming for the least invasive change possible, here, and I'd rather not try to rework the type of tactics without really understanding what's going on. However, handling tactics in a uniform way might help with #6411.

[ppedrot]

@ejgallego I don't think having locations in tactic expressions in a good idea. Or, more precisely, if we did so then we would need to split Ltac into a user-side version and an evaluation-oriented version. While writing Ltac2 I realized that many Ltac structures were already using locations, but they don't make sense at runtime because they're not stable by substitution. The final result is that you clutter your term with invalid information.

[ejgallego]

Well I am aware of the problems with stale location info which are not exclusive to tactics in any way; indeed it looks to me that locations have been historically added to the codebase in an organic way and we may need some more engineering to improve the situation.

However, I don't quite follow why your comment does not apply to the current situation too: a few tac constructors already have location info and it seems it is critical for some purpose. So maybe we may want to handle it in an uniform way, as opposed to the current ad-hoc route.

Regarding stale info, well, that is a problem of what you put in reduction, right? Recall that tags are optional so at "internalization" time you can erase them, also you could erase them in reduction, I dunno.

In fact, this is what happens with the main Constr.t datatype, all info is lost on their way back from detyping.

[ppedrot]

In fact, this is what happens with the main Constr.t datatype, all info is lost on their way back from detyping.

Right, but what I meant is that for tactic evaluation we would need some equivalent of Constr.t for Ltac, and there is no such thing. We reuse the same AST with invalid locations.

[ejgallego]

We reuse the same AST with invalid locations.

You mean the invalid locations are in the objects stored in "interpreted tactics"? [Not so many] Or in the ad-hoc locations stored on the gen_tactic AST?

If this is the last case, in fact, implementing uniform handling would indeed help erasing the stale info!

[ppedrot]

I'd prefer not to add the location to the abstract node. It would actually simplify this patch a lot, the core of it lies in Tacinterp. Just pass it a ghost location there.

[JasonGross]

I thought Loc.ghost disappeared... Do I pass in None?

[ppedrot]

Yep, I meant None.

[JasonGross]

@ppedrot Done

[ppedrot]

LGTM.

[herbelin]

@ppedrot: I'm not sure I understood the discussion. Locations in an Ltac tree may refer to the source code of the tactic, is that what you mean when you say "don't make sense at runtime because they're not stable by substitution"? If yes, these locations are valid and what we need is to print them with indication of the original file. Or do you mean that they are None but if so, the situation is not different from the detyping case. Do I misunderstand the discussion?

[ppedrot]

I'm not sure I understood the discussion. Locations in an Ltac tree may refer to the source code of the tactic, is that what you mean when you say "don't make sense at runtime because they're not stable by substitution"?

Indeed, they refer to the source code of the tactic.

If yes, these locations are valid and what we need is to print them with indication of the original file.

The fact that the locations points to some real part of the code does not entail that this is relevant in the context of the tactic evaluation. I often stumble upon tactic code that gives completely buggy location information. I'm not sure exactly where this comes from, but I suspect it is due to the dynamic model of Ltac where one needs to rely on dynamic heuristics to determine e.g. that some absolute piece of data actually stands for a bound variable. The same kind of problem arises when constructing data structures like intro patterns from data taken from the bound environment. Put otherwise, locations as backtraces only make sense when there is a somewhat standard evaluation model. This is what I meant about substitution.

[herbelin]

Well, in some cases, I was able to report the location of an error in the source code of the tactic and that was useful I think. But I agree that this is a difficult problem when you combine pieces of data coming from various origins.

And working within a clear(er) semantic evaluation model, that's a key point indeed.

[JasonGross]

This builds on my travis: https://travis-ci.org/JasonGross/coq/builds/316673281

The remaining discussion seems beyond the scope of this PR (how tactics should or shouldn't have locations in general); @herbelin does this seem accurate to you?