fstarlang / vimfstar Goto Github PK

module Foo
open Bar
open Baz

will not correctly highlight the first open. However,

module Foo (* quux *)
open Bar
open Baz

will correctly color everything. I assume this means the module region isn't correctly ending.

I've been looking into the interactive feature of VimFStar and it appears unusable.

• It seems to have never have been written to support Windows outside of cygwin (e.g. lines of code like let s:path = system("echo $PATH") suggests this to be the case).
• I've tried using it on a Debian Jessie system. Pressing <F2> per the instructions results in the plugin never leaving the Always busy state.
• VimFStar provides no feedback regarding what's wrong nor does there seem to be any meaningful diagnostic code.

I've begun an attempt to address these issues. Before I get too deep into it, I wanted to ask:

• Does anyone currently use this feature? If nobody responds within a reasonable time period, I will assume not.
• If yes, is there any critical portion that needs to be preserved? I anticipate modifying a large amount of code in my effort to understand, fix, and inject usability into this feature; I don't want to unintentionally harm anyone's productivity in the process.

I will be making all of my changes in a fork and will produce a pull request when I believe I have something of quality.

Thanks in advance for any comments. 😸

Note: Interactive mode requires a Cygwin build of (g)Vim.

What does it mean for non-Windows platforms?

(FWIW I'm porting this plugin to python3 right now, but missing some features)

This is a valid F* module that defines bar:

module Foo
(* // *)
let bar = 1

However VimFStar doesn't think that the comment on the second line ends on line 2. It thinks that it is never closed.

Hey @SimonForest and @mlr-msft,

We've just merged an improved IDE frontend in the FStar repo. I've documented the new protocol at https://github.com/FStarLang/FStar/wiki/Editor-support-for-F* , and added notes at the end about porting. It should be relatively easy to update VimFStar: the new protocol is mostly just JSON syntax and a bunch of new opt-in features. The old --in flag is still in place, of course, so nothing should break — but it would be nice to update and upgrade F* support in Vim!

Let me know if I can help with the port.

On suboptimal OSes (e.g. Windows), this prevents "make -C src/ocaml-output" from copying the fresh fstar.exe into the bin/ directory.

On my Macbook, opening any .fst file using 'vim' gives this error.

Error detected while processing /Users/anithagollamudi/.vim/bundle/VimFStar/ftplugin/fstar.vim:
line   47:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/Users/anithagollamudi/.vim/bundle/VimFStar/ftplugin/fstar-inter.py", line 62, in fstar_init
    fst=Popen([fstarpath,'--in'],stdin=PIPE, stdout=PIPE,bufsize=1,close_fds=ON_POSIX)
  File "/usr/lib/python2.7/subprocess.py", line 710, in __init__
    errread, errwrite)
  File "/usr/lib/python2.7/subprocess.py", line 1335, in _execute_child
    raise child_exception
OSError: [Errno 8] Exec format error

The interactive mode in vim is currently broken.
I created a pull request (#9) that fixes the issue.