[protocol] Add `Search` support.

ejgallego commented 6 years ago

Right now, the code for search reads:

  | Search         -> [CoqString "Not Implemented"]

Names provides a very restricted subset of Search, however we should unify

A question is what kind of object we'd like to return from Search, right now we just return names, but certainly a richer information would be appreciated.

cc: ejgallego/coq-serapi#51

kiranandcode commented 2 years ago

Any update on whether this will be supported? Are there some fundamental architectural issues that are blocking this feature? If not, I don't mind taking a crack at implementing this in a separate PR - it would be particularly useful for my own projects.

kiranandcode commented 2 years ago

I guess in the meanwhile I am able to make do with:

  let evd = Evd.from_env env in
  let acc = ref [] in
  Search.search env evd query ([], false) (fun refr kind _ typ ->
    acc := (refr,kind,typ) :: !acc
  )

JasonGross commented 2 years ago

A question is what kind of object we'd like to return from Search, right now we just return names, but certainly a richer information would be appreciated.

The amount of information returned should be configurable, otherwise I expect you'll run into performance issues as company-coq does when trying to find all names available for autocompletion.

ejgallego commented 2 years ago

@Gopiandcode , not a lot of progress on this, as indeed current Search.search does a linear traverse of the objects in Coq's scope, so I was hoping we could have improved the base Coq's search implementation first.

You are very welcome tho to submit a PR even with the linear scan performance issue, as @JasonGross points out, having a bit of a filter setup would alleviate that. Note that Query already has a place in the protocol for paginating results and filters.

mattam82 commented 12 months ago

Any hope to make a quick and dirty search/searchabout available? Even when writting Search foo in the document I don't see any result. It's kind of crucial to work on large libraries. And definitely the existing coq-lsp speedup is far more important than Search's performance.

Alizter commented 12 months ago

@mattam82 That's strange. Search should show something in the panel. Is your typing cursor over the Search statement?

mattam82 commented 12 months ago

Ah I see, it was just after the statement

Alizter commented 12 months ago

@mattam82 There is an option that shows the messages of the sentence before the cursor which might be useful if you find yourself backtracking alot.

ejgallego commented 11 months ago

@mattam82 I fully agree we need better search; I've discussed with some people about plans, but so far no one took on it yet, and my backlog is a bit large these days.

Indeed we can now do a bit better with how the cursor works I think, as always this kind of stuff is subtle.

What happens in Coq now when Search foo. is typed is that the sentence will indeed stop at the point.

I think the option @Alizter mentions doesn't affect the display of messages, but only of goals.