`error` field of `proof/goals` does not respect `goal_after_tactic`

[jpoiret]

Describe the bug If goal_after_tactic is set to false, the error field of the proof/goals request will contain the error message of the sentence under the requested position (seemingly executing it?) instead of the last sentence.

Desktop (please complete the following information):

• coq-lsp 0.2.2-8.20.0
• using my own rocq-mode.el on Emacs

[ejgallego]

Thanks @jpoiret , indeed the logic for goals and errors is different. I think here you may be witnessing 2 things:

• over-execution: in 0.2.2 we detected some commands do over-execute, this will be fixed in 0.2.3
• the logic for errors don't respect the attribute

So indeed, these could be two issues that interact but are different.

Can you provide an example .v Rocq file so we can reproduce the problem and add a test to the test-suite? Thanks!

[ejgallego]

Ping @jpoiret , I want to check that my understanding of this issue is correct:

I guess you want a fully lazy mode, so that sentences are not executed while you are writing it, correct?

In the first LSP prototypes, the idea is that the client would only issue the goals request when it wanted to display the goals, for example if you are in "on-demand mode", when the user press "Ctrl+Enter" (display goals), but I can see how this is inconvenient.

The behavior here is subtle so I'd like to be sure the fix captures your workflow properly.

[jpoiret]

I don't think the problem really is about execution, but rather the contents of the returned response: the error field of a proof/goals request should return the errors of the sentence that the proof/goals request targets, for consistency, rather than always the one under point.

Wrt. a fully lazy mode, I believe lsp-coq already supports it with the check on request mode. It just is surprising that when requesting a goal display for the sentence before the one under point, the sentence under point would also get executed.

[jpoiret]

As for a sample .v file, the following is sufficient to demonstrate the behavior:

Goal True -> False.
  intros ?.
  constructor.

If you have goal_after_tactic set to false, and request proof/goals with the point on the first t of constructor, you will get The type has no constructors. in the error field.

[ejgallego]

@jpoiret thanks for the example, I'm still not sure tho what the best fix for this issue is.

As you note, requesting a goal will indeed force the execution of the sentence at point. This is a bit hard to change, I'll explain why.

When we request information of a document point, it can be the case that we didn't check the document to that point yet. If that's the case, we postpone the request and schedule document checking to that point. If we reach that point, we answer the request.

Unfortunately, we cannot know in advance when we have reached the previous sentence for a particular position without at least calling the Rocq parser, which implies a fair amount of execution (for example syntax errors would happen).

This is due to Rocq's grammar being extensible.

So, we could change the behavior of error display, but we would still execute the sentence.

Am I correct that you want to avoid execution? If that's the case, the only way is not to issue proof/goals, at least for now.

We introduced goal_after_tactic as accommodate some display preferences; I'm not sure it was a good idea. For sure, based on what you tell me, it needs more improvement.

I wonder about the use case, taking your example, if the client issues proof/goals at the first t of constructor, why would we display information about intros ? ?