Closed jaybosamiya closed 6 years ago
Thanks! Turns out the heuristic that allows edits in comments also allows edits around comments… and fixing it isn't easy. I'll just kill this feature — it desynchronizes F* and Emacs anyway.
Wouldn't an easy fix be to check if the edit itself changes the number of comments, and disallow the edit if it does?
Having editable comments in the busy mode is extremely useful in general because it allows us to continue documenting things, etc. while F is "thinking". I also use it from time to time to set up new assertions / assumptions inside comments while F is "thinking", so that I just need to uncomment once it is done thinking and I can ask F* to go over the code again. Going a bit too fast on the "uncomment" is what led me to discovering this bug in the first place :)
Modifying comments while F* is busy is a useful feature. I would be sad to see it gone. I can live with desynchronized state (is it just line and column numbers?) and avoid Jay's hilarious trick if it means keeping this feature.
fstar-mode generally doesn't allow modifiying code which is in the busy section. However, changes to comments are allowed (since these should be safe). However, this leads to the following interesting behaviour:
Here, I have set up a function
foo
with lots of cases in itsmatch
statement. It however is equivalent tolet foo x = x
. Thus, withassert (False)
being commented, the proof should go through. The point of using lots of cases is to slow down this proof and cause it to take enough time, for me to move over to the comment, select it, and hitM-;
, which is able to uncomment it. This makes it look like we've provenFalse
. However, this information doesn't seem to propagate to F* and is simply what it looks like to the user who specifically does this weird combo.