fstarlang / fstar-interactive Goto Github PK

The colors used right now make it really hard to read code that was already checked (on my color theme at least, but I saw that on Cedric's one too). Any chance to let users customize the color of the various bars?

TypeError: Cannot read property 'onDidChangeCursorPosition' of undefined
  at Object.module.exports.highlightErrors (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:380:41)
  at Object.module.exports.onStdout (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:168:14)
  at emitOne (events.js:77:13)
  at Socket.emit (events.js:166:7)
  at readableAddChunk (_stream_readable.js:146:16)
  at Socket.Readable.push (_stream_readable.js:109:10)
  at Pipe.onread (net.js:517:20)

The error was thrown from the fstar-interactive package.

1. Write anything that fails checking, no matter how trivial. Checking a file that just contains the word "blah" is enough.
2. Place cursor at end of file
3. Press Ctrl+Shift+I

Atom Version: 1.3.2
System: Microsoft Windows 10 Pro Insider Preview
Thrown From: fstar-interactive package, v0.1.0

Stack Trace

Uncaught TypeError: Cannot read property 'isDestroyed' of undefined

At C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:304

TypeError: Cannot read property 'isDestroyed' of undefined
    at C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:304:15
    at C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:206:64

Commands

  4x -7:28.6.0 core:backspace (atom-text-editor.editor.is-focused)
     -7:24.4.0 core:move-left (atom-text-editor.editor.is-focused)
     -6:53.9.0 core:save (atom-text-editor.editor.is-focused)
     -6:23.8.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)
     -6:12 core:save (atom-notification.fatal.icon.icon-bug.native-key-bindings.has-detail.has-close.has-stack)
  2x -6:09.2.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)
     -0:12.3.0 core:move-down (atom-text-editor.editor.is-focused)
     -0:02.6.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)

Config

{}

Installed Packages

# User
fstar-interactive, v0.1.0
language-fstar, v0.1.0

# Dev
No dev packages

Any chance for another key shortcut Ctrl+Shift+N that advances the checking to the next top level definitions. Without this it's not so convenient to always go to the end of a large definition in order to re-check it.

On Atom 1.30 on Windows 10 x64 I got that message:

(0,0-0,0): (Warning 281) Error locations may be wrong, unrecognized string after #push:

on the erroneous program:

module Hello

let main = aksldjaskl

F* version downloaded as a binary from the official site:

C:\Users\Some>fstar --version
F* 0.9.6.0
platform=Windows_x64
compiler=OCaml 4.05.0
date=2018-05-17T15:32:12-07:00
commit=743819b90 (dirty)

How to get fstar support (syntax highlighting & interaction) when editing interfaces?

Currently I'm getting Unable to execute: undefined when typing Ctrl+Shift+I in tinyfstar-new.fst

Contrary to what one would expect, the --verify_module flag needs to be manually set in atom-fstar-build.json, to verify individual files.

Otherwise, verification is slow, and for miTLS reports way too many errors.

Moreover, if there is in addition a dangling space at the end of the JSON string, the following error is thrown:

Seems like a problem with parsing errors?

1. Load file with error and try to check it (Ctrl + Shift + I)
2. Packages > F* Interactive > Next error (Alt + Ctrl + G)
3. Uncaught TypeError: Cannot read property 'shift' of undefined

Atom Version: 0.199.0
System: linux 4.0.1-1-ARCH
Thrown From: fstar-interactive package, v0.1.0

Stack Trace

Uncaught TypeError: Cannot read property 'shift' of undefined

At /home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:291

TypeError: Cannot read property 'shift' of undefined
    at Object.module.exports.nextError (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:291:34)
    at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/usr/share/atom/resources/app.asar/src/command-registry.js:238:29)
    at CommandRegistry.handleCommandEvent (/usr/share/atom/resources/app.asar/src/command-registry.js:3:61)
    at CommandRegistry.module.exports.CommandRegistry.dispatch (/usr/share/atom/resources/app.asar/src/command-registry.js:153:19)
    at EventEmitter.<anonymous> (/usr/share/atom/resources/app.asar/src/window-event-handler.js:71:30)
    at emitOne (events.js:77:13)
    at EventEmitter.emit (events.js:166:7)

Commands

     -0:32.3.0 core:move-to-bottom (atom-text-editor.editor.is-focused)
     -0:29.3.0 core:backspace (atom-text-editor.editor.is-focused)
  5x -0:28.7.0 core:move-down (atom-text-editor.editor.is-focused)
     -0:27.6.0 core:move-left (atom-text-editor.editor.is-focused)
  5x -0:27.4.0 core:select-right (atom-text-editor.editor.is-focused)
     -0:26.2.0 core:backspace (atom-text-editor.editor.is-focused)
  2x -0:25.9.0 core:move-down (atom-text-editor.editor.is-focused)
     -0:25.3.0 core:move-to-bottom (atom-text-editor.editor.is-focused)
     -0:23.1.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)
     -0:00.3.0 fstar-interactive:next-error (div.build.tool-panel.panel-bottom.native-key-bindings)

The README says that Ctrl+Shift+G will jump to the next error, but on my machine it does something completely unrelated: it displays a "Styleguide"

Error messages report relative (with respect to previously checked part of the file) line numbers. rather than absolute path numbers from the beginning of the file.

Tried installing fstar-interactive, and I got this error as soon as I tried to use ctrl-shift-I.

fstar-interactive seems to be looking for a atom-fstar-build.json file in the folder of my fstar program, which doesn't necessarily exist.

John Kennerley reports this:

I downloaded Atom, git cloned atom-fstar and git cloned atom-interactive.
I ran apm intsall and apm link for both.
It looks like I got Atom syntax highlighting but fstar interactive in atom is giving me a exception in Atom.
Ctrl-Shift-i in Atom with a jk.fst file open yields an exception in Atom.
I tried clicking the create an issue on Atom from inside Atom but got a unicorn picture from github.
It looks like the Atom with fstar development could be a good thing, although was semi expecting a VS support for fstar.

This page is taking way too long to load.

The Atom exception
Error: ENOENT: no such file or directory, lstat 'C:\Users\John\AppData\Local\atom\app-1.0.7\atom:'
at Error (native)
at fs.lstatSync (fs.js:836:18)
at Object.fs.lstatSync (ATOM_SHELL_ASAR.js:170:16)
at Object.realpathSync (fs.js:1439:21)
at Object.fs.realpathSync (ATOM_SHELL_ASAR.js:243:29)
at C:\fstar-interactive\lib\main.js:180:27
at Function.find (C:\fstar-interactive\node_modules\lodash\dist\lodash.js:3217:15)
at FStarMain.module.exports.FStarMain.fstarArgs (C:\fstar-interactive\lib\main.js:179:33)
at FStarMain.module.exports.FStarMain.buildCommand (C:\fstar-interactive\lib\main.js:221:21)
at FStarMain.module.exports.FStarMain.startChildProcess (C:\fstar-interactive\lib\main.js:276:20)

I agree that the error messages should be better, but the fstar-interactive is really just a way to run F_. If you didn't manage to compile F_ and get an executable for it that you can use from the
command line then there is no way you can use fstar-interactive. The cryptic error might be about not finding fstar.exe in your PATH ...

Starting from Atom v1.13.0, the contents of atom-text-editor elements are no longer encapsulated within a shadow DOM boundary. This means you should stop using :host and ::shadow pseudo-selectors, and prepend all your syntax selectors with syntax--. To prevent breakage with existing style sheets, Atom will automatically upgrade the following selectors:

atom-text-editor::shadow .gutter .line-number.line-number-green => atom-text-editor.editor .gutter .line-number.line-number-green
atom-text-editor::shadow .gutter .line-number.line-number-blue => atom-text-editor.editor .gutter .line-number.line-number-blue
atom-text-editor::shadow .gutter .line-number.line-number-red => atom-text-editor.editor .gutter .line-number.line-number-red
.build .checking => .syntax--build .checking
.build h1.error => .syntax--build h1.syntax--error
.build h1.success => .syntax--build h1.success
.build h1.warning => .syntax--build h1.syntax--warning
.build ol => .syntax--build ol
.build li => .syntax--build li
.build li.error => .syntax--build li.syntax--error
Automatic translation of selectors will be removed in a few release cycles to minimize startup time. Please, make sure to upgrade the above selectors as soon as possible.

Trying to reproduce some other things, but now I'm getting new errors. Screenshot attached:

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: the new protocol is mostly just JSON syntax and a bunch of new opt-in features.

Hi there.

Trying to use fstar-interactive with one of the example files (downgrade.fst, see also here), everything seems almost-correct, until the final spawn of fstar.exe, where it passes --in, what the executable doesn't expect:

$ fstar --z3timeout 10 --in downgrade.fst
unrecognized option '--in'

I wonder if there's an incompatibility using this master branch and the latest fstar release?

Attached you find the console log. (There's another issue in there, regarding getBufferPosition, but I suppose it's less important...)

Thanks for your work, btw :)

about to parse: 
  options:--z3timeout 20;
  variables:LIB=../../lib;
  other-files:$LIB/classical.fst $LIB/ext.fst $LIB/set.fsi $LIB/set.fst $LIB/heap.fst
              $LIB/stperm.fst $LIB/seq.fsi $LIB/seq.fst $LIB/seqproperties.fst $LIB/arr.fst
              qs_seq.fst qsort_arr.fst

lib\main.js:112 >>>
  options:--z3timeout 20
lib\main.js:112 >>>
  variables:LIB=../../lib
lib\main.js:112 >>>
  other-files:$LIB/classical.fst $LIB/ext.fst $LIB/set.fsi $LIB/set.fst $LIB/heap.fst
              $LIB/stperm.fst $LIB/seq.fsi $LIB/seq.fst $LIB/seqproperties.fst $LIB/arr.fst
              qs_seq.fst qsort_arr.fst

lib\main.js:135 Parsed build config: <--z3timeout,20
 LIB,../../lib
 $LIB/classical.fst,$LIB/ext.fst,$LIB/set.fsi,$LIB/set.fst,$LIB/heap.fst,$LIB/stperm.fst,$LIB/seq.fsi,$LIB/seq.fst,$LIB/seqproperties.fst,$LIB/arr.fst,qs_seq.fst,qsort_arr.fst>
lib\main.js:137 replacing $LIB with ../../lib
lib\main.js:140 After replacement: <../../lib/classical.fst,../../lib/ext.fst,../../lib/set.fsi,../../lib/set.fst,../../lib/heap.fst,../../lib/stperm.fst,../../lib/seq.fsi,../../lib/seq.fst,../../lib/seqproperties.fst,../../lib/arr.fst,qs_seq.fst,qsort_arr.fst>
lib\main.js:213 Build command: --in,--z3timeout,20,../../lib/classical.fst,../../lib/ext.fst,../../lib/set.fsi,../../lib/set.fst,../../lib/heap.fst,../../lib/stperm.fst,../../lib/seq.fsi,../../lib/seq.fst,../../lib/seqproperties.fst,../../lib/arr.fst,qs_seq.fst,qsort_arr.fst
 cwd = C:\msys64\home\renatus\fstar\FStar\examples\algorithms
lib\main.js:270 Calling process with args: <--in,--z3timeout,20,../../lib/classical.fst,../../lib/ext.fst,../../lib/set.fsi,../../lib/set.fst,../../lib/heap.fst,../../lib/stperm.fst,../../lib/seq.fsi,../../lib/seq.fst,../../lib/seqproperties.fst,../../lib/arr.fst,qs_seq.fst,qsort_arr.fst>
C:\Users\renatus\AppData\Local\atom\app-0.209.0\resources\app.asar\src\text-editor.js:1318 Uncaught TypeError: Cannot read property 'getBufferPosition' of undefined
lib\main.js:240 unrecognized option '--in'