JSON decoding warnings

[nikswamy]

I sporadically get these warnings:

Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["JSON decoding failed: expected string, got null"])
Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["JSON decoding failed: expected string, got null"])
Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["JSON decoding failed: expected string, got null"])
Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["JSON decoding failed: expected string, got null"])

GNU Emacs 25.1.1 (x86_64-w64-mingw32) of 2016-11-15

and F* master (but I've had this for a long time now)

[nikswamy]

for the moment, i'd be happy to just have a way to suppress these warnings

[nikswamy]

it seems like disabling company-mode for fstar-mode.el at least made these warnings go away for now.

[cpitclaudel]

Hm, how annoying. I don't want to silence the warnings permanently, but I'd be happy to help you disable them temporarily while in deadline mode. Add this to your .emacs:

(require 'fstar-mode)

(defun fstar-subp-json--parse-status (status response)
  "Convert STATUS to a symbol indicating success.
RESPONSE is used in warning messages printed upon failure."
  (pcase status
    ((or "success" "failure") (intern status))
    (_ (message "Unknown status %S from F* subprocess \
\(response was [%S])" status response)
       `failure)))

[cpitclaudel]

Do you get a lot of these warnings? I'd really really like to reproduce them. Can you enable fstar-mode debugging and try to get a repro?

[nikswamy]

I created FStar/examples/demo/low-star/Test.fst with this content:

module Test
open Demo.Deps

let test l (src dest:lbuffer l uint8)
  : ST _ _ _ = ()

And then interacted like this until I got a single warning:

;;; Started F* interactive: ("d:/workspace/everest/FStar/bin/fstar.exe" "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" "--ide" "--smt" "d:/workspace/everest/z3-4.5.1.1f29cebd4df6-x64-win/bin/z3.exe" "--cache_checked_modules" "--use_hints" "--use_hint_hashes" "--use_two_phase_tc" "true" "--use_extracted_interfaces" "--use_two_phase_tc" "true" "--max_fuel" "0" "--max_ifuel" "0")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add"]}
{"kind":"message","level":"warning","contents":"Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test.fst.hints; ran without hints\n"}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add")))
;;; Complete message received: (status: nil; message: ((kind . "message") (level . "warning") (contents . "Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test.fst.hints; ran without hints
;;; ")))
;;; [202.81ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module Test\nopen Demo.Deps\n\nlet test l (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n"}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"module Test\nopen Demo.Deps\n","line":1,"column":0}}
{"kind":"response","query-id":"1","status":"success","response":null}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "1") (status . "success") (response . :json-null)))
{"kind":"response","query-id":"2","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "2") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"3","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":0}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 0)))] are late
{"kind":"response","query-id":"3","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "3") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"4","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":3}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 3)))] are late
{"kind":"response","query-id":"4","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "4") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"5","query":"lookup","args":{"context":"code","symbol":"test","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":8}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "test") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 8)))] are late
{"kind":"response","query-id":"5","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "5") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"6","query":"lookup","args":{"context":"code","symbol":"l","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":10}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "l") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 10)))] are late
{"kind":"response","query-id":"6","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "6") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"7","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":11}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 11)))] are late
{"kind":"response","query-id":"7","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "7") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"8","query":"peek","args":{"kind":"lax","code":"\nlet test l  (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"8","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "8") (status . "success") (response)))
;;; Highlighting Flycheck issues: nil
;;; Queue is empty (1 overlays)
>>> {"query-id":"9","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":12}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 12)))] are late
{"kind":"response","query-id":"9","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "9") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"10","query":"lookup","args":{"context":"code","symbol":"c","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":13}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "c") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 13)))] are late
{"kind":"response","query-id":"10","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "10") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"11","query":"lookup","args":{"context":"code","symbol":"cu","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":14}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "cu") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 14)))] are late
{"kind":"response","query-id":"11","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "11") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"12","query":"autocomplete","args":{"partial-symbol":"cur","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "cur") ("context" . "code"))] are late
{"kind":"response","query-id":"12","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "12") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"13","query":"lookup","args":{"context":"code","symbol":"cur","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":15}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "cur") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 15)))] are late
{"kind":"response","query-id":"13","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "13") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"14","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":16}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 16)))] are late
{"kind":"response","query-id":"14","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "14") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"15","query":"lookup","args":{"context":"code","symbol":"u","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "u") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 17)))] are late
{"kind":"response","query-id":"15","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "15") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"16","query":"autocomplete","args":{"partial-symbol":"uin","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uin") ("context" . "code"))] are late
{"kind":"response","query-id":"16","status":"success","response":[[3,"Demo.Deps","uint32"],[3,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "16") (status . "success") (response (3 "Demo.Deps" "uint32") (3 "Demo.Deps" "uint8"))))
>>> {"query-id":"17","query":"lookup","args":{"symbol":"Demo.Deps.uint32","context":"code","requested-info":["type","documentation"]}}
{"kind":"response","query-id":"17","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "17") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"18","query":"autocomplete","args":{"partial-symbol":"uint","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint") ("context" . "code"))] are late
{"kind":"response","query-id":"18","status":"success","response":[[4,"Demo.Deps","uint32"],[4,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "18") (status . "success") (response (4 "Demo.Deps" "uint32") (4 "Demo.Deps" "uint8"))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"19","query":"lookup","args":{"symbol":null,"context":null,"requested-info":["type","documentation"]}}
{"kind":"response","query-id":"19","status":"protocol-violation","response":"JSON decoding failed: expected string, got null"}
;;; Complete message received: (status: "protocol-violation"; message: ((kind . "response") (query-id . "19") (status . "protocol-violation") (response . "JSON decoding failed: expected string, got null")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"20","query":"autocomplete","args":{"partial-symbol":"uint3","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint3") ("context" . "code"))] are late
{"kind":"response","query-id":"20","status":"success","response":[[5,"Demo.Deps","uint32"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "20") (status . "success") (response (5 "Demo.Deps" "uint32"))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"21","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint3 (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"21","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,32],"end":[4,32]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "21") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 32) (end 4 32)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 32 32]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"22","query":"lookup","args":{"context":"code","symbol":"uint3","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":21}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint3") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 21)))] are late
{"kind":"response","query-id":"22","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "22") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"23","query":"lookup","args":{"context":"code","symbol":"uint32","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":22}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint32") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 22)))] are late
{"kind":"response","query-id":"23","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "23") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"24","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32 (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"24","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,33],"end":[4,33]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "24") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 33) (end 4 33)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 33 33]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"25","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{ (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"25","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,34],"end":[4,34]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "25") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 34) (end 4 34)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 34 34]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"26","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":23}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 23)))] are late
{"kind":"response","query-id":"26","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "26") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"27","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":24}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 24)))] are late
{"kind":"response","query-id":"27","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "27") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"28","query":"peek","args":{"kind":"lax","code":"\nlet test l (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"28","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "28") (status . "success") (response)))
;;; Highlighting Flycheck issues: nil
;;; Queue is empty (1 overlays)
>>> {"query-id":"29","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":37}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 37)))] are late
{"kind":"response","query-id":"29","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "29") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"30","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":5,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 5) ("column" . 17)))] are late
{"kind":"response","query-id":"30","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "30") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"31","query":"peek","args":{"kind":"lax","code":"\nlet test l (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"31","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "31") (status . "success") (response)))
;;; Highlighting Flycheck issues: nil
;;; Queue is empty (1 overlays)

[cpitclaudel]

Excellent, thanks. I'll look at this.

[nikswamy]

thank you!

[cpitclaudel]

One more question: are you positive turning company off solves it? This will help me focus on one of the likely sources.

[cpitclaudel]

Can you add this to your .emacs (without the snippet I gave above)?

(require 'fstar-mode)

(defun fstar-subp-company--async-meta (candidate callback)
  "Find type of CANDIDATE and pass it to CALLBACK."
  (cl-assert candidate)
  (fstar-subp-company--async-lookup candidate '(type documentation) ;; Needs docs for C-h hint
    (apply-partially #'fstar-subp-company--meta-continuation callback)))

and run M-x toggle-debug-on-error. After a small while, this should yield an assertion error with a trace. Hopefully this will have more info.

[nikswamy]

I turned company-mode off, in fstar-enabled-modules and did apply and save. This didn't seem to make the warning go away. But, then I restarted emacs (and checked that company-mode was marked as disabled) and the error did indeed go away.

[cpitclaudel]

OK, thanks. One more thing to add:

(defun fstar-subp-company-backend (command &optional arg &rest _rest)
  "Company backend for F*.
Candidates are provided by the F* subprocess.
COMMAND, ARG, REST: see `company-backends'."
  (interactive '(interactive))
  (fstar-log 'info "fstar-subp-company-backend: %S %S" command arg)
  (when (fstar--has-feature 'autocomplete)
    (pcase command
      (`interactive
       (company-begin-backend #'fstar-subp-company-backend))
      (`prefix
       (fstar-subp-company--prefix))
      (`candidates
       (fstar-subp-company-candidates arg fstar-subp-company--completion-context))
      (`meta
       `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
      (`doc-buffer
       `(:async . ,(apply-partially #'fstar-subp-company--async-doc-buffer arg)))
      (`quickhelp-string
       `(:async . ,(apply-partially #'fstar-subp-company--async-quickhelp arg)))
      (`location
       `(:async . ,(apply-partially #'fstar-subp-company--async-location arg)))
      (`sorted t)
      (`no-cache t)
      (`duplicates nil)
      (`match (get-text-property 0 'fstar--match-end arg))
      (`annotation (get-text-property 0 'fstar--annot arg))
      (`pre-render arg) ;; Preserve fontification of candidates
      (`post-completion (fstar-subp-company--post-completion arg)))))

(this is the same code as usually run, but with more debugging info). My working hypothesis is that company passes us a null value, but I'd like to confirm that...

[nikswamy]

Does this help?

;;; fstar-subp-company-backend: init nil
;;; 
;;; Started F* interactive: ("d:/workspace/everest/FStar/bin/fstar.exe" "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" "--ide" "--smt" "d:/workspace/everest/z3-4.5.1.1f29cebd4df6-x64-win/bin/z3.exe" "--cache_checked_modules" "--use_hints" "--use_hint_hashes" "--use_two_phase_tc" "true" "--use_extracted_interfaces" "--use_two_phase_tc" "true" "--max_fuel" "0" "--max_ifuel" "0")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add"]}
{"kind":"message","level":"warning","contents":"Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test.fst.hints; ran without hints\n"}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add")))
;;; Complete message received: (status: nil; message: ((kind . "message") (level . "warning") (contents . "Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test.fst.hints; ran without hints
;;; ")))
;;; [256.97ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module Test\nopen Demo.Deps\n\nlet test l (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n"}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"module Test\nopen Demo.Deps\n","line":1,"column":0}}
{"kind":"response","query-id":"1","status":"success","response":null}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "1") (status . "success") (response . :json-null)))
{"kind":"response","query-id":"2","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "2") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"3","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":0}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 0)))] are late
{"kind":"response","query-id":"3","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "3") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"4","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":3}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 3)))] are late
{"kind":"response","query-id":"4","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "4") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"5","query":"lookup","args":{"context":"code","symbol":"test","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":8}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "test") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 8)))] are late
{"kind":"response","query-id":"5","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "5") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"6","query":"lookup","args":{"context":"code","symbol":"l","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":10}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "l") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 10)))] are late
{"kind":"response","query-id":"6","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "6") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
>>> {"query-id":"7","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":11}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 11)))] are late
{"kind":"response","query-id":"7","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "7") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
>>> {"query-id":"8","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":12}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 12)))] are late
{"kind":"response","query-id":"8","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "8") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"9","query":"peek","args":{"kind":"lax","code":"\nlet test l ( (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"9","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,22],"end":[4,22]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "9") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 22) (end 4 22)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 22 22]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
>>> {"query-id":"10","query":"lookup","args":{"context":"code","symbol":"c","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":13}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "c") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 13)))] are late
;;; fstar-subp-company-backend: prefix nil
{"kind":"response","query-id":"10","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "10") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: candidates "cur"
>>> {"query-id":"11","query":"autocomplete","args":{"partial-symbol":"cur","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "cur") ("context" . "code"))] are late
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
{"kind":"response","query-id":"11","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "11") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"12","query":"lookup","args":{"context":"code","symbol":"cur","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":15}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "cur") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 15)))] are late
{"kind":"response","query-id":"12","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "12") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
>>> {"query-id":"13","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":16}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 16)))] are late
{"kind":"response","query-id":"13","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "13") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
>>> {"query-id":"14","query":"lookup","args":{"context":"code","symbol":"u","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "u") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 17)))] are late
{"kind":"response","query-id":"14","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "14") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: candidates "uin"
>>> {"query-id":"15","query":"autocomplete","args":{"partial-symbol":"uin","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uin") ("context" . "code"))] are late
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
{"kind":"response","query-id":"15","status":"success","response":[[3,"Demo.Deps","uint32"],[3,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "15") (status . "success") (response (3 "Demo.Deps" "uint32") (3 "Demo.Deps" "uint8"))))
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: annotation #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: annotation #("uint8" 0 5 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: match #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: pre-render #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: pre-render "Demo.Deps"
;;; fstar-subp-company-backend: match #("uint8" 0 5 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: pre-render #("uint8" 0 5 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
;;; fstar-subp-company-backend: pre-render "Demo.Deps"
;;; fstar-subp-company-backend: meta #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 3))
>>> {"query-id":"16","query":"lookup","args":{"symbol":"Demo.Deps.uint32","context":"code","requested-info":["type","documentation"]}}
{"kind":"response","query-id":"16","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "16") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; fstar-subp-company-backend: init nil
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: no-cache "uin"
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: candidates "uint"
>>> {"query-id":"17","query":"autocomplete","args":{"partial-symbol":"uint","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint") ("context" . "code"))] are late
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: prefix nil
{"kind":"response","query-id":"17","status":"success","response":[[4,"Demo.Deps","uint32"],[4,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "17") (status . "success") (response (4 "Demo.Deps" "uint32") (4 "Demo.Deps" "uint8"))))
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: meta "uint8"
>>> {"query-id":"18","query":"lookup","args":{"symbol":null,"context":null,"requested-info":["type","documentation"]}}
{"kind":"response","query-id":"18","status":"protocol-violation","response":"JSON decoding failed: expected string, got null"}
;;; Complete message received: (status: "protocol-violation"; message: ((kind . "response") (query-id . "18") (status . "protocol-violation") (response . "JSON decoding failed: expected string, got null")))
>>> {"query-id":"19","query":"lookup","args":{"context":"code","symbol":"uint","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":20}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 20)))] are late
{"kind":"response","query-id":"19","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "19") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: no-cache #("uint" 0 4 (fontified t))
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: candidates "uint3"
>>> {"query-id":"20","query":"autocomplete","args":{"partial-symbol":"uint3","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint3") ("context" . "code"))] are late
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: prefix nil
{"kind":"response","query-id":"20","status":"success","response":[[5,"Demo.Deps","uint32"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "20") (status . "success") (response (5 "Demo.Deps" "uint32"))))
;;; fstar-subp-company-backend: sorted nil
;;; fstar-subp-company-backend: duplicates nil
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: pre-render #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 5))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: ignore-case nil
;;; fstar-subp-company-backend: pre-render #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 5))
;;; fstar-subp-company-backend: meta #("uint32" 0 6 (fstar--context code fstar--annot "Demo.Deps" fstar--match-end 5))
>>> {"query-id":"21","query":"lookup","args":{"symbol":"Demo.Deps.uint32","context":"code","requested-info":["type","documentation"]}}
{"kind":"response","query-id":"21","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "21") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"22","query":"lookup","args":{"context":"code","symbol":"uint3","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":21}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint3") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 21)))] are late
;;; fstar-subp-company-backend: no-cache "uint3"
;;; fstar-subp-company-backend: prefix nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: require-match nil
;;; fstar-subp-company-backend: prefix nil
{"kind":"response","query-id":"22","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "22") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"23","query":"lookup","args":{"context":"code","symbol":"uint32","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":22}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint32") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 22)))] are late
{"kind":"response","query-id":"23","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "23") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"24","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32 (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
;;; fstar-subp-company-backend: prefix nil
{"kind":"response","query-id":"24","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,33],"end":[4,33]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "24") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 33) (end 4 33)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 33 33]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"25","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":23}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 23)))] are late
{"kind":"response","query-id":"25","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "25") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"26","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{ (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"26","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,34],"end":[4,34]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "26") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 34) (end 4 34)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" 4 4 34 34]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"27","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":23}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 23)))] are late
{"kind":"response","query-id":"27","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "27") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)

[cpitclaudel]

It does! How surprising. Hold on.

[cpitclaudel]

There a missing annotation on this "uint8". I need to understand whether it's removed by company-or by us. Can you add these two and reproduce the issue?

(defun fstar-subp-company-backend (command &optional arg &rest _rest)
  "Company backend for F*.
Candidates are provided by the F* subprocess.
COMMAND, ARG, REST: see `company-backends'."
  (interactive '(interactive))
  (fstar-log 'info "fstar-subp-company-backend: %S %S" command arg)
  (when (fstar--has-feature 'autocomplete)
    (let ((retv (pcase command
                  (`interactive
                   (company-begin-backend #'fstar-subp-company-backend))
                  (`prefix
                   (fstar-subp-company--prefix))
                  (`candidates
                   (fstar-subp-company-candidates arg fstar-subp-company--completion-context))
                  (`meta
                   `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
                  (`doc-buffer
                   `(:async . ,(apply-partially #'fstar-subp-company--async-doc-buffer arg)))
                  (`quickhelp-string
                   `(:async . ,(apply-partially #'fstar-subp-company--async-quickhelp arg)))
                  (`location
                   `(:async . ,(apply-partially #'fstar-subp-company--async-location arg)))
                  (`sorted t)
                  (`no-cache t)
                  (`duplicates nil)
                  (`match (get-text-property 0 'fstar--match-end arg))
                  (`annotation (get-text-property 0 'fstar--annot arg))
                  (`pre-render arg) ;; Preserve fontification of candidates
                  (`post-completion (fstar-subp-company--post-completion arg)))))
      (fstar--log 'info "-> %S" retv)
      retv)))

(defun fstar-subp-company--candidates-continuation (context callback status response)
  "Handle the results (STATUS, RESPONSE) of an `autocomplete' query.
Return (CALLBACK CANDIDATES).  CONTEXT is propertized onto all candidates."
  (pcase status
    ((or `failure `interrupted)
     (funcall callback nil))
    (`success
     (run-with-timer 2 nil
                     (lambda ()
                       (save-match-data
                         (funcall
                          callback
                          (let ((results (if (fstar--has-feature 'json-subp)
                                             (mapcar (apply-partially
                                                      #'fstar-subp-company-json--make-candidate context)
                                                     response)
                                           (delq nil
                                                 (mapcar (apply-partially
                                                          #'fstar-subp-company-legacy--make-candidate context)
                                                         (split-string response "\n"))))))
                            (fstar-log 'info "Company results: %S" results)
                            results))))))))

Sorry for the trouble. I'm hoping that this one of the last steps of data collection.

[nikswamy]

Did you mean for the last snippet of fstar-subp-company-backend to replace the previous one?

That's what I did and got this ... but the warning didn't show up. Instead, I got ```Error running timer: (void-variable callback) [3 times]

```;;; Started F* interactive: ("d:/workspace/everest/FStar/bin/fstar.exe" "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" "--ide" "--smt" "d:/workspace/everest/z3-4.5.1.1f29cebd4df6-x64-win/bin/z3.exe" "--cache_checked_modules" "--use_hints" "--use_hint_hashes" "--use_two_phase_tc" "true" "--use_extracted_interfaces" "--use_two_phase_tc" "true" "--max_fuel" "0" "--max_ifuel" "0")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add"]}
{"kind":"message","level":"warning","contents":"Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test2.fst.hints; ran without hints\n"}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add")))
;;; Complete message received: (status: nil; message: ((kind . "message") (level . "warning") (contents . "Unable to open hints file: d:\\workspace\\everest\\FStar\\examples\\demos\\low-star\\Test2.fst.hints; ran without hints
;;; ")))
;;; [209.18ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module Test2\nopen Demo.Deps\n\nlet test l (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n"}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"module Test2\nopen Demo.Deps\n","line":1,"column":0}}
{"kind":"response","query-id":"1","status":"success","response":null}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "1") (status . "success") (response . :json-null)))
{"kind":"response","query-id":"2","status":"success","response":[]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "2") (status . "success") (response)))
;;; Queue is empty (1 overlays)
>>> {"query-id":"3","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":0}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 0)))] are late
{"kind":"response","query-id":"3","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "3") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"4","query":"lookup","args":{"context":"code","symbol":"let","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":3}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "let") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 3)))] are late
{"kind":"response","query-id":"4","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "4") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"5","query":"lookup","args":{"context":"code","symbol":"test","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":8}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "test") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 8)))] are late
{"kind":"response","query-id":"5","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "5") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"6","query":"lookup","args":{"context":"code","symbol":"l","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":10}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "l") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 10)))] are late
{"kind":"response","query-id":"6","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "6") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"7","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":11}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 11)))] are late
{"kind":"response","query-id":"7","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "7") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"8","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":12}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 12)))] are late
{"kind":"response","query-id":"8","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "8") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"9","query":"peek","args":{"kind":"lax","code":"\nlet test l ( (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"9","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,22],"end":[4,22]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "9") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 22) (end 4 22)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 22 22]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "c"
>>> {"query-id":"10","query":"lookup","args":{"context":"code","symbol":"c","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":13}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "c") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 13)))] are late
{"kind":"response","query-id":"10","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "10") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "cu"
>>> {"query-id":"11","query":"lookup","args":{"context":"code","symbol":"cu","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":14}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "cu") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 14)))] are late
;;; fstar-subp-company-backend: prefix nil
;;; -> nil
{"kind":"response","query-id":"11","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "11") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"12","query":"lookup","args":{"context":"code","symbol":"cur","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":15}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "cur") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 15)))] are late
{"kind":"response","query-id":"12","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "12") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"13","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":16}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 16)))] are late
{"kind":"response","query-id":"13","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "13") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "u"
>>> {"query-id":"14","query":"lookup","args":{"context":"code","symbol":"u","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "u") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 17)))] are late
{"kind":"response","query-id":"14","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "14") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "ui"
;;; fstar-subp-company-backend: prefix nil
;;; -> "uin"
;;; fstar-subp-company-backend: ignore-case nil
;;; -> nil
;;; fstar-subp-company-backend: candidates "uin"
>>> {"query-id":"15","query":"autocomplete","args":{"partial-symbol":"uin","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uin") ("context" . "code"))] are late
;;; -> (:async closure ((x . needs-callback) (retv needs-callback) (context . code) (prefix . "uin") cl-struct-fstar-ns-or-mod-info-tags cl-struct-fstar-option-info-tags cl-struct-fstar-symbol-info-tags cl-struct-fstar-lookup-result-tags cl-struct-fstar-issue-tags cl-struct-fstar-subp-query-tags auto-insert-alist fstar--fqn-at-point-syntax-table cl-struct-fstar-location-tags t) (cb) (let* ((v retv)) (setcdr v (apply-partially (function fstar-subp-company--candidates-continuation) context cb))))
;;; fstar-subp-company-backend: sorted nil
;;; -> t
;;; fstar-subp-company-backend: duplicates nil
;;; -> nil
{"kind":"response","query-id":"15","status":"success","response":[[3,"Demo.Deps","uint32"],[3,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "15") (status . "success") (response (3 "Demo.Deps" "uint32") (3 "Demo.Deps" "uint8"))))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "uint"
;;; fstar-subp-company-backend: ignore-case nil
;;; -> nil
;;; fstar-subp-company-backend: candidates "uint"
>>> {"query-id":"16","query":"autocomplete","args":{"partial-symbol":"uint","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint") ("context" . "code"))] are late
;;; -> (:async closure ((x . needs-callback) (retv needs-callback) (context . code) (prefix . "uint") cl-struct-fstar-ns-or-mod-info-tags cl-struct-fstar-option-info-tags cl-struct-fstar-symbol-info-tags cl-struct-fstar-lookup-result-tags cl-struct-fstar-issue-tags cl-struct-fstar-subp-query-tags auto-insert-alist fstar--fqn-at-point-syntax-table cl-struct-fstar-location-tags t) (cb) (let* ((v retv)) (setcdr v (apply-partially (function fstar-subp-company--candidates-continuation) context cb))))
;;; fstar-subp-company-backend: sorted nil
;;; -> t
;;; fstar-subp-company-backend: duplicates nil
;;; -> nil
{"kind":"response","query-id":"16","status":"success","response":[[4,"Demo.Deps","uint32"],[4,"Demo.Deps","uint8"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "16") (status . "success") (response (4 "Demo.Deps" "uint32") (4 "Demo.Deps" "uint8"))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"17","query":"lookup","args":{"context":"code","symbol":"uint","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":20}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 20)))] are late
{"kind":"response","query-id":"17","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "17") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "uint3"
;;; fstar-subp-company-backend: ignore-case nil
;;; -> nil
;;; fstar-subp-company-backend: candidates "uint3"
>>> {"query-id":"18","query":"autocomplete","args":{"partial-symbol":"uint3","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint3") ("context" . "code"))] are late
;;; -> (:async closure ((x . needs-callback) (retv needs-callback) (context . code) (prefix . "uint3") cl-struct-fstar-ns-or-mod-info-tags cl-struct-fstar-option-info-tags cl-struct-fstar-symbol-info-tags cl-struct-fstar-lookup-result-tags cl-struct-fstar-issue-tags cl-struct-fstar-subp-query-tags auto-insert-alist fstar--fqn-at-point-syntax-table cl-struct-fstar-location-tags t) (cb) (let* ((v retv)) (setcdr v (apply-partially (function fstar-subp-company--candidates-continuation) context cb))))
;;; fstar-subp-company-backend: sorted nil
;;; -> t
;;; fstar-subp-company-backend: duplicates nil
;;; -> nil
{"kind":"response","query-id":"18","status":"success","response":[[5,"Demo.Deps","uint32"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "18") (status . "success") (response (5 "Demo.Deps" "uint32"))))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "uint32"
;;; fstar-subp-company-backend: ignore-case nil
;;; -> nil
;;; fstar-subp-company-backend: candidates "uint32"
>>> {"query-id":"19","query":"autocomplete","args":{"partial-symbol":"uint32","context":"code"}}
;;; Results for [cl-struct-fstar-subp-query "autocomplete" (("partial-symbol" . "uint32") ("context" . "code"))] are late
;;; -> (:async closure ((x . needs-callback) (retv needs-callback) (context . code) (prefix . "uint32") cl-struct-fstar-ns-or-mod-info-tags cl-struct-fstar-option-info-tags cl-struct-fstar-symbol-info-tags cl-struct-fstar-lookup-result-tags cl-struct-fstar-issue-tags cl-struct-fstar-subp-query-tags auto-insert-alist fstar--fqn-at-point-syntax-table cl-struct-fstar-location-tags t) (cb) (let* ((v retv)) (setcdr v (apply-partially (function fstar-subp-company--candidates-continuation) context cb))))
;;; fstar-subp-company-backend: sorted nil
;;; -> t
;;; fstar-subp-company-backend: duplicates nil
;;; -> nil
{"kind":"response","query-id":"19","status":"success","response":[[6,"Demo.Deps","uint32"]]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "19") (status . "success") (response (6 "Demo.Deps" "uint32"))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"20","query":"lookup","args":{"context":"code","symbol":"uint32","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":22}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "uint32") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 22)))] are late
{"kind":"response","query-id":"20","status":"success","response":{"kind":"symbol","name":"Demo.Deps.uint32","defined-at":null,"type":"Type0","documentation":null,"definition":null}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "20") (status . "success") (response (kind . "symbol") (name . "Demo.Deps.uint32") (defined-at . :json-null) (type . "Type0") (documentation . :json-null) (definition . :json-null))))
;;; fstar-subp-company-backend: init nil
;;; -> nil
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"21","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":23}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 23)))] are late
{"kind":"response","query-id":"21","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "21") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"22","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{ (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"22","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,34],"end":[4,34]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "22") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 34) (end 4 34)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 34 34]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "f"
>>> {"query-id":"23","query":"lookup","args":{"context":"code","symbol":"f","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":24}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "f") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 24)))] are late
{"kind":"response","query-id":"23","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "23") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"24","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{f (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"24","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,35],"end":[4,35]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "24") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 35) (end 4 35)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 35 35]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> "fa"
>>> {"query-id":"25","query":"lookup","args":{"context":"code","symbol":"fa","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":25}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "fa") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 25)))] are late
{"kind":"response","query-id":"25","status":"failure","response":"No such symbol, module, or namespace."}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "25") (status . "failure") (response . "No such symbol, module, or namespace.")))
;;; Queue is empty (1 overlays)
>>> {"query-id":"26","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{fa (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"26","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,36],"end":[4,36]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "26") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 36) (end 4 36)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 36 36]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"27","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":26}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 26)))] are late
{"kind":"response","query-id":"27","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "27") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"28","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{fa] (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"28","status":"success","response":[{"level":"error","message":"Syntax error: Parsing.Parse_error","ranges":[{"fname":"<input>","beg":[4,26],"end":[4,26]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "28") (status . "success") (response ((level . "error") (message . "Syntax error: Parsing.Parse_error") (ranges ((fname . "<input>") (beg 4 26) (end 4 26)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 26 26]) "Syntax error: Parsing.Parse_error"])
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"29","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":26}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 26)))] are late
{"kind":"response","query-id":"29","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "29") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
;;; fstar-subp-company-backend: prefix nil
;;; -> ""
>>> {"query-id":"30","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":4,"column":27}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 4) ("column" . 27)))] are late
{"kind":"response","query-id":"30","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "30") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"31","query":"peek","args":{"kind":"lax","code":"\nlet test l (cur:uint32{fa}) (src dest:lbuffer l uint8)\n  : ST _ _ _ = ()\n","line":3,"column":0}}
{"kind":"response","query-id":"31","status":"success","response":[{"level":"error","message":"Identifier not found: [fa]","ranges":[{"fname":"<input>","beg":[4,23],"end":[4,25]}]}]}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "31") (status . "success") (response ((level . "error") (message . "Identifier not found: [fa]") (ranges ((fname . "<input>") (beg 4 23) (end 4 25)))))))
;;; Highlighting Flycheck issues: ([cl-struct-fstar-issue error ([cl-struct-fstar-location "d:/workspace/everest/FStar/examples/demos/low-star/Test2.fst" 4 4 23 25]) "Identifier not found: [fa]"])
;;; Queue is empty (1 overlays)
>>> {"query-id":"32","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":5,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 5) ("column" . 17)))] are late
{"kind":"response","query-id":"32","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "32") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"33","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":5,"column":17}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 5) ("column" . 17)))] are late
{"kind":"response","query-id":"33","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "33") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"34","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":6,"column":0}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 6) ("column" . 0)))] are late
{"kind":"response","query-id":"34","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "34") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)
>>> {"query-id":"35","query":"lookup","args":{"context":"code","symbol":"","requested-info":["type","documentation"],"location":{"filename":"<input>","line":6,"column":0}}}
;;; Results for [cl-struct-fstar-subp-query "lookup" (("context" . "code") ("symbol" . "") ("requested-info" type documentation) ("location" ("filename" . "<input>") ("line" . 6) ("column" . 0)))] are late
{"kind":"response","query-id":"35","status":"success","response":{"kind":"namespace","name":"","loaded":false}}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "35") (status . "success") (response (kind . "namespace") (name . "") (loaded . :json-false))))
;;; Queue is empty (1 overlays)

[nikswamy]

happy to try to collect more data for you, if it helps

[cpitclaudel]

Ah, stupid me, sorry. Your .emacs is using dynamic scoping; that's why the timer thing failed. Thanks for the debugging help. The following should be easier: can you replace everything I suggested earlier with a simple (load "~/.emacs.d/fstar-patches.el"), and put the following in a file called ~/.emacs.d/fstar-patches.el?

;; -*- lexical-binding: t; -*-

(require 'fstar-mode)

(defun fstar-subp-company--candidates-continuation (context callback status response)
  "Handle the results (STATUS, RESPONSE) of an `autocomplete' query.
Return (CALLBACK CANDIDATES).  CONTEXT is propertized onto all candidates."
  (pcase status
    ((or `failure `interrupted)
     (funcall callback nil))
    (`success
     (save-match-data
       (funcall
        callback
        (let ((results (if (fstar--has-feature 'json-subp)
                           (mapcar (apply-partially
                                    #'fstar-subp-company-json--make-candidate context)
                                   response)
                         (delq nil
                               (mapcar (apply-partially
                                        #'fstar-subp-company-legacy--make-candidate context)
                                       (split-string response "\n"))))))
          (fstar-log 'info "Company results: %S" results)
          results))))))

(defun fstar-subp-company-backend (command &optional arg &rest _rest)
  "Company backend for F*.
Candidates are provided by the F* subprocess.
COMMAND, ARG, REST: see `company-backends'."
  (interactive '(interactive))
  (fstar-log 'info "fstar-subp-company-backend: %S %S" command arg)
  (when (fstar--has-feature 'autocomplete)
    (let ((retv (pcase command
                  (`interactive
                   (company-begin-backend #'fstar-subp-company-backend))
                  (`prefix
                   (fstar-subp-company--prefix))
                  (`candidates
                   (fstar-subp-company-candidates arg fstar-subp-company--completion-context))
                  (`meta
                   `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
                  (`doc-buffer
                   `(:async . ,(apply-partially #'fstar-subp-company--async-doc-buffer arg)))
                  (`quickhelp-string
                   `(:async . ,(apply-partially #'fstar-subp-company--async-quickhelp arg)))
                  (`location
                   `(:async . ,(apply-partially #'fstar-subp-company--async-location arg)))
                  (`sorted t)
                  (`no-cache t)
                  (`duplicates nil)
                  (`match (get-text-property 0 'fstar--match-end arg))
                  (`annotation (get-text-property 0 'fstar--annot arg))
                  (`pre-render arg) ;; Preserve fontification of candidates
                  (`post-completion (fstar-subp-company--post-completion arg)))))
      (fstar--log 'info "fstar-subp-company-backend: %S %S -> %S" command arg retv)
      retv)))

Thanks!

[cpitclaudel]

Any updates on this?

[cpitclaudel]

Nik and I chatted about this on the phone. There was a recent-ish change in company (https://github.com/company-mode/company-mode/issues/760) to work around an Emacs bug that we suspect might be related. We could not immediately reproduce the issue after updating company.

If this comes up again I'll debug in person, likely at PLDI.

[cpitclaudel]

If this comes up again I'll debug in person, likely at PLDI.

Looks like I will have to ^^

[nikswamy]

Hi Clement. Can you remind me: What's the recommended way to update company? And the recommended way to check which version is currently being used? I installed it again from melpa but now it tells me that I have two versions of company installed.

[cpitclaudel]

Use M-x list-packages to get a package list, then wait for the refresh to complete. Press U to mark all packages for an update, then x to execute it.

You could also do M-x package-refresh-contents followed by M-x package-reinstall RET company RET