search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

feature request: go to location when "F*: subprocess exited". #57

Closed fournet closed 6 years ago

fournet commented 7 years ago

I often make syntax errors. I get F*: subprocess exited on the command line, and go to the Messages buffer to know where to look at:

[F* raw output] Interactive mode; ignoring --verify_module{"kind":"protocol-info","version":1,"features":["autocomplete","describe-protocol","exit","lookup","lookup/documentation","pop","push"]}
[F* error] C:/cygwin64/home/fournet/everest/mitls-fstar/src/tls/Handshake.fst(310,18-310,18): (Error) Syntax error: Parsing.Parse_error
[F* error] 1 error was reported (see above)
F*: subprocess exited.
Mark set [2 times]

Displaying the detailed error within my fstar buffer would be very convenient.

cpitclaudel commented 7 years ago

Yeah, it's a pain. But it would be much better if F simply didn't die (and instead reported a regular error). See https://github.com/FStarLang/FStar/issues/912 for the F side.