Cyril Cohen (Jun 08 2020 at 20:14): Cyril Cohen (Jun 08 2020 at 20:14):Hi all, can someone remind me the rationale behind this, I am currently trying to do the appropriate fix in mathcomp, but I have the feeling it makes the work environement and its setup more heavy than usual. The more I proceed to porting the less I am happy with this new restriction...
Ali Caglayan (Jun 08 2020 at 20:15):Is this because you need to specify a hint database?
Cyril Cohen (Jun 08 2020 at 20:18):@Ali Caglayan no, this is because Hint with arbitrary terms (e.g. (@le_trans _ my_type)) are deprecated, and the warning recommands to set a global constant before doing the hint, which could be either a Definition and pollute the global environement or a Let ant pollute the section environement...
Cyril Cohen (Jun 08 2020 at 20:19):And in addition to polluting either environement, we could do Hint Resolve t1 t2 .. tn with several open terms before, and now, we need to put one definition per term, which expands the size of code by as many hints per line we could fit...
Ali Caglayan (Jun 08 2020 at 20:31):Would Local Definition be a good substitute? The local namespace would be polluted, but not when the module is exported.
Cyril Cohen (Jun 08 2020 at 20:38):Ali Caglayan said:
Would
Local Definitionbe a good substitute? The local namespace would be polluted, but not when the module is exported.
Given that Search would not ignore the module, it would pollute the Search results
Jason Gross (Jun 08 2020 at 22:02):There's a line Add Search Blacklist "_subproof" "_subterm" "Private_". in theories/Init/Prelude.v, so you could get Search to ignore your constants by prefixing them with Private_. Or by explicitly adding them to the Search Blacklist.
Jason Gross (Jun 08 2020 at 22:03):I believe the reason that it's deprecated, though, is that it complicates the internal representation significantly? cc @Matthieu Sozeau @Pierre-Marie Pédrot , I think
Matthieu Sozeau (Jun 08 2020 at 23:09):Yes, it basically duplicates the definition code in hints, does not play well with universes or evars, and prevent implementing discharging correctly.
Matthieu Sozeau (Jun 08 2020 at 23:12):You could define a specific "Hint_" prefix and ignore that during search too.
Matthieu Sozeau (Jun 08 2020 at 23:15):Maybe you could give us a few examples where it's a real pain @Cyril Cohen ? We could also have glue code that would make the definitions for you I suppose, but ideally we'd have Hint just take global_references as argument so they can be turned into terms in any environment directly..
Cyril Cohen (Jun 08 2020 at 23:24):Matthieu Sozeau said:
Maybe you could give us a few examples where it's a real pain Cyril Cohen ? We could also have glue code that would make the definitions for you I suppose, but ideally we'd have Hint just take global_references as argument so they can be turned into terms in any environment directly..
There are not many very problematic example in final code (you may have to scroll down)
I would be glad if the definition could be done on the fly.
Moreover, I do use prefix/suffix filtering (although I remember having trouble extending it a few years ago), but I do not think it allows for readable code. (Is there an Issue / PR about having an attribute instead?)
Maxime Dénès (Jun 09 2020 at 09:53):Search blacklisting should be done by an attribute, not hacking a prefix IMHO
Matthieu Sozeau (Jun 09 2020 at 10:10):That would be nicer indeed
Théo Zimmermann (Jun 09 2020 at 10:11):I would be glad if the definition could be done on the fly.
See also coq/coq#11970 "Why is the declaration of arbitrary terms as hints deprecated?"
We should probably not remove the feature until on the fly declaration of global constants is supported.
Matthieu Sozeau (Jun 09 2020 at 10:15):Remove which feature?
I mean, it seems what we are leaning towards is to support arbitrary terms as Hints but doing it by defining constants for the non-globals.
Théo Zimmermann (Jun 09 2020 at 10:15):Yes, that's basically what I'm saying.
Matthieu Sozeau (Jun 09 2020 at 10:16):There might be a parsing issue too. How do you differentiate Hint f declaring a global or a constr when f has e.g. implicits?
Théo Zimmermann (Jun 09 2020 at 10:17):There is a standard disambiguation trick for users: if it is f, then it is a global, if it is (f), then it is a constr.
Théo Zimmermann (Jun 09 2020 at 10:17):I'm pretty sure that's already what happens today.
Pierre-Marie Pédrot (Jun 09 2020 at 10:20):Indeed.
Pierre-Marie Pédrot (Jun 09 2020 at 10:21):That said, I am not super happy with automatic declaration of constants. Amongst other things, you don't control on the generated name.
Pierre-Marie Pédrot (Jun 09 2020 at 10:22):ring relies on the same kind of tricks and it's not pretty
Théo Zimmermann (Jun 09 2020 at 10:23):Pierre-Marie Pédrot said:
That said, I am not super happy with automatic declaration of constants. Amongst other things, you don't control on the generated name.
Well users are not forced to use the feature.
Maxime Dénès (Jun 09 2020 at 10:24):Why not take the name in the command?
Pierre-Marie Pédrot (Jun 09 2020 at 10:24):Then I don't really see the difference with a Definition
Kenji Maillard (Jun 09 2020 at 10:24):Isn't it the point of anonymous declaration of whatever that fresh names should be generated and these should never appear to the user/interfere with his code ?
Pierre-Marie Pédrot (Jun 09 2020 at 10:24):@Kenji Maillard this is a fairy tale unfortunately
Pierre-Marie Pédrot (Jun 09 2020 at 10:25):objects have names, and they're reachable in many ways
Maxime Dénès (Jun 09 2020 at 10:25):In fact, why isn't a Hint attribute enough for @Cyril Cohen 's use case?
Pierre-Marie Pédrot (Jun 09 2020 at 10:25):I was about to hint at that
Maxime Dénès (Jun 09 2020 at 10:26):@Théo Zimmermann what does this on-the-fly declaration bring?
Pierre-Marie Pédrot (Jun 09 2020 at 10:26):but I think that his problem is that he precisely doesn't want to think about the defintion
Kenji Maillard (Jun 09 2020 at 10:26):it's an idealization rather than a fairy tale: the system should strive to keep private names hidden (it's a best effort, not a formal property)
Maxime Dénès (Jun 09 2020 at 10:27):@Kenji Maillard sure, but the problem is that we don't even have a notion of private names at the moment
Pierre-Marie Pédrot (Jun 09 2020 at 10:27):we could use modules cough cough
Kenji Maillard (Jun 09 2020 at 10:33):Maxime Dénès said:
Kenji Maillard sure, but the problem is that we don't even have a notion of private names at the moment
A fair point (I do not have much clue about what's implemented in Coq, but I do know that as a user I frequently have troubles with names and scopes).
Do module implement a form of such private names ? (I will take the risk of being thrown out of this room but I remember appreciating the fact that in Lean every datatype comes with its own namespace and that you can scope names with respect to these, cleanly in my meager experience)
Théo Zimmermann (Jun 09 2020 at 10:38):Yes, that's one of the niceties of Lean (that exist from the early days in fact).
Théo Zimmermann (Jun 09 2020 at 10:38):Coq never got proper namespaces.
Théo Zimmermann (Jun 09 2020 at 10:39):Maxime Dénès said:
Théo Zimmermann what does this on-the-fly declaration bring?
Users seem to want that (at least @Jason Gross and @Cyril Cohen).
Jason Gross (Jun 09 2020 at 16:00):Note, by the way, that Hint already does on-the-fly declaration of constants. In particular, Hint Resolve -> and Hint Resolve <- declare projections from iff lemmas, I believe.
Pierre-Marie Pédrot (Jun 09 2020 at 16:03):Yes, and you can get a fancy error if you define the name that is generated before
Pierre-Marie Pédrot (Jun 09 2020 at 16:05):Coq doesn't try to freshen the name
Pierre-Marie Pédrot (Jun 09 2020 at 16:06):It's not hard to generate a constant every time one passes a term instead of a global reference, but it's a breaking change
Michael Soegtrop (Jun 09 2020 at 17:57):@Emilio Jesús Gallego Arias : I saw that in 8.12 it is deprecated to use arbitrary terms as hints. May I ask why? I use this frequently because many lemmas are not formulated in a way suitable as hints, so I have quite a few little Gallina helper functions which convert lemmas to a more suitable form. E.g. if I use a library lemma with a conjunction as goal, I use a function to split out the left and right part and add them separately as hint. I would say half of my hints are of this type. Of cause I could define every of these as global separately, but it is not terribly convenient.
Emilio Jesús Gallego Arias (Jun 09 2020 at 18:01):@Michael Soegtrop this thread seems to be in wrong place? There is already a thread about that in the proper subforum, I didn't participate in that discussion tho, you will find lots of context on the PR and the thread
Cyril Cohen (Jun 09 2020 at 18:05):Michael Soegtrop said:
Emilio Jesús Gallego Arias : I saw that in 8.12 it is deprecated to use arbitrary terms as hints. May I ask why? I use this frequently because many lemmas are not formulated in a way suitable as hints, so I have quite a few little Gallina helper functions which convert lemmas to a more suitable form. E.g. if I use a library lemma with a conjunction as goal, I use a function to split out the left and right part and add them separately as hint. I would say half of my hints are of this type. Of cause I could define every of these as global separately, but it is not terribly convenient.
I asked the same question here yesterday. May I move your message to this same topic?
Karl Palmskog (Jun 09 2020 at 18:14):please move the messages here to the correct stream
Michael Soegtrop (Jun 09 2020 at 18:36):Sorry, I though I clicked on Coq dev - thanks for the redirection - I will continue there.
Michael Soegtrop (Jun 09 2020 at 18:46):I just wanted to mention that I am also not very happy about this. I use this frequently because many lemmas are not formulated in a way suitable as hints, so I have quite a few little Gallina helper functions which convert lemmas to a more suitable form. E.g. if I use a library lemma with a conjunction as goal, I frequently use a function to extract the left and right part and add them separately as hint or sometimes also to swap the left and right part. Or to swap the two sides of an iff. Or I add lemmas with some premises or parameters filled in. Here is an example for such a lemma transformation function:
Definition SplitConjLeft3_1 {T1 T2 T3 : Type} {P1 P2 Q1: T1->T2->T3->Prop} (L : forall (t1:T1) (t2:T2) (t3:T3), Q1 t1 t2 t3 -> P1 t1 t2 t3 /\ P2 t1 t2 t3)
: forall (t1:T1) (t2:T2) (t3:T3), Q1 t1 t2 t3 -> P1 t1 t2 t3
:= fun (t1:T1) (t2:T2) (t3:T3) (H:Q1 t1 t2 t3) => match L t1 t2 t3 H with conj l r => l end.
Yup, I would have moved them myself but I cannot do that.
Jason Gross (Jun 09 2020 at 22:08):It's not hard to generate a constant every time one passes a term instead of a global reference, but it's a breaking change
It seems reasonable to make this a flag that's deprecated, and remove it in a couple of versions?
Théo Zimmermann (Jun 10 2020 at 09:46):Yep. In any case, given the feedback that we've received on this deprecation, even before the beta is out, it seems to me that we are forced to do something about it, either right now, or before the final release.
Théo Zimmermann (Jun 10 2020 at 09:46):I see two options:
Théo Zimmermann (Jun 10 2020 at 09:47):#[ hint(db) ] Definition := in 8.13, as part of coq/ceps#42 (important change of syntax) Théo Zimmermann (Jun 10 2020 at 09:49):Hint Resolve syntax. Automatically declare global references for terms as hints. Provide a (deprecated) compatibility option that can be turned off to restore the previous behavior. This might be feasible for 8.12+beta1. Notification Bot (Jun 10 2020 at 10:34):This topic was moved here from #Dune devs & users > arbitrary terms as hints by Cyril Cohen
Cyril Cohen (Jun 10 2020 at 10:36):I just moved this message which was posted on the wrong stream, from @Michael Soegtrop
Cyril Cohen (Jun 10 2020 at 11:26):Maxime Dénès said:
In fact, why isn't a Hint attribute enough for Cyril Cohen 's use case?
Sorry I forgot to answer. In the use case I have, I define several hints in line and without giving them names (since they are meant to be used by auto only), and thus not adding them to the environement. It's much less verbose that way.
Maxime Dénès (Jun 10 2020 at 11:39):I see, thanks. I guess we should figure out a way to properly generate constants on the fly, then.
Théo Zimmermann (Jun 10 2020 at 12:57):OK, so that would be option 3. In the meantime, what to do? Backtrack on the deprecation in 8.12?
Cyril Cohen (Jun 10 2020 at 13:03):Maxime Dénès said:
I see, thanks. I guess we should figure out a way to properly generate constants on the fly, then.
If so they must be automatically tagged in a way to exclude them from Search
Théo Zimmermann (Jun 10 2020 at 13:04):It's easy and we're already doing this for abstract lemmas.
Pierre-Marie Pédrot (Jun 10 2020 at 13:54):Please don't backtrack on deprecation, or we're never going to make any progress on the issue of term as hints.
Pierre-Marie Pédrot (Jun 10 2020 at 13:54):This has been lingering for a few versions already.
Pierre-Marie Pédrot (Jun 10 2020 at 13:54):I'd rather define constants on the fly.
Pierre-Marie Pédrot (Jun 10 2020 at 13:55):The reason I didn't do that was essentially backwards compatibility.
Pierre-Marie Pédrot (Jun 10 2020 at 13:57):So, if our end-users are OK with it I can implement the automatic declaration of constants, but I need to be sure that this is what is wanted.
Pierre-Marie Pédrot (Jun 10 2020 at 13:58):Note that a similar problem occurs with terms passed to (e)auto through the using clause.
Pierre-Marie Pédrot (Jun 10 2020 at 13:58):I planned to replace that with an automatic declaration of a hypothesis, but once again this is a breaking change.
Pierre-Marie Pédrot (Jun 10 2020 at 13:59):More generally, what's the process to change the behaviour of a feature ?
Cyril Cohen (Jun 10 2020 at 13:59):Pierre-Marie Pédrot said:
More generally, what's the process to change the behaviour of a feature ?
This needs a topic of its own...
Pierre-Marie Pédrot (Jun 10 2020 at 14:00):Right, but the particular problem at hand fits the topic.
Pierre-Marie Pédrot (Jun 10 2020 at 14:00):I was under the impression that it was better to first deprecate a feature which we wanted to change somehow
Pierre-Marie Pédrot (Jun 10 2020 at 14:00):so that at version n+2 you can replace it
Pierre-Marie Pédrot (Jun 10 2020 at 14:01):that could be the plan for term-as-hints
Cyril Cohen (Jun 10 2020 at 14:01):I think the point is that people that complained here do not want the syntax to be deprecated, even though the behavior might change.
Pierre-Marie Pédrot (Jun 10 2020 at 14:02):Right, but they may have to change their use anyways, if it's breaking stuff
Cyril Cohen (Jun 10 2020 at 14:08):Pierre-Marie Pédrot said:
Right, but they may have to change their use anyways, if it's breaking stuff
I would agree if there were no increase in verbosity.
A different syntax for the same thing is ok as long as it triggers a locally constant expansion of the code.
Here our complain is that the result is more verbose for no user-good reasons.
Théo Zimmermann (Jun 10 2020 at 14:17):@Pierre-Marie Pédrot The process is that you change the behavior and provide a deprecated compatibility option, that you can set in the appropriate compat file.
Théo Zimmermann (Jun 10 2020 at 14:17):My question about backtracking on the deprecation was only about the v8.12 branch.
Théo Zimmermann (Jun 10 2020 at 14:18):Because I can't see the declaration on the fly feature being implemented in time for 8.12+beta1.
Pierre-Marie Pédrot (Jun 10 2020 at 14:23):What about having another beta? It's quite a minor change.
Pierre-Marie Pédrot (Jun 10 2020 at 14:24):I really don't want to postpone the deprecation again.
Pierre-Marie Pédrot (Jun 10 2020 at 14:24):This is holding back a big cleanup of the hint databases, which are currently complete nonsense.
Cyril Cohen (Jun 10 2020 at 14:29):Pierre-Marie Pédrot said:
This is holding back a big cleanup of the hint databases, which are currently complete nonsense.
I do not understand the link. What cleanup are you referring to, and what prevents you from doing it without deprecating the feature? AFAIK the deprecation is about a restriction anyway...
Théo Zimmermann (Jun 10 2020 at 14:32):OK fine for the second beta... but please prepare the PR soon so that it doesn't come very late in the process.
Pierre-Marie Pédrot (Jun 10 2020 at 15:58):OK, I'm writing it right now, should be fast.
Pierre-Marie Pédrot (Jun 10 2020 at 16:18):Should I leave a warning or just remove it altogether?
Théo Zimmermann (Jun 10 2020 at 16:18):I think it should be removed.
Pierre-Marie Pédrot (Jun 10 2020 at 16:19):OK, I am reusing the same piece of code as for Hint ->, so we don't get to see any message saying it's declaring something in your back
Théo Zimmermann (Jun 10 2020 at 16:19):But another option could be to leave the deprecation warning and to tell users to turn the option on to change the behavior and disable the warning.
Pierre-Marie Pédrot (Jun 10 2020 at 16:20):I think that the option should be on by default
Pierre-Marie Pédrot (Jun 10 2020 at 16:21):And what lovely name should we give to this option?
Pierre-Marie Pédrot (Jun 10 2020 at 16:21):I prefer to ask before bikeshedding sets in
Théo Zimmermann (Jun 10 2020 at 16:21):Auto Declare Hints?
Théo Zimmermann (Jun 10 2020 at 16:21):Anyway, that can be anything, but please make it shorter than what @Jason Gross proposed in the issue.
Pierre-Marie Pédrot (Jun 10 2020 at 16:22):Auto is confusing, given that we have the auto tactic
Pierre-Marie Pédrot (Jun 10 2020 at 16:23):I think I'll call it "Declare Hint Proxy"
Pierre-Marie Pédrot (Jun 10 2020 at 16:30):See https://github.com/coq/coq/pull/12493. It's missing documentation and changelog, but the code should be fine.
Pierre-Marie Pédrot (Jun 10 2020 at 16:44):The documentation currently doesn't mention that one can declare arbitrary terms as hints
Théo Zimmermann (Jun 10 2020 at 16:46):Indeed, that's probably because devs have planned to remove the feature for a long time already.
Théo Zimmermann (Jun 10 2020 at 16:46):But undocumented doesn't mean unused.
Théo Zimmermann (Jun 10 2020 at 16:46):It seems like it is time to finally document it.
Pierre-Marie Pédrot (Jun 10 2020 at 16:46):I git-blamed, and actually I was the one to tweak the doc in the deprecation PR, although I didn't remember
Pierre-Marie Pédrot (Jun 10 2020 at 16:46):the comment says that the doc was outdated though
Pierre-Marie Pédrot (Jun 10 2020 at 16:47)::shrug:
Pierre-Marie Pédrot (Jun 10 2020 at 16:47):I don't know how to make the doc change readable though
Pierre-Marie Pédrot (Jun 10 2020 at 16:48):because it's really two different commands depending on the shape of the parsed result
Pierre-Marie Pédrot (Jun 10 2020 at 16:48):should I write a variant?
Théo Zimmermann (Jun 10 2020 at 16:52):Nah, you can replace @qualid by @one_term and explain that if @one_term is not an existing global reference, then a global reference will be generated on the fly.
Last updated: Jun 04 2023 at 19:30 UTC