F* sent into a weird state about fstar-mode.el HOT 6 CLOSED

Hi Jonathan,

Indeed; there is such a convention; we originally discussed it on the beta thread. The documentation mentions it, but it could be more explicit:

Emacs                 Atom     Action
-------------------------------------------------------------------------------------
C-c C-n               C-S-n    Process the next block (terminated by two empty lines)

The trick is, there are two opposing constraints here:

• Make it convenient to process everything up to a point
• Auto-detect block boundaries so that it's possible to process just the next block, and so that rewinding after processing a large section does not rewind the entire section

If I map C-c C-RET to "process everything up to this point, extending to the next block boundary", then you loose fine-grained control over what gets sent (unless you use double newlines already)

OOTH, if I map C-c C-RET to "process everything up to this point exactly", then being in the middle of a definition confuses the REPL.

Finally, if I take the first approach but make a single new line the block delimiter, then definitions like

let a = 
  blah

and let b =
  bluh

can't be sent to the interpreter...

I'm not sure if we can solve this issue unless there's a clear block delimiter. Until then, I can add a setting for C-c C-RET to only send full blocks (as delimited by a double empty line).

from fstar-mode.el.

Hmm right. My bad, I should've seen this in the README. I guess I shouldn't be using C-c C-RET unless I'm really sure where my cursor is, then.

What about the fact that F* is sent in a bad state? I assume this is something you have no control over?

from fstar-mode.el.

Not sure about the bad state :) I'll check this week-end!

from fstar-mode.el.

The trick about the cursor position is that you probably just want to use C-c C-n most of the time.

from fstar-mode.el.

Can you give me more details about the weird state; maybe a file that shows this behaviour? I have trouble reproducing it.

from fstar-mode.el.

I can't reproduce, sorry. I'll re-open if I find a proper testcase.

from fstar-mode.el.