More search options

[herbelin]

Kind: feature

This is a proposal to extend the search mechanism with the following modifiers:

• hyp:notation_string, hyp:pattern to restrict the search in the hypotheses of the statement
• concl:notation_string, concl:pattern to restrict the search in the conclusion of the statement (this is a bit stronger than SearchHead as the pattern can occur in any position of the conclusion, not only in head position; so, this is like ssreflect "head" search)
• is:Instance, is:Coercion, is:Conjecture, is:Example, is:[Instance Coercion], etc. to restrict the search to object of the given kind (or kinds, if a list)

Example:

Require Import Morphisms.
Search is:Instance iff -Proper.
(*
iff_equivalence: Equivalence iff
iff_Transitive: Transitive iff
iff_Symmetric: Symmetric iff
iff_Reflexive: Reflexive iff
RewriteRelation_instance_1: RewriteRelation iff
iff_impl_subrelation: subrelation iff Basics.impl
iff_flip_impl_subrelation: subrelation iff (Basics.flip Basics.impl)
*)

This should address #8663 but this should eventually also pave the way towards more fine-tunable search drivable from Graphical User Interfaces.

Suggestions, new ideas welcome.

With respect to ssreflect's Search, I made only the minimal changes so that it compiles. What to do?

Polishing and documentation to be done after first feedback.

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in CHANGES.md.

Overlays:

• Adapt to small change of search API (Coq PR #8855). coq-community/coq-dpdgraph#72
• Adapt to change of search API (Coq PR #8855). lukaszcz/coqhammer#66

[gares]

Looks very interesting. I don't have time to dive into the implementation, hence some doc would be helpful.
For example I don't get what is the difference between repeating a filter and using the list, eg is:Instance is:Coercion and is:[Instance Coercion]. I guess the filters are in conjunction, so I don't get the need for the list operation.

[herbelin]

I guess the filters are in conjunction, so I don't get the need for the list operation.

The list notation is to indicate a disjunction. We could also adopt the convention that several is: clauses are collected by default into a disjunction, but I was afraid that it might be confusing.

[gares]

I'm sorry but at least for is: I don't think I see any use for disjunction.
So I'm asking you if you have a concrete use case for that disjunction?

Don't get me wrong, I think being able to query the type classes or coercions db via Search is a very good feature and can probably subsume stuff like Print Canonical Projections or the equivalent command for type classes (that now I don't recall).
But I quite don't see why one would need query two data bases within the same query. I mean, one can always write two Search queries.
And the little output example you give does not show in which db the term was found, and knowing that x is either a coercion or a TC instance is not very useful: being in a db or the other changes very much how x is can be used.
Finally I may have a use case for querying constants being both coercions and canonical structures (they play an important role in type inference, and knowing one of them is missing may help debugging). But I don't see any use for the dual query.

[herbelin]

I'm sorry but at least for is: I don't think I see any use for disjunction.
So I'm asking you if you have a concrete use case for that disjunction?

A typical query would be is:[Theorem Lemma], or is:[Theorem Axiom].

But, of course, it all depends on what kind of arguments would be the most interesting to give to is:. Currently it supports a subset of Decl_kinds.logical_kind,, and this is what Theorem or Axiom are referring to above, but we could alternatively provide a custom list of attributes. For instance, we could also discriminate on Transparent, Opaque. Or we could discriminate less cosmetically than using the words Axiom/Parameter, Conjecture and Theorem/Lemma/Definition by using, say, the words Assumption, Admitted, Qed.

I implemented only a subset of Decl_kinds.logical_kind because it was not straightforward to implement all and also precisely because I was not fully decided on what kind of criterion we may eventually want to stabilize.

[Zimmi48]

With respect to ssreflect's Search, I made only the minimal changes so that it compiles. What to do?

If this eventually subsumes the features provided by SSR's Search and everyone is satisfied by the new search language, delete it (or at least deprecate it). Search should not be left in finished proof scripts so there is no problem with removing it.

[gares]

I implemented only a subset of Decl_kinds.logical_kind because it was not straightforward to implement all and also precisely because I was not fully decided on what kind of criterion we may eventually want to stabilize.

Are you saying that writing
Instance foo := ... and Definition foo := ... . Existing Instance foo would give different results?

I'm fine for Lemma and Theorem, these are annotations with just one syntax. But Instance and Coercion have two for example.

I really think I need to see some doc, otherwise the discussion is not going to converge.

[herbelin]

Are you saying that writing
Instance foo := ... and Definition foo := ... . Existing Instance foo would give different results?

Yes, I'm saying that, the way it is currently implemented, this gives different results. I'm not saying that this is the optimal decision to take. It is indeed probably more interesting to have a way to query what is declared as an instance, and maybe even to discriminate between different kinds of instance.

I really think I need to see some doc, otherwise the discussion is not going to converge.

If you're waiting for a final product, then, you should indeed wait. If you want to continue to contribute to the discussion, e.g. by listing attributes one would like to discriminate, you are most welcome.

[herbelin]

Are you saying that writing
Instance foo := ... and Definition foo := ... . Existing Instance foo would give different results?

A possible idea to address this would be to register searching keys and to add to declare_object a method of type, say unit -> (Glob.Ref.t * search_key list) list which would tell which properties of which global references the object is providing (something somehow related to what @SkySkimmer has in #8491). For instance, the "instance" object would tell that "foo" is an instance in both the Instance foo case and the Existing Instance foo case.

@gares: You expressed a strong interest in this extension of Search. Would you be interested to investigate what could be done further in this direction?

[SkySkimmer]

Searching by the Coercion/Instance decl kinds may be more confusing than it's worth considering it won't find Existing Instance, record projections declared as coercions, etc.
I think we should at least print a warning like "you restricted search to Instance, be aware that this will only allow constants originally defined with the Instance keyword".

[herbelin]

@SkySkimmer: I fully agree. If ever we want to search on the keyword of the command, it should a minima be, say keyword: Instance, keyword: "Existing Instance", ... but what we want in practice is a priori to search on the effective status of being an instance than on the keyword which introduced the command.

[Zimmi48]

It would make a lot of sense if the language of kinds to search was the same as the one of kinds to import, yes.

[gares]

@gares: You expressed a strong interest in this extension of Search. Would you be interested to investigate what could be done further in this direction?

I have no time for that, sorry

[herbelin]

I have no time for that, sorry

But you do think that it would be worth to be done, right?

[gares]

Absolutely. I think the idea emerging here of exposing more metadata via search is great, but of course it needs to be exposed in a "faithful" way, e.g. abstract over the syntax used to attach the metadata to an object.

[herbelin]

OK, thanks for positive feedback. So, let's pile this on the list of wishes. I'll decide by a couple of weeks if I split the PR to keep at least hyp: and concl:, and, if I retarget is: as, say, keyword: or not.

[ppedrot]

@herbelin any news on this front?

[JasonGross]

This should possibly also be profiled on something? I know Search already has performance issues that show up in company-coq when I have many identifiers in the environment.

[Zimmi48]

The promote target for the test-suite may help.

I'm using the approve-output target from the test-suite's Makefile (which is compatible with building with dune).

[Zimmi48]

But I also need to tweak the examples in the documentation because the output for the Search commands that I show has become too large following #11948.

[gares]

I'm sorry I could not help much here. I'll try to get feedback from math-comp people as soon as 8.12 is released, so that we can see if we can finally get rid of ssrsearch. Even reading the discussion again I can't say if it 100% subsumes the old code, I guess the best is to try it and see.

[Zimmi48]

@proux01 I've added a Add Search Blacklist "internal_". to the documentation examples, but I wonder if it shouldn't be also in the stdlib.

[proux01]

@proux01 I've added a Add Search Blacklist "internal_". to the documentation examples, but I wonder if it shouldn't be also in the stdlib.

Maybe, I don't have a strong opinion. The new material is mostly useful for numeral notations but is not expected to be useful directly for most users, so that sounds reasonnable.

Sorry for the inconvenience!

[ejgallego]

Overlay for dpdgraph seems to need to be fixed?

[Zimmi48]

@herbelin Can you look into it? I could also take care of it but I don't know when I will find a minute to do it.

[ejgallego]

After reading the discussion carefully I'm concerned about the deprecation plan for ssr's search; if I understand things correctly ssr users will be silently switched to the new search without a warning, IMO this is very confusing; Coq should instead use the old semantics for one release but warn users to import the module.

Removal in the next release is IMO not factible, one extra release is needed so users can provide adequate feedback.

[ejgallego]

Coq should instead use the old semantics for one release but warn users to import the module.

That should be pretty easy to do as warning [as we did for example when we removed Funind from the Prelude] , so this PR doesn't need to wait for that; can be done as a separate, 8.12-only PR.

[herbelin]

Overlay for dpdgraph seems to need to be fixed?

Done

[Zimmi48]

What I can do is to add a warning to the default Search command that is emitted when SSReflect has been loaded so that users are made aware that this is not SSReflect's Search and that they need to require ssrsearch to access it.

[ejgallego]

What I can do is to add a warning to the default Search command that is emitted when SSReflect has been loaded so that users are made aware that this is not SSReflect's Search and that they need to require ssrsearch to access it.

Yup, we can do this, but IMHO only in 8.12 , WDYT?

[Zimmi48]

Yes, good idea. Then I'll open an 8.12-only PR after the branch has been created.

[ejgallego]

Ok, will merge then and open an issue.