search

FStarLang / fstar-mode.el

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

No company completion #103

Closed brettgilio closed 5 years ago

brettgilio commented 5 years ago

Hi all. I installed fstar through Opam, and have fstar.exe and z3 on my path. However, I have no completion through company or using C-return. I have company installed, and it works for other languages, just not fstar. Thoughts?

{"kind":"response","query-id":"14","status":"failure","response":"Current module unset"}
;;; Complete message received: (status: "failure"; message: ((kind . "response") (query-id . "14") (status . "failure") (response . "Current module unset")))
;;; Query "14" completed in 0.0010s
;;; [5.75ms] Fetched results for #s(fstar-subp-query "autocomplete" (("partial-symbol" . "app") ("context" . "code")))
;;; Queue is empty (0 overlays)
cpitclaudel commented 5 years ago

Thanks for including debug output. You won't get completion until you've processed (C-c C-n or C-c C-RET) the initial module XXX line of your file, which enables most features on the F* side, including completion.

brettgilio commented 5 years ago

Thank you for your help with that! Now I am having an issue with It not finding any of the FStar submodules. like FStar.All or FStar.List saying that the namespace can not be found. Sorry for the bother, I am new to FStar and trying to figure this out.

cpitclaudel commented 5 years ago

That would be best discussed on the FStar tracker :) I think your issue here is that all imports are processed when you start F, so you need to open FStar.List (or use it anywhere in your file) and restart F (or press C-c C-r)

brettgilio commented 5 years ago

Thank you!