ceps
ceps copied to clipboard
coq
Contributing to the discussion on versioning tactics
I find it a good idea to have a generic mechanism for parametrizable tactics. A typical use case would be eauto where we have identified a lot of possible parameters whose "right" default is not so clear. I started with a compat setting but was now in the process of just having a record of parameters.
When on the contrary, we want to completely rework the implementation, then duplication of code instead is the way to go (although the new implementation can still have a record of parameters / compat settings).
I am not quite convinced by some of these proposals, but it might be because I don't fully understand them. I am fine with commands such as Set Version 8.6 and Set Structural Injection, but I don't agree with them having a dynamic scope. The scope should be lexical/static. In other words, flags/version should be completely resolved at the time the tactic is internalized; they should not wait for execution (contrarily to what the None argument seems to imply). Similarly, I would be fine with the tacticals only if their scope is lexical.
Here is an example to make my point clearer:
Set Version 8.8. (* runtime version made explicit for the sake of the example *)
Section S.
Set Version 8.6.
Ltac bar foo := tac 1 ; foo 2. (* tac is internalized as 8.6 *)
End S.
Ltac baz := bar tac. (* tac is internalized as 8.8 *)
Set Version 8.7.
Goal True.
baz.
When the user calls baz, first the 8.6 version of tac is executed with argument 1, then the 8.8 version of tac is executed with argument 2. Resolution of the version/flags should be purely lexical.
@silene Same thing here, this should be static scoping, otherwise tactic writers will run into a hell if they try to mix higher-order tactics from different versions.
I was trying to accomodate @JasonGross' need in a discussion starting here in #276. In the proposal, the default policy is static binding. The version dynamic in tactical changes it to an explicit runtime binding as an extra convenience. Then, it is the responsibility of the user not to abuse runtime binding and to flirt with debugging hell.
Note that moving to static is also a change of semantics, so, strictly speaking, preserving former semantics needs to let the possibility of runtime binding (for instance shall we want that -compat 8.7 uses static bindings even though it is currently dynamic bindings?).
So "with_version 8.6 tac" would still work by internalizing tac in the right version? Also, the dispatch on versions still has to be done in the TACTIC EXTEND entries right? Would we need special support for this, e.g making all extend entries expect a "version" variable that is statically scoped?
Hmm ok, IIUC, @silene and @ppedrot would rather have dynamic binding be replaced by explicit option passing using optional/labeled arguments?
My wish is that OCaml tactics should not be special, or at least should be as unspecial as possible. If an OCaml tactic can resolve it's flags at internalization time, I should also be able to write Ltac which has flags which are resolved at the internalization time of my user-space tactic. Moreover, I should be able to nest this sort of construction, and say, e.g., that for a tactic myrewrite which invokes rewrite, the flags of rewrite are resolved when the call to myrewrite is internalized.
So it's not not really "at runtime" that I want, but "delay resolution".
So "with_version 8.6 tac" would still work by internalizing tac in the right version?
Yes.
Also, the dispatch on versions still has to be done in the TACTIC EXTEND entries right?
Yes (or in tacinterp.ml for the tactics of g_tactics.ml4). How to do it is however unclear. Either by forcing tactics to take an extra version argument, but this would need changing all calls everywhere, even when not needed. Or on a by-need basis as in the current cep.
Would we need special support for this, e.g making all extend entries expect a "version" variable that is statically scoped?
Yes, we need a way to communicate the value of version to the tactic in TACTIC EXTEND. Either using a conventional "version" variable provided by the macro (the same way as we provide a variable named loc) or by using a reference (as in the current version of the cep). The first one is more elegant (generated code is purely static) but maybe more difficult to learn for whom is not used with OCaml macros magically binding variables in the macro itself.
@herbelin It's not very hard to pass an extra-argument to TACTIC EXTEND with a canonical name, which allows to keep the code working without modifying it. This is already what we do for ist which is bound to the environment.
@herbelin to the call site of the tactic being defined. Alternatively, I'd like something like
LtacWithOptions(options) myrewrite lem :=
with_options options rewrite lem.
And then if myrewrite is ever invoked without being surrounded by with_options, then the value of the options should be fixed at that call site.
would rather have dynamic binding be replaced by explicit option passing using optional/labeled arguments?
On the OCaml side, yes, since I don't know any better way to do that. On the Ltac side, however, since we have to come up with a syntax anyway, there are several possibilities. As long as the semantics offers lexical scoping, I am fine with either tacticals or tactic options or whatever syntax.
@JasonGross: Then, this seems to be exactly the point of this version runtime in (syntax not fixed):
Ltac myrewrite lem := version runtime in rewrite lem.
Goal ... .
version 8.7 in myrewrite lem (* use options defined for 8.7 in rewrite *)
myrewrite lem (* use default options in rewrite *)
Syntax can then later on possibly be made more precise to pass specific options.
Are these two the same?
Ltac myrewrite lem := version runtime in rewrite lem.
Ltac myrewrite87 lem := version 8.7 in myrewrite lem.
And
Ltac myrewrite87 lem := version 8.7 in rewrite lem.
?
I'm failing to see why we need an extra layer of complexity to implement static binding of versioned tactics. Why not simply piggy back on the module system?
We can indeed define a Coq module Ltac86 that contains the right Declare ML Module, such that this ML module actually replaces the parsing rules of built-in tactics by the corresponding versioned tactic. This would already work as of today, with a simple, predictible model and no implementation tarpit hassle.
Obviously, if we want dynamic dispatch it is another story, but I still have to be convinced that we actually ardently desire the latter.
Correction to my above post: we wouldn't shadow parsing rules, but tactic notations. Apart from the last handful of hardwired tactics, every ML tactic now relies on tactic notations to parse, so that it's enough to shadow the notation content (a notation is a mere kernel name).
@ppedrot: Do you mean things like Ltac86.rewrite or Ltac87.rewrite? If not, can you give an example?
Hi, coming back on this proposal, what I proposed (i.e. TACTIC EXTEND injection [ "injection" ] -> [ myinj !dynamic None false None ] END is not enough for static binding of the configuration flags, as myinj would be called only at runtime. And we want static binding, which is easier to track, to control, to debug, right?
For static binding of the configuration flags, one would typically need to keep a copy of the frozen state of options in the TacML constructors, and build at runtime the configuration flags of the tactic from this statically-frozen state.
Any objections if I start to explore this direction?
(An alternative would be otherwise to provide a make_config : Flags.compat_version option -> 'a method at each TACTIC EXTEND node, in the style of TACTIC EXTEND injection [ "injection" ] -> [ fun flags -> inj flags None false None ] CONFIGURATED WITH make_config END. That would be a more specific information, but that would be a disruptive change in the TACTIC EXTEND API and more complicated to support a stepwise transition.)
@herbelin So, you can't write Ltac86.rewrite because most of ML-side tactics are defined by tactic notations, so this wouldn't even parse.
Nonetheless, nowadays most of built-in tactics are defined through TACTIC EXTEND, and this mechanism is scoped w.r.t. to the import. That is to say, assume you write in Ltac86.v
Declare ML Module "ltac86"
where the ltac86 plugin defines the very same TACTIC EXTEND as standard Ltac, except that their body is replaced by a call to the legacy implementation. Now, when you do Import Ltac86, everything you parse is going to call statically the legacy implementation instead of the current one. That is,
Goal foo.
Proof.
rewrite bar. (** Current implementation *)
Import Ltac86.
rewrite bar. (** Legacy implementation *)
Abort
Import Ltac86.
Ltac foo := rewrite bar. (** Will always call the legacy implementation *)
Obviously this does not solve the problem of mixing the two worlds in the same tactic, although it can probably be emulated in most of the cases. For such mixing to occur (if we really want that) we could mayber divert the implementation of Import.
Also, your first proposal above seems very wrong. First, you shouldn't ever store the summary in the TacML node, this is going to be huge in size and totally ad-hoc. If you want to go that way, you should rather extract the version flag at internalization time and store only this in the tactic node.
I don't understand you second proposal, but if what bothers you is retro-compatibility of the macro, you can always pass the flag variable statically in it, and let the macro handle it if it wishes so, as I mentioned in a previous post (just like ist).
if what bothers you is retro-compatibility of the macro, you can always pass the flag variable statically in it, and let the macro handle it if it wishes so, as I mentioned in a previous post (just like ist).
What bothers me is to get some kind of ideal world, where Coq with option -compat 8.X, or Coq with Set Compat Version 8.6, works, tactics-wise, unification-wise, etc. exactly as if it was working in Coq version 8.X, while in current Coq we can freely improve the implementation of any tactic or unification heuristics without being bothered with compatibility issues. This ideal world is what looks to me the best model for simultaneously satisfying the need of users who do not always have the time to upgrade existing developments and the joint wish of users and developers for the most up-to-date tactics or unification. This does not mean that users have to stay with older versions, but it means that they can upgrade at their own pace, own calendar, if and when time permits.
At least from the technical point of view, providing such an ideal world is possible. The drawback is a potential additional complexity in the code to manage the diversity of behaviors, however mitigated by the fact that this complexity is actually already here, since we started to have a system of dynamically-bound options to control the behavior of features. My hope is, that by a uniformly-designed configurability engine, we stop tinkering with the compatibility problem. Such truly configurable system, like I remember Linux had at some time, and probably still has, would be multi-purpose. In addition to preserve compatibility with older versions, it would also allow programmability of behaviors: which unification to use, which amount of reduction, which support for evars, which kind of users, typically beginner or expert, is targetted in the behavior of a tactic, etc.
Of course, it depends on components. I'm not talking about components which are painful to maintain (e.g. Metas or w_unify), and for which it is reasonable to drop the support. I'm not saying that we have to maintain at any price a compatibility with "broken" features. But in most cases, configurability is just about a line if myoption then bla else bli somewhere and this is just basic. Our time is precious and having to understand and amend code that is complex to understand knowing that this code is there only for compatibility is indeed a "waste of time".
I'm not talking either about which deprecation policies we shall adopt or not. I'm only talking about the technical side and about what a configurability engine would give us in terms of both freedom to make progresses, and support for the users to follow us in the evolutions. The fact is that for years and years and years, the compatibility issue blocked us, and we do have to find a solution to let us produce new primitive tactics, new tactic languages, new features that we want for new developments, without being stopped by stupid things such as a different name or a different evar-evar instantiation, or a section variable incompatibility in existing developments.
I do want to see new ideas emerge, like Ltac2, and like other ongoing projects, and it is for this reason that I'm trying to set a framework in which these new directions can be developed without always being constrained by the past, and by travis stopping us with a red cross.
Currently, the behavior of a tactics is dynamically controlled by individual flags, mostly Boolean ones, and by the version number. I think that @silene is right when he complains that this dynamic aspect of configurability breaks e.g. continuation-passing-style. I don't think that @JasonGross is wrong in saying that dynamic configuration has some benefits. What I have currently in mind is just an infrastructure so that the existing behaviors can be managed consistently, and providing a new support for a statically-scoped version of the configurability. This means, that e.g., when in 8.6 compabitility mode, interpreting Set Keyed Unification should be interpreted the same way as in 8.6, i.e. dynamically, and that an Import Ltac86 should be aware of this, while an Import Ltac88 shall treat Set Keyed Unification statically. So, an Import methodology will not be able alone to deal with configurability.
Maybe I will be told that this is overkill, that users can deal with the incompatibilities on their own and that we don't need this complexity. But, I'm not sure that this complexity is so bad at the end. Might this complexity be on the contrary what will allow us to evolve more easily because we will precisely stop to care too much about the cost of adaptation for users.
Otherwise, about freezing the whole summary, we need to know where we are going. If the plan is to go towards a fully functional system (in the sense of functional programming), and I think that this should indeed be the plan for many reasons, starting with parallelism and debugging, we shall have to pass the frozen summary around anyway everywhere, shan't we? So, the question does not seem to me too much about the cost of freezing (it should eventually morally be just copying a pointer to a purely functional universal summary).
So, an Import methodology will not be able alone to deal with configurability.
Configurability is a distinct, subtly related matter. I don't think we would gain clarity by confusing them, but unluckily that's what we've being doing with the global compatibility flags introduced across the versions.
Might this complexity be on the contrary what will allow us to evolve more easily because we will precisely stop to care too much about the cost of adaptation for users.
I'm not totally convinced by this statement. It will undoubtedly remove adaptation cost from the point of view of the user, but it'll most probably shift it into the hands of the poor developers that will have to handle it. I'm particularly afraid by the fact that the ratio Coq developers / Coq users is definitely not in our favour, and that we won't have the material time to satisfy everyone. And this is getting worse.
the question does not seem to me too much about the cost of freezing (it should eventually morally be just copying a pointer to a purely functional universal summary).
I don't think it has anything to do with the functional / imperative debate. It's just that it's going to be stored in the vo, leading to huge memory consumption, for nothing, because you just want the compatibility version of Coq at internalization time. So I stand my ground, what we should do is passing the compatibility version to the Ltac internalization function (e.g. in the glob_sign.extra field) and store it in the glob AST. That's like a 10-line patch.
Although I am not knowledgeable enough to comment on the details of the proposal, I want to say @herbelin that I fully support your efforts. I think that we both lack a clear compatibility policy to share with our users and precise guidelines for developers on how to develop breaking changes. The framework you propose might concur to achieve such objective; other solutions might work too but we should really settle on one and document it.
I'm not totally convinced by this statement. It will undoubtedly remove adaptation cost from the point of view of the user, but it'll most probably shift it into the hands of the poor developers that will have to handle it. I'm particularly afraid by the fact that the ratio Coq developers / Coq users is definitely not in our favour, and that we won't have the material time to satisfy everyone. And this is getting worse.
So, what would be your ideal direction?
I can provide a POC patch if you want to see what I mean.
Yes, gladly!