FStar fails to check a file due to single syntax error, and we jump to line 0

[hacklex]

Can we somehow make fstar-mode in emacs break the input file into parts according to top-level definitions, and submit as many as it could one by one so that I can at least have an idea at which top-level definition did something happen?

This is especially painful since sometimes you're in the middle of writing something, then you swtich context and write an auxiliary lemma above it, sometimes another one above, and F* process is kept alive, but at some point it just freezes. Then you have to terminate it (C-c C-x, or whatever your shortcut is) -- and when you restart it it just says "parser error" and the cursor is placed at (0,0).

How can I quickly locate at least the last good top level definition, without manually bisecting the file? Like, manually bisecting a source file to find a syntax error sounds a bit strange in 2022?

Therefore I'm asking whether we can somehow change emacs's fstar-mode (I presume changing the fstar parsing mechanism is way harder and nobody will want to do that) so that it would send the file part by part... is this possible?