Stream: Coq users

Topic: How to search in Coq?


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

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

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

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

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

view this post on Zulip Théo Zimmermann (Oct 21 2020 at 09:37):

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

view this post on Zulip Théo Zimmermann (Oct 21 2020 at 09:37):

https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.search

view this post on Zulip Théo Zimmermann (Oct 21 2020 at 09:37):

Changelog entry: https://coq.inria.fr/refman/changes.html#search

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

And: https://coq.inria.fr/refman/changes.html#ssrsearch

view this post on Zulip Ralf Jung (Oct 21 2020 at 09:43):

thanks for the pointers!

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

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

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

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

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

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

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

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

view this post on Zulip Christian Doczkal (Oct 22 2020 at 09:32):

@Théo Zimmermann I opened a new issue

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

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.

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

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

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

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

view this post on Zulip Ralf Jung (Oct 22 2020 at 17:04):

that's way more effort as I need a setup to be able to build-test things... not sure when I'll be able to make time for that

view this post on Zulip Ralf Jung (Oct 22 2020 at 17:04):

unless you're fine with me just submitting a PR I didnt even try to build

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 17:50):

+1, that’s what CI is for

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 17:51):

this has been explicitly encouraged for documentation, and I think that applies to error messages.

view this post on Zulip Ralf Jung (Oct 22 2020 at 19:19):

Here's a strawman proposal: https://github.com/coq/coq/pull/13257

view this post on Zulip Ralf Jung (Oct 22 2020 at 19:19):

I didn't know what to do with these checkboxes ;) they do not apply here I think? I hope?^^

view this post on Zulip Li-yao (Oct 22 2020 at 19:23):

That's right, they only make sense for bigger changes. You can ignore them.

view this post on Zulip Théo Zimmermann (Oct 22 2020 at 19:50):

Ralf Jung said:

unless you're fine with me just submitting a PR I didnt even try to build

Yep, this is always fine!


Last updated: Jan 27 2023 at 00:03 UTC