How does one use the --in mode of fstar.exe?

[A-Manning]

If I want to write code in the command line, how do I invoke verification? I can enter as much code as I like, but I'm not sure how to make F* actually verify it.

[s-zanella]

The --in flag is intended to be used from within an editor mode, like the one provided by https://github.com/FStarLang/fstar-mode.el. It doesn't provide you with a typical REPL, if that's what you were expecting.

It's based on a text-based protocol that mixes data and control. See #519 for an example of how the interaction looks like. It's not something you would like to do without the assistance of an editor.

[A-Manning]

That's exactly why I need it - I'm trying to add F* support to an editor.

[s-zanella]

That's great! I'm curious about which editor you have in mind. Please keep us updated.

[sishtiaq]

If you do Visual Studio Code, I'll be up for helping!

[A-Manning]

@sishtiaq @s-zanella I may add VS code at some point. For now, I've made it work in Atom, through atom-script (fstar-interactive is not working, or maintained). Pull request is here. https://github.com/rgbkrk/atom-script/pull/1078

From what I've seen, the fstar-mode.el makes extensive use of the --in mode. I've used the --fsi mode, as I couldn't figure out --in. I'm sure there's some design decision for this and I'll eventually run into some problems, but for now this is working for me.

[s-zanella]

I'm not sure I understand your use of --fsi, or what you intend to achieve using atom-script.

The key feature of the F* Emacs mode (and the unmaintained Atom mode) is interaction, in the sense that one could typecheck a file progressively, one chunk at a time, roll back to a previous point in a file, use pragmas to tweak proofs and get more feedback (i.e. #set-options). Of course, syntax highlighting, indentation and Unicode pretty printing are nice features to have too.

[A-Manning]

@s-zanella At the moment, I've enabled checking an entire file in Atom.

atom-script supports running only a selection of a file, which I intend to eventually deploy in order to achieve the same level of interaction present in fstar-mode. I don't think I've ever used fstar-mode to do anything besides checking an entire file, so whilst I'm aware that supporting selection-based checking is essential to exposing all of the features of F, I thought the first step is getting a run command for an entire file. Since that's the entire functionality of the online tutorial, at the very least we can once again consider atom to be a working IDE for F, although still a little behind emacs.

For now, one can run F* code from inside atom editor again. F* is now supported by atom-script, so many users of atom will already be able to do this.

As for my use of --fsi, I chose it because it worked for checking an entire file. If that's not the best way to do things, it can always be changed. I eventually want to use --in and do this the proper way, which was the reason I created this issue.

What do you mean by 'Unicode pretty printing'? If you're referring to things like mathematical symbols in fstar-mode, I intend to add that to language-fstar as soon as possible, as I'm rather fond of it in emacs.

[s-zanella]

I've just tried out atom-script, but I couldn't make it to work with a .fst file. I can't see F* (or F# for that matter) in the list of languages (I'm using the dev version, which includes your PR).

I might be wrong, but I think the use case for atom-script is quite different than the one for interactive proof assistants---it rarely makes sense to run just a selection of an F* file, because most likely it depends on what appears before. Still, as a basic mode that allows you to type check an entire file is useful.

I wonder why you needed the --fsi flag. Doesn't it work without it?

What do you mean by 'Unicode pretty printing'? If you're referring to things like mathematical symbols in fstar-mode, I intend to add that to language-fstar as soon as possible, as I'm rather fond of it in emacs.

Yes, I meant showing mathematical symbols as unicode.

[A-Manning]

That's strange, it's on the list of languages in the release version: https://atom.io/packages/script. I did a fresh install on my work PC today as a test and it works fine.

Is fstar.exe in your PATH?

The current way to run a script is Packages->Script->Run Script or CTRL-Shift-B.

The --fsi flag was used because languages like F# use their interactive mode in script. I don't notice any difference, but I assumed that there may be some deeper reason.

Unicode Pretty Printing is not easy in atom, but as a short-term replacement one can use a font that supports ligatures such as Fira-Code

[s-zanella]

I had to use Atom developer mode to get your PR to atom-script, because at that time the latest stable release (3.9.0) didn't include your changes to support F*. I now see that 3.10.0 was released, which does include your changes.

With the latest release, I still can't execute .fst files. Using Packages->Script->Run Script yields

You must select a language in the lower right, or save the file with an appropriate extension.

F* isn't in the list of languages, andfstar.exe is in the path that I get with process.env['PATH'] from Atom's console.

You shouldn't use --fsi. That specific flag is used to tell F* that you're checking an interface file (i.e. .fsti) interactively (meaning using the inline protocol that the Emacs mode uses, #push, etc.). I see how you this can be confused with the REPL for F# (F# interactive, aka fsi).

[A-Manning]

@s-zanella I've been unable to replicate this behaviour. It seems that Atom is unable to infer that you're using F* - do you have 'atom-fstar' installed? If not, atom-script will not recognise that you are using F* , and this would also explain why F* is not in your list of languages.

As for --fsi, I can absolutely remove it. I had planned on eventually using --fsi and --in in the same way as the Emacs mode, but playing around with the --in mode is rather confusing, and I can't seem to figure out what all of the done done-nok done-ok end etc actually do.

I've added some basic support for pretty-printing, through a fork of the 'conceal' package. https://github.com/A-Manning/FStar-Ligatures The package is experimental at the moment and may have several bugs.

Both FStar-Ligatures and atom-script depend on atom-fstar. I recommend using my fork of atom-fstar, as there is slightly better grammar support, and FStar-Ligatures cannot pretty-print symbols that are not defined in a language's grammar - for example, my atom-fstar has 'int' as a keyword, but the master atom-fstar does not. My atom-fstar is at https://github.com/A-Manning/atom-fstar.

Update: I've created a pull request to remove --fsi from atom-script. Update2: atom-script no longer uses --fsi. The changes will be included in the next release.

[cpitclaudel]

As for --fsi, I can absolutely remove it. I had planned on eventually using --fsi and --in in the same way as the Emacs mode, but playing around with the --in mode is rather confusing, and I can't seem to figure out what all of the done done-nok done-ok end etc actually do.

Hey @A-Manning. Not sure if you're still motivated about this, but if you are there's a new JSON based protocol now (--ide), which unlike --in is fully documented: https://github.com/FStarLang/FStar/wiki/Editor-support-for-F%2A#adding-support-for-new-ides :) And of course I'd be happy to help with understanding how the protocol works. But the error messages should be pretty friendly:

$ ../bin/fstar.exe --in ~/.emacs.d/lisp/fstar.el/test.fst 
{"kind":"protocol-info","version":1,"features":["autocomplete","compute","describe-protocol","exit","lookup","lookup/documentation","lookup/definition","pop","peek","push","search"]}
asdasd
{"kind":"response","query-id":"?","status":"protocol-violation","response":"JSON decoding failed: expected dictionary, got null"}
{"query": "blah"}
{"kind":"response","query-id":"?","status":"protocol-violation","response":"Missing key [query-id] in query."}
{"query": "blah", "query-id": 0}
{"kind":"response","query-id":"?","status":"protocol-violation","response":"JSON decoding failed: expected string, got int (0)"}
{"query": "blah", "query-id": "a"}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"Missing key [args] in query."}
{"query": "blah", "query-id": "a", "args": []}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"JSON decoding failed: expected dictionary, got list (...)"}
{"query": "blah", "query-id": "a", "args": {}}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"Unknown query \u0027blah\u0027"}
{"query": "push", "query-id": "a", "args": {}}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"Missing key [kind] in [args]."}
{"query": "push", "query-id": "a", "args": {"kind": "lax"}}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"Missing key [code] in [args]."}
{"query": "push", "query-id": "a", "args": {"kind": "lax", "code":"module Test\n"}}
{"kind":"response","query-id":"a","status":"protocol-violation","response":"Missing key [line] in [args]."}
{"query": "push", "query-id": "a", "args": {"kind": "lax", "code":"module Test\n", "line": 0, "column": 1}}
{"kind":"response","query-id":"a","status":"success","response":[]}

[A-Manning]

I'm aware of the --ide flag - I do plan on adding support to atom when I get the chance, although that probably won't be soon Thanks for the update though!

[cpitclaudel]

That would be awesome :crossed_fingers: :) Let me know if you run into issues with --ide.

[cpitclaudel]

Closing this :) We now have complete docs of the IDE protocol.