Fix rewrite in * side conditions

[herbelin]

Hi, this fixes the problem (indirectly) reported by @sigurdschneider in the Containers contribution: rewrite was wrongly be called recursively also on side conditions when called with the * |- and * clauses.

In theory, this is a change of semantics, but in practice, Travis does not report any incompatibility. There shall be an incompatibility on containers though. What shall we do, considering also the ceps discussion on configurability?

• Regarding this specific bug, it is so rarely used that adapting scripts shall be easily manageable, so just push it and document it in CHANGES?
• But in general, such a fix can have an unexpected impact in many places, so what do to? Shall we methodologically encapsulate the two lines which changed into a if Flags.version_strictly_greater Flags.V8_7 then new-code else former-code, so that, at least when called with -compat 8.7, the old behavior is ensured to be the same?
• But what if 8.7 Ltac code is eventually mixed with 8.8 code; shouldn't we make the code of rewrite depend on a set of configuration flags so that Ltac code referring to rewrite can determine at definition-time whether the 8.7 semantics or 8.8 semantics is expected, even if code in 8.7 semantics is mixed with code in 8.8 semantics? I started a branch in this direction, creating a file tactic_config.ml to centralize configurabibility of tactics, knowing e.g. that autorewrite depends on rewrite which depends on unification, etc., so that in theory, autorewrite or even ssr's rewrite itself depends on which unification module is used and about how it is configured. Don't know what to do yet with this, but it seems to me to be a first direction to collect exactly what a given feature depends on, in a way which is not too invasive (basically only adding an explicit argument flags to tactics) and which can tell in one grasp at tactic_config.ml what depends on what. This is a direction similar to the one taken in Trunk+abstracting injection flags #677, going towards being able to statically control configuration flags (though, currently, selection of flags remains done at runtime). It should be so that it does not add extra burden on developers though and that every developer can work in good conditions.
• Combine this with a model with versioned ltac_plugin?
• Other?

[maximedenes]

@herbelin Is there any special plan around this PR? Should it be merged as is?

maybe @charguer has an opinion?

[herbelin]

@maximedenes:

Is there any special plan around this PR? Should it be merged as is?

I was hoping to trigger a discussion on how to deal with tactic compatibility in general but no discussion happens.

Considering that the fix has no impact on Travis and a small one on coq-contribs, I guess that we can commit it independently of a general discussion about tactic compatibility.

[Zimmi48]

I also tried to relaunch this discussion at the WG of October without success.
I agree that Travis showing no incompatibility should be a reasonable criterion to merge this PR.
Wrt making significant progress on tactics (with compatibility breaking), I now only see the option of developing a new plugin.

[maximedenes]

@herbelin Could we document the new behavior (if it is not already)? And add a CHANGES entry?

[herbelin]

@maximedenes: it is more a bug fix than a new behavior, in that it is the natural expectation, and what rewrite was already doing with other forms of the in clause. I'm otherwise a bit reluctant at documenting now the behaviors of tactics with respect to side conditions. I would say that it'll be better to document them when the behaviors will be stabilized and made uniform across the different forms of incantation, what do you think?

[Zimmi48]

It might not be worth documenting now if not stabilized but the note in CHANGES is a good idea in any case so that our users can find the reason for the change in behavior if they happen to stumble upon it. See also #6396.

[herbelin]

But then, shouldn't we do that virtually for all bug fixes, which we could certainly try to do with a bit of discipline (and which @maximedenes did for some former version), but which we did not do yet for 8.8 and which we would have to do retroactively? (I'm however ok to do for my own fixes if decided.)

The alternative is to have this kind of link as for 8.7.1 but it shall not a priori be as long-lasting and trackable as in a file.

[Zimmi48]

Come on Hugo, it is you who started your PR by saying that there was a risk of incompatibility and proposed as a first possible solution:

Regarding this specific bug, it is so rarely used that adapting scripts shall be easily manageable, so just push it and document it in CHANGES?

I precisely don't want to put all bug fixes in CHANGES because it would mean that compatibility breaking bug fixes (especially when they are a direct change to tactics) are not highlighted in any way.

[herbelin]

@Zimmi48: Are you saying that I'm writing inconsistent comments? Well, apparently.

So, I don't know any more what to do. Do you suggest I follow comment 1 or comment 2?

[maximedenes]

it is more a bug fix than a new behavior, in that it is the natural expectation

I disagree. "Natural expectation" is way too subjective to consider this a pure bug fix. And even so, what does it cost to add a CHANGES entry?

Listing bug fixes systematically in CHANGES is a separate topic.

I would say that it'll be better to document them when the behaviors will be stabilized and made uniform across the different forms of incantation, what do you think?

I would prefer that we document at least this particular behavior now. The fact that some other behaviors are not uniform or maybe counter-intuitive is an argument for more documentation IMHO, not less.

[herbelin]

it is more a bug fix than a new behavior, in that it is the natural expectation

I disagree. "Natural expectation" is way too subjective to consider this a pure bug fix.

I'm unsure to understand what you are disagreeing with. Do you personally think that not rewriting in the side conditions is not the intended behavior? If yes, could you give examples highlighting what is your "natural" expectation?

And even so, what does it cost to add a CHANGES entry?

As @Zimmi48 noticed, this was apparently my initial proposal. As far as I understand the question, it costs nothing to add an entry in CHANGES. It is just about evaluating whether it is worth and relevant to do it in this particular case knowing that we don't do it systematically.

I would prefer that we document at least this particular behavior now. The fact that some other behaviors are not uniform or maybe counter-intuitive is an argument for more documentation IMHO, not less.

If I say "The fact that some other behaviors are not uniform or maybe counter-intuitive is an argument for more documentation concomitantly with the introduction of uniformity", would it be a sentence on which we could both agree?

[charguer]

I think that it is useful to have a two line note in the change log, saying that a bug was fixed for rewrite and say under which conditions an incompatibility might be expected.

Regarding treatment of backward compatibility, the only long term general solution that I can think of is to be able to declare lemmas, proof script and tactics within "version scopes". I will try to think of a concrete proposal for ltac 2.0.

[ejgallego]

@charguer I think that Coq is very close to support "versioned scripts", IMHO we are just lacking the manpower to finish the remaining bits.

A particular source of problems is all the hooks that happen to be statically initialized and bring in version-dependent behavior. I'd dare to say that once that code is refactored out, a version specification pragma should be doable without too much pain.

[maximedenes]

I'm a bit lost. I agree this change is "right", but I disagree with not wanting to document the behavior and the change. I was simply asking if we coud

1. document this behavior, that is, if the manual doesn't say what rewrite in * does to side conditions, it should
2. add a CHANGES entry

Is there a problem with that?

[herbelin]

@maximedenes, @charguer: I added 3 lines in the CHANGES. Is it ok for you as I did? About the reference manual, I wondered how to tell what happens to side conditions, but the explanation for rewrite ... in * does not suggest that something recursive applies under the hood. It presents things as if the rewrite was done on all hypotheses at the same time. So, I think it is clear from the text that side conditions are not supposed to be affected by any kind of further rewriting.

@charguer: What concrete user-level API do you typically have in mind for "version scopes"?