On macOS F* output requires interaction with Emacs to be processed

[tchajed]

I've noticed some bizarre behavior with long proofs. If I process a slow proof and then don't do anything in Emacs, the proof never finishes. As soon as I interact with Emacs (eg, moving the point around), the proof will be marked as complete.

I've also noticed that the blinking ✪ doesn't blink quite as fast if I don't interact with Emacs.

I don't yet know if this is reproducible in Linux.

[cpitclaudel]

Thanks. That's too little info for me to say much, but here are few things that would help:

• Did you try in emacs -Q?
• Does it happen on all files? Can you make a small file that reproduces the issue? How long does the proof need to be?
• Does it happen on all macOS machines?
• Are you using an OCaml F, or an F# F? Which version?
• Can you show input and output from the fstar-debug window? When does output arrive? Right after you interact with Emacs? Do all kinds of interactions work, or just keyboard? Does pressing C-g also make output arrive?

[cpitclaudel]

Ping :) Any news on this?