Confusing error when asking to "Print" on a term that is not yet processed

[RalfJung]

To reproduce, have a file where nat is used multiple times, and then process that file part-way by putting the cursor between the two uses and hitting "Alt-Right":

Definition a (x : nat) := x. (* process until here *)
Definition spacer := ().
Definition b (x : nat) := x.

Now move the cursor over the 2nd nat, and hit Ctrl-Alt-A, which should run About nat. Confusingly, this gives an error: "No context found". It is quite unclear to a user what that error means. Trying to get info about the exact same term, nat, by putting the cursor on the 1st nat works fine.

My guess is that vscoq tries to take into account the context of the proof at the place where the identifier is used, and of course that fails for the 2nd nat as that part has not been processed yet. However, during proof development it is quite common to need information about an identifier in the next command because that command fails for some reason -- not being able to use Ctrl-Alt-A for that is not great. IMO if the proof state isn't available for the exact location where the identifier is used, vscoq should just should the proof state for the closest previous available location. That will almost always be right, and makes it possible to lookup identifiers in commands that do not succeed processing yet.

[RalfJung]

Okay, turns out this works fine if the identifier I am looking for is immediately in the next command after what has currently been processed. So in the case where one debugs the immediate next command, things work as expected.

But it would still be nice to also be able to print things from further down the file.

[rtetley]

This is a more general issue related to the query panel. Right now, when you prompt a search this is what happens:

• It send a loc and a string to the server
• The sever tries to find a context with that loc (if it does not find one, you get your error)
• Searches in that context

Now for manual mode this is easily fixed: just make sure the context is always the green executed area.

For continuous mode it gets tricky. What context should one use ?

[RalfJung]

Now for manual mode this is easily fixed: just make sure the context is always the green executed area.

Are you saying the user should make sure of that, or the server?

[rtetley]

The server. Right now the context is the loc where your cursor is when you launch the request (not sure if it was clear before). The server can make sure it chooses the green zone context.

[rtetley]

This is a more general issue related to the query panel. Right now, when you prompt a search this is what happens:

• It send a loc and a string to the server
• The sever tries to find a context with that loc (if it does not find one, you get your error)
• Searches in that context

Now for manual mode this is easily fixed: just make sure the context is always the green executed area.

For continuous mode it gets tricky. What context should one use ?

For example, say you have opened a document that requires heavy computation in continuous mode. The server is busy executing the document and is about half way through. You launch a Search. What would be the desired outcome ?

• Should the query take precedence even if the context is "incomplete" ?
• Should we wait until the document is fully processed ?

[RalfJung]

We should never have to wait until the document is fully processed, only until the point where the cursor is is processed, right?

[rtetley]

I like that solution ! And it will be easy to do I believe !

[rtetley]

We've been discussing this internally and it has lead me to believe that the best solution for this and #906 is probably something like #659. You would get a search tool much like the query panel in the proof view and the results would come up in the messages section. This will make it very unambiguous in which state a query is being performed.

For the query panel either:

• we keep it as a "save" feature (you could save the results from a given query in that panel
• we wait till we have some sort of global search tool but that is a much larger question