Stream: Coq devs & plugin devs

Topic: declaring arbitrary terms as hints is deprecated


view this post on Zulip 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...

view this post on Zulip Ali Caglayan (Jun 08 2020 at 20:15):

Is this because you need to specify a hint database?

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jun 08 2020 at 20:38):

Ali Caglayan said:

Would Local Definition be 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jun 08 2020 at 23:12):

You could define a specific "Hint_" prefix and ignore that during search too.

view this post on Zulip 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..

view this post on Zulip 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?)

view this post on Zulip Maxime Dénès (Jun 09 2020 at 09:53):

Search blacklisting should be done by an attribute, not hacking a prefix IMHO

view this post on Zulip Matthieu Sozeau (Jun 09 2020 at 10:10):

That would be nicer indeed

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 10:15):

Yes, that's basically what I'm saying.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 10:17):

I'm pretty sure that's already what happens today.

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:20):

Indeed.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:22):

ring relies on the same kind of tricks and it's not pretty

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Jun 09 2020 at 10:24):

Why not take the name in the command?

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:24):

Then I don't really see the difference with a Definition

view this post on Zulip 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 ?

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:24):

@Kenji Maillard this is a fairy tale unfortunately

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:25):

objects have names, and they're reachable in many ways

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:25):

I was about to hint at that

view this post on Zulip Maxime Dénès (Jun 09 2020 at 10:26):

@Théo Zimmermann what does this on-the-fly declaration bring?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 10:27):

we could use modules cough cough

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Jun 09 2020 at 10:38):

Coq never got proper namespaces.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 16:05):

Coq doesn't try to freshen the name

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jun 09 2020 at 18:14):

please move the messages here to the correct stream

view this post on Zulip Michael Soegtrop (Jun 09 2020 at 18:36):

Sorry, I though I clicked on Coq dev - thanks for the redirection - I will continue there.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 09 2020 at 18:52):

Yup, I would have moved them myself but I cannot do that.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 09:46):

I see two options:

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 09:47):

  1. Backtrack on the deprecation in 8.12, implement #[ hint(db) ] Definition := in 8.13, as part of coq/ceps#42 (important change of syntax)

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 09:49):

  1. Keep the 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.

view this post on Zulip Notification Bot (Jun 10 2020 at 10:34):

This topic was moved here from #Dune devs & users > arbitrary terms as hints by Cyril Cohen

view this post on Zulip Cyril Cohen (Jun 10 2020 at 10:36):

I just moved this message which was posted on the wrong stream, from @Michael Soegtrop

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 13:04):

It's easy and we're already doing this for abstract lemmas.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 13:54):

This has been lingering for a few versions already.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 13:54):

I'd rather define constants on the fly.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 13:55):

The reason I didn't do that was essentially backwards compatibility.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 13:59):

More generally, what's the process to change the behaviour of a feature ?

view this post on Zulip 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...

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 14:00):

Right, but the particular problem at hand fits the topic.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 14:00):

so that at version n+2 you can replace it

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 14:01):

that could be the plan for term-as-hints

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 14:17):

My question about backtracking on the deprecation was only about the v8.12 branch.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 14:23):

What about having another beta? It's quite a minor change.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 14:24):

I really don't want to postpone the deprecation again.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 15:58):

OK, I'm writing it right now, should be fast.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:18):

Should I leave a warning or just remove it altogether?

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 16:18):

I think it should be removed.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:20):

I think that the option should be on by default

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:21):

And what lovely name should we give to this option?

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:21):

I prefer to ask before bikeshedding sets in

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 16:21):

Auto Declare Hints?

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:22):

Auto is confusing, given that we have the auto tactic

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:23):

I think I'll call it "Declare Hint Proxy"

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:44):

The documentation currently doesn't mention that one can declare arbitrary terms as hints

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 16:46):

But undocumented doesn't mean unused.

view this post on Zulip Théo Zimmermann (Jun 10 2020 at 16:46):

It seems like it is time to finally document it.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:46):

the comment says that the doc was outdated though

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:47):

:shrug:

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:47):

I don't know how to make the doc change readable though

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 16:48):

should I write a variant?

view this post on Zulip 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: Oct 21 2021 at 22:02 UTC