FStarLang / VimFStar

A Vim mode for FStar
Vim License
24 stars 12 forks source link

Interactive Feature is Unusable #12

Closed mlr-msft closed 8 years ago

mlr-msft commented 8 years ago

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

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

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. :smile_cat:

catalin-hritcu commented 8 years ago

@SimonForest originally implemented this, but I don't think is still using it (or F*). @ngrimm: are you using it?

ngrimm commented 8 years ago

I'm currently not using the feature but I was using it before and plan to use it again. Of course I'm looking forward to possible improvements, so feel free to make any modifications.

mlr-msft commented 8 years ago

It took a while but I've learned that the interactive mode currently requires Cygwin to function. I use a native build of Vim. I'll document this in the README and close out the issue.