Clément Pit-Claudel

Ah, right because it's using the server. That's a bit annoying. Then I agree, it would be good to offer to save the buffer.

Well, it wouldn't be for me (I don't use F* these days), but if you want to write the patch, that would be great!

Hi Aseem, > I recently added support for typechecking the F* typechecker source files in the emacs mode via Makefile(s) and the -in targets. This helps keep the F* command...

> Most of us have a small script in .emacs that finds such a target in the Makefile, invokes it to get the F* options, and then sets the fstar-subp-prover-args...

> But in that case, the support will be for all F* files, and not just the typechecker ones, so the code that is removed in the PR should still...

:heart_eyes: this example is so small, thanks a lot :)

Some quick notes: The CPU profile looks like this: ``` - fstar-subp-filter 21762 52% - if 21758 52% - progn 21756 52% - let 21742 52% - if 21738 52%...

Another thing: Emacs is bad at long lines. Like, really bad. So these long lines will tend to slow the display to a crawl. I suspect that's the 100% CPU...

Regarding RAM usage: are you running with fstar-debug set? With it I observe linearly growing ram as I replay the snippet over and over, which is expected (the full history...

I think this is F* side; we just jump to the position it reports. But we could work around it on our side if needed. Here's I'd go about it...