search

FStarLang / fstar-mode.el

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

Starting interactive proving with syntax errors #52

Closed jldodds closed 7 years ago

jldodds commented 7 years ago

If I'm working on file A which depends on file B and I make a change in B I then

  1. kill the subprocess in file A in order to reload file B
  2. get a message F*: subprocess exited. until I fix any outstanding syntax errors and save them

Is step 1 the appropriate way to deal with this situation?

As a feature request, once I have started stepping into a file, syntax errors/what is saved is no longer a problem, it would be great if it were the same initially.

cpitclaudel commented 7 years ago

I think I know what you mean, but a small example would help. IIUC, that's an F* issue (it's trying to determine dependencies)

cpitclaudel commented 7 years ago

I updated fstar-mode to display the error message more clearly, and the rest of the feature request is tracked at https://github.com/FStarLang/FStar/issues/912 .

cpitclaudel commented 7 years ago

Note also that at you can now press C-c C-r to reload the current file's dependencies without restarting F*.