Last chunk verified reverted when saving buffer

[s-zanella]

Sometimes when I push a new chunk of code for which verification succeeds, and saving the buffer immediately after, the state reverts to the previous checkpoint (reverting the chunk that just verified).

Sorry if this is hard to reproduce. I can't say exactly what triggers this but I hit this quite often in a session. Mostly, I want to know if I'm the only one seeing this behavior or if it is something that other users experienced.

[cpitclaudel]

Do you have something like (add-hook 'before-save-hook 'whitespace-cleanup) in your .emacs? It could be emacs removing stray end-of-line spaces before saving, which would cause fstar-mode to rewind the affected regions.

[s-zanella]

That's it! I'm using ws-butler, which should be trimming white-space doing something similar. I'm impressed with your remote-diagnostic ability!

[cpitclaudel]

:) Can end-of-line whitespace ever be significant in F*? For example, are there multiline strings? If not, we could try to work around this issue.

[s-zanella]

I think end-of-line space is never significant in F*. @kyod should know the answer.

[kyoDralliam]

F* strings are multiline by default and a new line can also be materialized by a '\' as usual. I'm not exactly sure if the default behaviour is a bug or a feature, will ask the higher-ups to see their opinion on that matter.

[cpitclaudel]

Thanks @kyoDralliam (and hi!)