feat: adding option for interpreting to exact cursor position or next command during interpret to point

[Durbatuluk1701]

This PR adds a "interpret to next point" that will take the current cursor position and if it is part of a tactic then it will interpret through the completion of that tactic.

This should fix #870

Some test cases have also been added to test the function to find the end of the next tactic.

I am not sure if we want this to be the default behavior for continuous mode or should be an option that can be enabled.

[Durbatuluk1701]

Another possibility I have considered is that the getNextPosition function could be utilized in continuous mode to help prevent repeatedly sending interpretToPoint requests that won't change the proof state since they are mid tactic.

For example (where | represents a cursor):
ta|c1. tac2 transitioning to tac|1. tac2
Should not need a new interpretToPoint request as no proof state change would occur.

[rtetley]

I like this ! However I wonder if finding the correct position should be done on the server side rather. What do you think @gares ?

[rtetley]

Also I think it should be an option maybe other users can give their sentiment about this ?

[gares]

I love it too, thanks!

The lang server knows the end of sentences, it should compute what next means.

[SkySkimmer]

This PR adds a "interpret to next point" that will take the current cursor position and if it is part of a tactic then it will interpret through the completion of that tactic.

Is it actually tactic specific? I guess it probably works for any command (eg Definition foo1 |:= 1. Definition foo2 := 2.)

[Durbatuluk1701]

This PR adds a "interpret to next point" that will take the current cursor position and if it is part of a tactic then it will interpret through the completion of that tactic.

Is it actually tactic specific? I guess it probably works for any command (eg Definition foo1 |:= 1. Definition foo2 := 2.)

You are correct it isn't tactic specific. I think my wording is definitely wrong, but I think any solution that would fix #870 would probably need to be general/work for any command and not tactic specific.

[Durbatuluk1701]

I love it too, thanks!

The lang server knows the end of sentences, it should compute what next means.

Sounds good, I can start working on that.

One point of clarification, do we want a separate "interpretToNextPoint" sort of command (that would be utilized by continuous mode), or to modify the existing "interpretToPoint" functionality to interpret to the next command?

I think the primary difference would be how using "interpretToPoint" works when in manual mode.

[rtetley]

I love it too, thanks!
The lang server knows the end of sentences, it should compute what next means.

Sounds good, I can start working on that.

One point of clarification, do we want a separate "interpretToNextPoint" sort of command (that would be utilized by continuous mode), or to modify the existing "interpretToPoint" functionality to interpret to the next command?

I think the primary difference would be how using "interpretToPoint" works when in manual mode.

Yes I think we should create a interpretToNextPoint function in the server. We then create a boolean server setting that can be toggled from the front end. Depending on that setting a vscoq/interpretToPoint request calls one or the other.

[Durbatuluk1701]

Pushed some changes to make it so that the computation occurs on the server side and an option for configuring it.

I was a little confused on all the times that id_of_pos was being called and when some of those should have the next_pos switch hard-coded to false vs. when it should be propagated from above, so a keen eye reviewing some of those would be helpful.

I additionally encountered a corner case that I don't think has been addressed in the previous discussion in regard to a case with bullets like:

Lemma test : forall {A} (x y : A), x = x /\ y = y.
Proof.
  intros.
  split.
  - eauto.
  - eauto.
Qed.

Specifically for bullets, do we want -| eauto. to interpret to:

1. -| eauto. (bullets break up commands)
2. split.| \n - eauto. (bullets don't break up commands, roll back before any bullets)
3. - eauto.| (bullets don't break up commands, roll forward after the bullet)

I currently have it set up to do option 1.

[TheoWinterhalter]

Option 1 is how I use interpret to point most of the time so it would be my favoured option as well.

[rtetley]

I think this approach will make the code more readable and avoid possible regressions due to too many API changes and unnecessary boolean flags.

[Durbatuluk1701]

I think this approach will make the code more readable and avoid possible regressions due to too many API changes and unnecessary boolean flags.

Much cleaner approach indeed! Thank you for your help

[rtetley]

Yup ! Thanks a lot ! This is good for me ! @gares I'll let you take care of it as you requested the changes !

[gares]

I think we can improve further and kill that regexp.

Instead of computing the position of the next sentence on the RawDocument, we can do so on the (parsed) Document.
Here for example we do something similar, see the call to find_sentence_after.

vscoq/language-server/dm/documentManager.ml

Lines 326 to 333 in f8b2c9f

	let get_next_range st pos =
	match id_of_pos st pos with
	| None -> None
	| Some id ->
	match Document.get_sentence st.document id with
	| None -> None
	| Some { stop } ->
	match Document.find_sentence_after st.document (stop+1) with

I think the easiest would be keep just one coqtopInterpretToPoint with a boolean flag and then call Dm.DocumentManager.interpret_to_position or a new Dm.DocumentManager.interpret_to_next_position. The two functions would be almost identical (but they are 2 lines each) and the latter would call a new id_of_sentence_after_pos that should look like get_next_range (the code I link above).

WDYT @rtetley , am I missing something? I don't have the time to try this solution out, but looks simpler.

[rtetley]

The problem is that all the other functions in the interpretToPoint function rely on the position, such as mk_proof_view_event, etc.... So you at least have to propagate the new position. Your solution would be fine as long as Dm.DocumentManager.interpret_to_next_position also returns the value of next_pos, and the we use that for the rest of the functions.

[gares]

So you at least have to propagate the new position. Your solution would be fine as long as Dm.DocumentManager.interpret_to_next_position also returns the value of next_pos, and the we use that for the rest of the functions.

Right, I missed that piece. But it still looks cleaner that the current code, no?

[rtetley]

So you at least have to propagate the new position. Your solution would be fine as long as Dm.DocumentManager.interpret_to_next_position also returns the value of next_pos, and the we use that for the rest of the functions.

Right, I missed that piece. But it still looks cleaner that the current code, no?

Agreed, its definitely an improvement !

[gares]

Look better to me. @rtetley would it be possible to make the boolean argument optional in the protocol so to be backwards compatible?

[rtetley]

Look better to me. @rtetley would it be possible to make the boolean argument optional in the protocol so to be backwards compatible?

I believe it is enough to make to_next_point an option. i.e.:

Suggested change

	type t = {
	textDocument : VersionedTextDocumentIdentifier.t;
	position : Position.t;
	to_next_point : bool
	} [@@deriving yojson]
	type t = {
	textDocument : VersionedTextDocumentIdentifier.t;
	position : Position.t;
	to_next_point : bool option;
	} [@@deriving yojson]

[rtetley]

But I guess there is a larger question here, and I feel kinda silly because I am the one that suggested making this part of the protocol instead of the server options. Are we going to use both versions simultaneously ? If it makes sense to sometimes use the to_next_point: true version and false version in the same editing session we should keep it that way. Otherwise we can revert to making it a server option. What do you think @gares ?

[gares]

I see no use case of using both behaviors at the same time :-/

[rtetley]

Well I think then we should revert to making it an option in the server that gets sent through the configuration request ! Sorry @Durbatuluk1701 😅

[Durbatuluk1701]

All good, I think the iterations has made this an overall better solution for sure

[rtetley]

@gares I can't merge this since you asked for the changes !