Ability to use "fstar --indent"

[jaybosamiya]

I have implemented some code that introduces the C-c <tab> keybinding that calls out to fstar --indent for the region of code that the cursor is in (i.e., a subp).

It also exposes fstar-indent-region, fstar-indent-buffer and fstar-indent-subp as interactive commands that can be executed via M-x.

I have not made this as a PR since I didn't want to mess with fstar-mode.el yet. If you believe that I should add this code into fstar-mode.el and make a PR instead, please do let me know, and I will do so.

fstar-indent.el: https://gist.github.com/jaybosamiya/e8ffadf521803a96ee4f3c30a61ec67d

[cpitclaudel]

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 start by looking at shell-command-on-region, which does something fairly similar.

[jaybosamiya]

I had originally considered shell-command-on-region but then not used it since F* requires us to have a module MODULENAME declaration at the start of any file we send it. That's why there's the whole has-module-name and related stuff in the code. During the discussion at the all-hands though, it seemed like a good idea to expose the --indent functionality via the --ide interface, in which case a lot of the code complexity for fstar-mode would go down, and we wouldn't even need the hack to add a temp module name.

If that feature is added into fstar sometime soon, then I'd be happy to write code to use that feature; alternatively, I will take another look at this code itself and make a PR soon.

Thanks :)

[cpitclaudel]

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 it accepts :)

it seemed like a good idea to expose the --indent functionality via the --ide interface

That'll be inconvenient for anyone whose not using the IDE, and it might even be inconvenient for IDE users as well (the --ide interface is synchronous, so you wouldn't be able to indent a function while another one is verifying).

I think the ideal interface on the F* side would be for --indent to read from stdin, write to stdout, and not complain when module … is missing. Once we have this, the implementation on the Emacs side will be essentially shell-command-on-region. WDYT?

[jaybosamiya]

Sounds good and makes sense :) Having essentially a shell-command-on-region would be a good idea.

I'll look into the F side for being more tolerant when I get some time (haven't looked into that side of F before, but should be interesting nevertheless :))

[cpitclaudel]

Let me know if you need help with this :)

[jaybosamiya]

I haven't had a chance to look at this yet. Sometime soon though. Thanks for pinging :)