advance-to-point advance to the end of the current block

[LukeXuan]

This pull request modifies the behavior of fstar-subp-advance-or-retract-to-point such that it will advance to the end of the current block.

Previously, if the cursor is in the middle of a block, for example,

let foo (_: unit) = ()
             ^

Pressing C-c RET will pass let foo( to the sub-process, and reports an error. The updated function will pass the entirety of let foo ... to the process and succeed. This is helpful when I'm still trying to figure out the function body (especially if it spans multiple line), since I won't need to move my cursor (which I can use M-n) and back (which is more difficult).

I'm not a fstar power user and in all my use cases, I'm always advancing the proof checker on a block granularity. Maybe there is indeed a demand for sub-block advancement (maybe at tactic level, such as in Coq). If that's the case, I can create a separate function for this altered behavior and register a different key for it.

[cpitclaudel]

Hi Luke!

I don't know whether the "go to this exact point" behavior is still useful, but I suspect it is: the automatic logic to figure out where a block ends is not very good, and so it's good to be able to override it.

That said, I agree with you that I prefer your behavior when it works.

Doesn't C-c C-n do what you want in most cases? (Process the next block?)

[LukeXuan]

Yes, C-c C-n technically do the same thing, but I prefer C-c RET for three reasons,

• muscle memory from using C-c RET for years from coq-mode has trained me to that binding only,
• C-c RET can both retract and advance, while I would need to hit C-p for retract otherwise.
• I'm using homerow modifiers. In other words, control key is J/F for me. As you can imagine, none of J-c J-n, J-c F-n or F-c F-n is easy to work with.

[cpitclaudel]

I think the right API to call is fstar-subp--next-point-to-process

[cpitclaudel]

I think this case shouldn't change since it overrides the default block subdivision logic

[cpitclaudel]

Maybe we could have a setting for this. Or maybe one of the F* devs can comment?

[nikswamy]

Being able to configure C-c C-RET to behave like C-c C-n sounds like a good idea to me.

FWIW, finding the end of the current definition is difficult without actually using F* to parse the contents of the buffer. FYI, in fstar-vscode-assistant, when the user hits Ctrl+. the editor passes the current cursor location to the F* server, F* parses the buffer and advances to checker to up to the definition that encloses the current cursor location.

[LukeXuan]

FYI, in fstar-vscode-assistant, when the user hits Ctrl+. the editor passes the current cursor location to the F* server, F* parses the buffer and advances to checker to up to the definition that encloses the current cursor location.

It feels like the proper way to address the problem. Is it an API that emacs can also use or limited to vscode?

[cpitclaudel]

Is fstar-vscode-assistant using LSP or the custom F* protocol?