Feature request: interactive mode shouldn't send output until it receives a query

[cpitclaudel]

This is essentially the F* side of FStarLang/fstar-mode.el#21 . When booting, F* does a bunch of things that can produce errors. These errors are reported immediately, without an end-of-message marker or a way to know where they came from, and fstar-mode consequently doesn't report them.

The fix is pretty simple: delay most initialization until an #init call or something similar has been received.

This way we could get rid of the https://github.com/FStarLang/FStar/wiki/Early-stumbling-blocks,-FAQ#fstar-mode-gives-error-message-f-subprocess-exited-what-shall-i-do and README entries about it :)

[nikswamy]

Hi @cpitclaudel . In my nik_912 branch, I implemented something to address this issue.

Basically, when launching fstar --ide a.fst, we now just print the hello message back and then wait for the next message.

When the next message arrives (usually a push) we type-check the dependences of the current buffer etc. If there are any errors in the dependences, then we print those errors back and then exit with error code 1.

However, this doesn't seem to have much impact from what is observed from the side of fstar-mode.el.

Could fstar-mode.el be revised to at least report the error message that F* prints back before exiting?

Not exiting on the fstar side is quite hard ... since without a proper dependence graph, it's not at all clear how to proceed.

Thanks!

[cpitclaudel]

In my nik_912 branch, I implemented something to address this issue.

Yay, thanks!

However, this doesn't seem to have much impact from what is observed from the side of fstar-mode.el.

Hmm. How are you printing the errors and exiting? Can you show me what a transcript looks like (it should be easy with fstar-toggle-debug)?

Could fstar-mode.el be revised to at least report the error message that F* prints back before exiting?

Doesn't it do that (in the Messages buffer)?

When the next message arrives (usually a push) we type-check the dependences of the current buffer etc. If there are any errors in the dependences, then we print those errors back and then exit with error code 1.

What happens if instead of exiting you just revert to the state right before the push?

[nikswamy]

I have in a.fst:

module A
let f = B.x

and in b.fst

module B
let f (x:int) = x + "hello"

I'm launching fstar-mode.el on a.fst using nik_912.

Here's the output from the debug window:

;;; Started F* interactive: ("c:/Users/nswamy/workspace/FStar/bin/fstar.exe" "c:/Users/nswamy/workspace/test/a.fst" "--ide")
;;; Processing queue
>>> {"query-id":"1","query":"push","args":{"kind":"full","code":"module A\nlet f = B.x\n","line":1,"column":0}}
{"kind":"protocol-info","version":1,"features":["autocomplete","compute","describe-protocol","describe-repl","exit","lookup","lookup/documentation","lookup/definition","pop","peek","push","search"]}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 1) (features "autocomplete" "compute" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/documentation" "lookup/definition" "pop" "peek" "push" "search")))
{"kind":"message","level":"error","contents":".\\b.fst(2,26-2,27): (Error) Expected expression of type \"Prims.int\"; got expression \"\"hello\"\" of type \"Prims.string\"\n"}
{"kind":"message","level":"error","contents":"1 error was reported (see above)\n"}
;;; Complete message received: (status: nil; message: ((kind . "message") (level . "error") (contents . ".\\b.fst(2,26-2,27): (Error) Expected expression of type \"Prims.int\"; got expression \"\"hello\"\" of type \"Prims.string\"
;;; ")))
;;; Complete message received: (status: nil; message: ((kind . "message") (level . "error") (contents . "1 error was reported (see above)
;;; ")))
;;; Signal received: [exited abnormally with code 1
;;; ] [exit]

Here's what's in the Messages buffer.

 [F* error] .\b.fst(2,26-2,27): (Error) Expected expression of type "Prims.int"; got expression ""hello"" of type "Prims.string"
[F* error] 1 error was reported (see above)
F*: subprocess exited.

This seems ok enough ... I'm not sure what the desired behavior here should be.

I, for one, find it confusing when the most prominent error message just says "F* subprocess exited".

It would be cool if there were some way to instead (or in addition) show the error message related to the failure in the b.fst in the ribbon at the bottom.

What do you think?

About this:

What happens if instead of exiting you just revert to the state right before the push?

In this setting, it would mean trying to proceed without any type checking / desugaring environment at all. Or, at best, with some more work, an environment populated with only some of the dependences. Neither of which seem like a particularly useful state to be in. Perhaps I'm misunderstanding ...

[cpitclaudel]

It would be cool if there were some way to instead (or in addition) show the error message related to the failure in the b.fst in the ribbon at the bottom.

I can try to work something out. These two messages come from different parts of the code, so it's hard to teach them about each other.

What happens if instead of exiting you just revert to the state right before the push?

In this setting, it would mean trying to proceed without any type checking / desugaring environment at all. Or, at best, with some more work, an environment populated with only some of the dependences. Neither of which seem like a particularly useful state to be in. Perhaps I'm misunderstanding ...

Or perhaps I am. Here's the flow I'm suggesting:

• User open a syntactically invalid file pointing to a syntactically invalid dependency.
• fstar-mode launches a copy of F*. F* sends capabilities message. F* is not in state "A"
• User tries to process the first chunk of the buffer. fstar-mode sends a push message. F* tries to do a dependency check but fails. F* responds to the push with information on the syntax error, and reverts to state "A".
• User fixes error, and tries to process the first chunk of the buffer again. fstar-mode sends a push message. F* tries to do a dependency check but fails again. F* responds to the push with information on the error, and reverts to state "A" again.
• User fixes the error in the dependency, and tries to push one last time. Things work fine this time.

Does this make sense?

[s-zanella]

It makes sense to me. That would save a lot of time trying to see where are the errors in dependencies by looking at the *Messages* buffer.

[cpitclaudel]

I have a draft implementation for the proposal above. There are some issues:

• Inconsistencies between the saved file and the current version of it are even more confusing: you get an error message that matches something in the on-disk version of the file, but not something in the buffer. I plan to fix this by having fstar-mode send the whole file with the first push, instead of sending the name of a possibly out-of-sync file for F* to read from.

• It's not easy to report errors in other files.

• Dealing with push, pops, and marks is tricky. I plan to revise that code with @protz

[cpitclaudel]

I have refreshed the code mentioned above, and made progress with the implementation. I now have…

• …added a way for IDEs to pass the contents of the current buffer to us. This way, there are no more inconsistencies between the buffer and the underlying file.
• …helped implement support for secondary error locations, which allow us to link to another file.
• …gotten rid of marks
• …refactored/simplified the IDE mode's stack management

Here's how my code works (in cpitclaudel_912). When we launch F*, we create a small, partial REPL state and we do only minimal initialization. Then, when we receive our first push, we process dependencies and report errors if any instead of those of the pushed chunk (which we go on to process if dependency checking was successful).

Now I need help. tc_deps and update_deps are broken in my branch: when they fail, they don't revert the modifications (Z3 pushes, essentially). This was OK when these failures caused us to exit — but it's not OK anymore. Instead, these two functions need to learn to revert to a clean state after any failed dependency check, either by popping all dependencies, or by popping only the failed one and saving their current (partial) state until they are called again.

The first solution sounds much simpler; I'd favor taking that route, since we expect dependency re-loading to be fast once we introduce on-the-fly compilation of modules. But I can easily adjust to either solution.

@aseemr, could you help me? I'm excited to be this close to a resolution for this long-standing bug :)

[cpitclaudel]

As a side note / starting point, here's a draft / what I guess tc_deps could look like if we forget about update_deps:

let rec push_then_do_or_revert_all env stack fn =
  let revert env stack =
    Util.print1 "Reverting %s entries" (string_of_int (List.length stack));
    let rec aux env stack =
      match stack with
      | [] -> env
      | env' :: stack' -> pop env' "typecheck_modul"; aux env' stack' in
    aux env stack in

  let stack = env :: stack in
  let env' = push env "tc prims, deps, or interface" in

  match with_captured_errors env' fn with
  | None -> Inr (revert env' stack)
  | Some res -> Inl (stack, res)

let tc_deps (env: env_t) (stack: deps_stack_t) (remaining: list<string>) =
  let rec aux (env: env_t) (stack: deps_stack_t)
              (ts: m_timestamps) (remaining: list<string>) =
    match remaining with
    | [] -> Inl (stack, env, ts)
    | _ ->
      let stack = env :: stack in

      let push_kind = if Options.lax () then LaxCheck else FullCheck in
      Options.restore_cmd_line_options false |> ignore;

      match push_then_do_or_revert_all env stack
              (fun () -> Some <| tc_one_file remaining (set_check_kind env push_kind)) with
      | Inr env -> Inr env
      | Inl (stack, ((intf, impl), env, remaining)) ->
        let intf_t = intf |> Util.map_option get_file_last_modification_time in
        let impl_t = get_file_last_modification_time impl in
        aux env stack ((intf, impl, intf_t, impl_t) :: ts) remaining in

  aux env stack [] remaining

[cpitclaudel]

I have a full draft in cpitclaudel_912_wip