{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/678","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/678/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/678/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/678/events","html_url":"https://github.com/FStarLang/FStar/issues/678","id":176996505,"number":678,"title":"How does one use the --in mode of fstar.exe? ","user":{"login":"A-Manning","id":10554686,"avatar_url":"https://avatars.githubusercontent.com/u/10554686?v=3","gravatar_id":"","url":"https://api.github.com/users/A-Manning","html_url":"https://github.com/A-Manning","followers_url":"https://api.github.com/users/A-Manning/followers","following_url":"https://api.github.com/users/A-Manning/following{/other_user}","gists_url":"https://api.github.com/users/A-Manning/gists{/gist_id}","starred_url":"https://api.github.com/users/A-Manning/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/A-Manning/subscriptions","organizations_url":"https://api.github.com/users/A-Manning/orgs","repos_url":"https://api.github.com/users/A-Manning/repos","events_url":"https://api.github.com/users/A-Manning/events{/privacy}","received_events_url":"https://api.github.com/users/A-Manning/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/FStarLang/FStar/labels/proof-assistant","name":"proof-assistant","color":"eb6420"},{"url":"https://api.github.com/repos/FStarLang/FStar/labels/question","name":"question","color":"cc317c"},{"url":"https://api.github.com/repos/FStarLang/FStar/labels/usability","name":"usability","color":"009800"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2016-09-14T19:21:50Z","updated_at":"2016-09-15T14:25:20Z","closed_at":null,"body":"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. "},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/247343463","html_url":"https://github.com/FStarLang/FStar/issues/678#issuecomment-247343463","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/678","id":247343463,"user":{"login":"A-Manning","id":10554686,"avatar_url":"https://avatars.githubusercontent.com/u/10554686?v=3","gravatar_id":"","url":"https://api.github.com/users/A-Manning","html_url":"https://github.com/A-Manning","followers_url":"https://api.github.com/users/A-Manning/followers","following_url":"https://api.github.com/users/A-Manning/following{/other_user}","gists_url":"https://api.github.com/users/A-Manning/gists{/gist_id}","starred_url":"https://api.github.com/users/A-Manning/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/A-Manning/subscriptions","organizations_url":"https://api.github.com/users/A-Manning/orgs","repos_url":"https://api.github.com/users/A-Manning/repos","events_url":"https://api.github.com/users/A-Manning/events{/privacy}","received_events_url":"https://api.github.com/users/A-Manning/received_events","type":"User","site_admin":false},"created_at":"2016-09-15T14:25:20Z","updated_at":"2016-09-15T14:25:20Z","body":"@s-zanella At the moment, I've enabled checking an entire file in Atom. \r\n\r\n`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. \r\nSince 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. \r\n\r\nFor 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. \r\n\r\nAs 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. \r\n\r\nWhat 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. \r\n"}}
{"actor":{"display_login":"A-Manning"}}