Clément Pit-Claudel

I'd love to add that feature to fstar-mode :) And I'd be happy to look at a PR together. I think we can simplify the code a bit, too. I'd...

> F* requires us to have a module MODULENAME declaration at the start of any file we send it. Let's fix that, then. F* should be more tolerant on what...

Let me know if you need help with this :)

Hi Jean-Karim, Thanks for the suggestions! I don't think it's currently feasible (but I'm hoping to be wrong!) The problem is that we have types for identifiers, but not for...

Yep, that's a new emacs "feature": faces that want to extend to the end of the line need a `:extend` spec. Can you try adding `:extend t` to the relevant...

Hi Luke! I don't know whether the "go to this exact point" behavior is still useful, but I suspect it is: the automatic logic to figure out where a block...

Maybe we could have a setting for this. Or maybe one of the F* devs can comment?

Is fstar-vscode-assistant using LSP or the custom F* protocol?

:thinking: this is not looking good. AFAICT, the remote F* process exited after complaining about an unparseable input. Can you run the same experiment after `M-x fstar-toggle-debug`? This should open...

Thanks. It looks like F* is receiving a bad JSON message, although what fstar-mode sends seems fine. Could you patch F* to print back the JSON string before exiting? The...