unrecognized option '--in'

[srenatus]

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'

[beurdouche]

Hi Stephan, The last pre-release of F* was before the interactive mode was introduced (--in) so it is expected to work only with the master branch...

[srenatus]

Hi Benjamin,

oh, I see. Thanks a lot.

I'll close this issue then.