Add pos argument to tryStep and return range of proof via proofContext

[DikieDick]

• Bumps version to 0.11.1 (which is odd, so prerelease?)
• Adds the option of trying a proof step at a given position, by updating the API and executeCommandBase.
• proofContext now returns the range of the proof script (between Proof. and Qed., but works for scripts without Proof. as well, see the regex)

[sonarqubecloud]

Quality Gate failed

Failed conditions
0.0% Coverage on New Code (required ≥ 80%)

See analysis details on SonarQube Cloud

[pimotte]

I think the code looks fine, but I do have some questions:

• Just to check, this PR targets main intentionally?
• Was there a way I could easily test these API methods interactively?
• Does it make sense to unit test the commandExecutor?
• Do the proofContext changes have an implication for the Lean functionality when backmerging this into mapping?

[DikieDick]

Just to check, this PR targets main intentionally?

Yes, as River currently works best (maybe even 'only') on main.

Was there a way I could easily test these API methods interactively?

Apart from using River's translateProof with a faulty proof and cursor not at the start of the input area, no.

The main problem this solves is that River would otherwise only be able to start a petanque context at the cursor position, instead of a blank input area.

Does it make sense to unit test the commandExecutor?

Yes, but we can't fully test it without having a valid LSP in the background.

Do the proofContext changes have an implication for the Lean functionality when backmerging this into mapping?

To my knowledge all this API stuff is only ever used for River, which relies on Rocq

[pimotte]

I think it does make sense to unit test the executor with a mocked client. While it's not much code, I think it's good to err on the side of testing a bit too much, and it also documents the assumptions we make on the LSP output for purposes of the executor. Especially if it's easier to setup, a test with the real client but mocked LSP messages would also be a good option.