How to search in Coq? · Coq users

Stream: Coq users

Topic: How to search in Coq?

Ralf Jung (Oct 21 2020 at 08:07):

For many months, PG showed warnings that SearchAbout is deprecated and one should use Search instead. PG changed to accommodate this, only to immediately run into a new warning:

Warning: SSReflect's Search command has been moved to the ssrsearch module; please Require
that module if you still want to use SSReflect's Search command [ssr-search-moved,deprecated]

Looks like search commands are being deprecated faster than tools can keep up :joy: .
So what is the command one should use instead? What is "the best search command" in latest Coq right now? The error tells me how I can keep using the deprecated Search, but it does not tell me what the non-deprecated alternative is...

Théo Zimmermann (Oct 21 2020 at 09:02):

This deprecation message was added so that users of SSR Search are not surprised by the change of behavior. It's not entirely satisfying. There is nothing you need to do, except probably disable that warning.

Théo Zimmermann (Oct 21 2020 at 09:06):

If this command is used through PG instead of SearchAbout, then I think PG maintainers themselves should disable that warning.

Ralf Jung (Oct 21 2020 at 09:26):

So there are two Search, one in ssreflect and one in main Coq? What is the difference between the two? Is there some way I can already opt to use the "new default" now so I can give feedback if it works well enough?

Théo Zimmermann (Oct 21 2020 at 09:37):

You are already (by default) using the new default. This warning is just to make you aware of this. If you were previously using SearchAbout, it is a strict extension.

Théo Zimmermann (Oct 21 2020 at 09:37):

I suggest having a look at the documentation to learn more about the new features.

Ralf Jung (Oct 21 2020 at 09:43):

thanks for the pointers!

Pierre Courtieu (Oct 22 2020 at 07:45):

Théo Zimmermann said:

If this command is used through PG instead of SearchAbout, then I think PG maintainers themselves should disable that warning.

Why would PG remove the warning? We don't want to use the deprecated SearchAbout, and if coq devs think the warning is useful I don't think we should hide it.
What is the new ssreflect search command? Is there a shortcut or menu for it in PG currently?

Théo Zimmermann (Oct 22 2020 at 08:25):

PG used to call SearchAbout which was a deprecated variant of Search. But SearchAbout was useful because when users loaded SSR, SearchAbout was the way to keep using the normal Search command instead of SSR's Search command.

Théo Zimmermann (Oct 22 2020 at 08:26):

There is no new ssreflect search command. On the contrary, we want to get rid of it. Starting in 8.12, it is deprecated and buried in a separate plugin that you have to load separately.

Théo Zimmermann (Oct 22 2020 at 08:27):

However, some developers thought it was important to warn SSR users using Search that they were now using the default search unless they loaded the new ssrsearch plugin. This is the reason of the warning.

Théo Zimmermann (Oct 22 2020 at 08:28):

If the Search command is used as a replacement of SearchAbout, then there is no reason to raise this warning.

Théo Zimmermann (Oct 22 2020 at 08:28):

But honestly, I think that introducing this warning was a mistake in the first place because it just brought a lot of confusion.

Christian Doczkal (Oct 22 2020 at 08:52):

Théo Zimmermann said:

But honestly, I think that introducing this warning was a mistake in the first place because it just brought a lot of confusion.

I would disagree on that one. When I upgraded to 8.12, this warning probably saved me quite a bit of time/confusion, because I had been using the Ssreflect search command for a long time, frequently with the in restriction (which is now inside).

I find the new search command to be a definite improvement, even though I'm a bit annoyed that the new search doesn't automatically insert the necessary coercions to make the pattern a type when using headconcl:. That is, one has to search for headconcl:(is_true (_ <= _)) rather than headconcl:(_ <= _) to get the expected results.

Théo Zimmermann (Oct 22 2020 at 09:04):

@Christian Doczkal Thanks a lot for the feedback. That's the first positive feedback I get for the warning. Also, would you mind opening an issue about the automatic coercion insertion? This could be an oversight.

Christian Doczkal (Oct 22 2020 at 09:32):

@Théo Zimmermann I opened a new issue

Ralf Jung (Oct 22 2020 at 09:52):

Théo Zimmermann said:

But honestly, I think that introducing this warning was a mistake in the first place because it just brought a lot of confusion.

I think the warning could have been worded more clearly, to explicitly say:

if you were using ssreflect Search before, behavior now changed
if you were using Coq's SearchAbout before, now Search behaves the same as SearchAbout did before

From the warning it was not entirely clear to me if it was telling me behavior will change in the future or has changed recently.

Ralf Jung (Oct 22 2020 at 09:52):

but on top of that my problem here was that I did not even know which command PG was using for me

Théo Zimmermann (Oct 22 2020 at 12:26):

In 8.13 the warning will be removed. But we could improve the wording in 8.12.1 which is about to be released. WDYT?

Ralf Jung (Oct 22 2020 at 14:05):

Théo Zimmermann said:

In 8.13 the warning will be removed. But we could improve the wording in 8.12.1 which is about to be released. WDYT?

I'm happy to give feedback to a proposed wording, or propose a wording.

Théo Zimmermann (Oct 22 2020 at 15:18):

If you open the PR, it's the best way to ensure that it will happen! The text to change is in plugins/ssr/ssrvernac.mlg. You may want to make the PR on the v8.12 branch only, since master already has coq/coq#13231 that removes the warning.