[protocol] Add `Search` support. about coq-lsp

[ejgallego]

@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.

[kiranandcode]

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]

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]

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.

[mattam82]

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]

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

[mattam82]

Ah I see, it was just after the statement

[Alizter]

@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]

@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.

[adrianleh]

In 0.1.8 for Coq v8.18, I no longer see any results in messages when I use Search/Check/Print. This was not an issue previously on Coq 8.16 with lsp.

[Alizter]

@adrianleh Do you see the results when your cursor is over the Search statement or before and after it. There is a configuration option that displays the goal / messages at the cursor vs just before.

[adrianleh]

I only see it upon mouse-over, however there is no text cursor state (either before or after the period) where is see it.

[adrianleh]

Screen.Recording.2024-01-30.at.16.04.13.mov

[Alizter]

@adrianleh Hmm that is very strange. Does the same happen when you do a check at the top of the file? Sometimes a hanging proof may stop the goal window from being updated.

I have the same version numbers as you and I haven't seen any such issue when using Search.

[adrianleh]

This happens anywhere in the file

[ejgallego]

Hi @adrianleh , it seems to me that this is a problem with the extension being activated multiple times, and maybe some configuration mixup.

I think coq-lsp Zulip could be a better place to discuss this, would you mind if we move the discussion there?

[adrianleh]

Adding https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/LSP.20search.20issue/near/419497086 as a reference