Completion support

[cpitclaudel]

Hi all,

Based on @nikswamy's experiments I looked at adding completion support to fstar-mode.el. I cobbled together a rough prototype at https://github.com/FStarLang/fstar-mode.el/tree/company , with corresponding F* patches at https://github.com/cpitclaudel/FStar/tree/clement_info

Here's how it looks:

The basic idea is that fstar-mode send a search term, and F responds with a list of candidates. Then, while displaying search terms, fstar-mode queries the underlying F process to get type information. If you feel adventurous, you can test it by checking out and compiling the branches linked above :) (you'll need to M-x package-install company on the Emacs side)

Remaining issues:

• [x] Results aren't sorted
• [ ] Completion only returns definitions, not modules (what else would be relevant?)
• [x] Completion only returns fully qualified names, instead of using the shortest name in scope (e.g. "Som" should complete to "Some", not "Prims.Some" — but "Pr.So" should complete to "Prims.Some")
• [x] The implementation of the #info-fqn query is horrendous (it doesn't have to be: I just didn't know which function to call to resolve a fully-qualified name)
• [x] I haven't measured performance. What's a typical number of symbols in scope in F* (does it run in the thousands, or tens of thousands, or...)?
• [x] Company's completion popups flicker
• [x] The #info request doesn't work on non-fully-qualified names

Can a more experienced F* hacker help with the issues above? Thanks!

[cpitclaudel]

Completion only returns fully qualified names, instead of using the shortest name in scope (e.g. "Som" should complete to "Some", not "Prims.Some" — but "Pr.So" should complete to "Prims.Some")

Fixed.

The implementation of the #info-fqn query is horrendous (it doesn't have to be: I just didn't know which function to call to resolve a fully-qualified name)

Fixed too, though I'm not sure why lookup_id Prims.HasEq_bool fails.

[cpitclaudel]

[nikswamy]

I bow before your awesomeness! : )

I looked at your diff on the F* side. It looks pretty solid. Do you think you could contribute it as a pull request on FStarLang/FStar? I'll merge it in, first to nik_info, then to master ... Probably need to do a little massaging to get it to fit inside our somewhat baroque bootstrapping setup.

Also, FYI, although it's not in place at the moment, we plan to soon ask folks contributing to FStarLang/FStar to sign a CLA similar to https://cla.microsoft.com/cladoc/microsoft-contribution-license-agreement.pdf

[cpitclaudel]

Results aren't sorted

Fixed.

I also added support for company's location feature (C-w during completion):

[cpitclaudel]

I looked at your diff on the F* side. It looks pretty solid. Do you think you could contribute it as a pull request on FStarLang/FStar? I'll merge it in, first to nik_info, then to master ... Probably need to do a little massaging to get it to fit inside our somewhat baroque bootstrapping setup.

Ok, I'll open a PR. There are some bits that need performance tuning, I expect, but I'm happy to leave it to F* folks, once the performance becomes an issue :)

Also, FYI, although it's not in place at the moment, we plan to soon ask folks contributing to FStarLang/FStar to sign a CLA similar to https://cla.microsoft.com/cladoc/microsoft-contribution-license-agreement.pdf

That's fine (I already have a Microsoft one on file, if that helps).

[cpitclaudel]

Company's completion popups flicker

Fixed, a long as completion candidates come back fast enough. Flickers when F is too slow are unavoidable in company-mode's current state, but quick tests after loading most of F's standard library suggest that things are fine (it takes 15ms to get 2380 completion candidates on my machine).

Probably need to do a little massaging to get it to fit inside our somewhat baroque bootstrapping setup.

Done.

[nikswamy]

I've merged your changes to F* into FStarLang/FStar master and bumped the version number to 0.9.4.2

Been trying out the feature in the company branch and it works very well! Thank you!

Some wrinkles to iron out ... Recording them here to keep track of it. I'll try to fix them on the F* side, if you don't beat me to it.

• [X] Auto-completion doesn't seem to work with module abbreviations

e.g.,

module A
module L = FStar.List.Tot
let f = L.a //<--- doesn't complete to L.append etc.

• [X] As the snip below shows, the name and it's corresponding namespace appear in reverse order and are not separated ... perhaps the namespace in parentheses would do?

• [x] The completed name is not resolved

module A
module L = FStar.List.Tot
let f = app .... //<-- this is completed to "append"

However, the identifier append is not resolved; only L.append or FStar.List.Tot.append is resolvable. I guess the recommended completion needs to take into account the opened namespaces when suggesting name.

[cpitclaudel]

Auto-completion doesn't seem to work with module abbreviations

That's correct. The current algorithm just walks through all symbols and matches them against the search term. That matching should probably be extended to consider aliases too. I'm not sure what the most efficient way is.

the name and it's corresponding namespace appear in reverse order and are not separated

That one is easy :) (setq-default company-tooltip-align-annotations t). I'll make it the default.

The completed name is not resolved

That's a sign of my being confused about name resolution rules in F* :) I think the issue likely comes from https://github.com/FStarLang/FStar/blob/master/src/tosyntax/FStar.ToSyntax.Env.fs#L376

I'm happy to leave 1 and 3 to you ; 3 in particular should be easy to fix for someone with a good understanding of the scoping rules :)

[cpitclaudel]

Been trying out the feature in the company branch and it works very well! Thank you!

Thanks for testing :)

[nikswamy]

I'm having trouble installing company on one of my machines.

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

Leaving directory ‘c:/Users/nswamy/.emacs.d/elpa/company-0.9.2’

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-abbrev.el at Mon Mar 27 21:36:31 2017
Entering directory ‘c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/’

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-bbdb.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-capf.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-clang.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-cmake.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-css.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-dabbrev-code.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-dabbrev.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-eclim.el at Mon Mar 27 21:36:31 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-elisp.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-etags.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-files.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-gtags.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-ispell.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-keywords.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-nxml.el at Mon Mar 27 21:36:32 2017

In company-nxml-attribute-value:
company-nxml.el:106:24:Warning: looking-back called with 1 argument, but
    requires 2-3

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-oddmuse.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-pkg.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-semantic.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-template.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-tempo.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-xcode.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company-yasnippet.el at Mon Mar 27 21:36:32 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/company.el at Mon Mar 27 21:36:32 2017
Leaving directory ‘c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/’

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/all.el at Mon Mar 27 21:36:32 2017
Entering directory ‘c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/’

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/async-tests.el at Mon Mar 27 21:36:32 2017
async-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/bbdb-tests.el at Mon Mar 27 21:36:32 2017
bbdb-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/clang-tests.el at Mon Mar 27 21:36:33 2017
clang-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/core-tests.el at Mon Mar 27 21:36:33 2017
core-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/elisp-tests.el at Mon Mar 27 21:36:33 2017
elisp-tests.el:24:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/files-tests.el at Mon Mar 27 21:36:33 2017
files-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/frontends-tests.el at Mon Mar 27 21:36:33 2017
frontends-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/keywords-tests.el at Mon Mar 27 21:36:33 2017

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/template-tests.el at Mon Mar 27 21:36:33 2017
template-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

Compiling file c:/Users/nswamy/.emacs.d/elpa/company-0.9.2/test/transformers-tests.el at Mon Mar 27 21:36:33 2017
transformers-tests.el:22:1:Error: Cannot open load file: No such file or directory, company-tests

[nikswamy]

And if I ignore the failing tests and try to load fstar-mode.el anyway, I get

Warning (initialization): An error occurred while loading ‘c:/Users/nswamy/.emacs’:

File error: Cannot open load file, No such file or directory, company

[cpitclaudel]

How are you installing company? M-x package-install RET company RET?

[nikswamy]

yeah

[cpitclaudel]

It looks like the compilation process is recursing down subdirectories ­— it shouldn't do that. Maybe something in your .emacs? This is surprising.

[cpitclaudel]

Also, are you on MELPA stable or the regular MELPA?

[cpitclaudel]

My log looks like this:

Leaving directory ‘/build/emacs/melpa/sandbox/elpa/company-20170327.1753’

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-abbrev.el at Tue Mar 28 00:47:46 2017
Entering directory ‘/build/emacs/melpa/sandbox/elpa/company-20170327.1753/’

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-bbdb.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-capf.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-clang.el at Tue Mar 28 00:47:46 2017
company-clang.el:41:1:Warning: defcustom for
    ‘company-clang-begin-after-member-access’ fails to specify type
company-clang.el:41:1:Warning: defcustom for
    ‘company-clang-begin-after-member-access’ fails to specify type

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-cmake.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-css.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-dabbrev-code.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-dabbrev.el at Tue Mar 28 00:47:46 2017
company-dabbrev.el:59:1:Warning: defcustom for ‘company-dabbrev-ignore-case’
    fails to specify type
company-dabbrev.el:59:1:Warning: defcustom for ‘company-dabbrev-ignore-case’
    fails to specify type
company-dabbrev.el:64:1:Warning: defcustom for ‘company-dabbrev-downcase’
    fails to specify type
company-dabbrev.el:64:1:Warning: defcustom for ‘company-dabbrev-downcase’
    fails to specify type

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-eclim.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-elisp.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-etags.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-files.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-gtags.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-ispell.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-keywords.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-nxml.el at Tue Mar 28 00:47:46 2017

In company-nxml-attribute-value:
company-nxml.el:106:24:Warning: looking-back called with 1 argument, but
    requires 2-3

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-oddmuse.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-semantic.el at Tue Mar 28 00:47:46 2017
company-semantic.el:52:1:Warning: defcustom for
    ‘company-semantic-begin-after-member-access’ fails to specify type
company-semantic.el:52:1:Warning: defcustom for
    ‘company-semantic-begin-after-member-access’ fails to specify type

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-template.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-tempo.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-xcode.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company-yasnippet.el at Tue Mar 28 00:47:46 2017

Compiling file /build/emacs/melpa/sandbox/elpa/company-20170327.1753/company.el at Tue Mar 28 00:47:46 2017

[aseemr]

There are two company packages, one company-2017 ... which installs ok, one company 0.9.2 which fails.

[aseemr]

if i do list-packages, then i see both, and i can install one and not the other.

[nikswamy]

I trimmed down my .emacs to

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "http://melpa.org/packages"))
(package-initialize)
(require 'fstar-mode "~/workspace/fstar-mode.el/fstar-mode.el")

and this seems to work with company-0.9.2. Investigating ... will also try company-2017

[cpitclaudel]

I managed to reproduce it; @aseemr is right, there's something fishy with the ELPA version (ELPA is the FSF-sanctionned package archive; MELPA is the main community one).

[nikswamy]

now I can no longer reproduce it. I restored my full .emacs and it works fine now. : /

[cpitclaudel]

Well, problem solved then? :) I'll investigate on my side.

[cpitclaudel]

I merged the company branch into fstar-mode's master, btw, so the next MELPA build will yield an F* package that automatically pulls company-mode as a dependency.

[cpitclaudel]

I see what the problem is now; I misspoke earlier about package.el not recursing in subdirectories; it does (the thing that doesn't recurse is the program that collects autoload cookies). The problem is due to the ELPA package bundling too much (the MELPA one doesn't include the test/ folder).

[nikswamy]

so, should i

(setq package-archives
             '("melpa" . "http://melpa.org/packages"))

Rather than

(add-to-list 'package-archives
             '("melpa" . "http://melpa.org/packages"))

?

[cpitclaudel]

No, add-to-list should be fine. Normally (after running M-x package-refresh) Emacs should default to the MELPA version of company (its version number, 2017.…, ranks higher than 0.9.2). I'm not sure why it picked the ELPA one first. Possibly because you hadn't run M-x package-refresh first (opening the package list with M-x list-packages does that too).

[cpitclaudel]

Nik: your bug was fixed :) https://github.com/company-mode/company-mode/commit/90123e7097c17686951f7122be07bdf177e73618

[nikswamy]

I've updated F* so that in response to Completion requests, it only suggests names that are accessible. Names that are hidden due to shadowing (e.g., opened namespaces) etc. just don't show up in the completion list. It also deals with module abbreviations etc.

This seems to be the only remaining issue here: -- Completion only returns definitions, not modules (what else would be relevant?)

Returning only definitions seems reasonable to me. Eventually, we might want completion for modules, field names, projectors, discriminators etc. But, it might make sense to close this issue and track completion for other syntactic elements, as and when the need/requests for them come up.

[cpitclaudel]

I've updated F* so that in response to Completion requests, it only suggests names that are accessible. Names that are hidden due to shadowing (e.g., opened namespaces) etc. just don't show up in the completion list. It also deals with module abbreviations etc.

Great, thanks! It works nicely. Some small issues that I noticed:

• Completions for empty string don't use the shortest possible identifier. For example, if I'm in module Test and I run company-manual-begin (I bind it to C-RET), then I get Test.a in the list of results instead of a.

• Partial matches don't seem to be able to start halfway through the fully qualified name. For example if I type List.app and FStar isn't open I should get "FStar.List.append" as one of the candidates.

• There are some discontinuities in the output: if I type List I get List.Tot.Base.append as the first result, but if I add a dot that completion disappears and I get List.append instead.

A small feature request, too: in this part of info requests, I think it would be nice to print the fully qualified name (lid) instead symbol (that would make it clear what name symbol was resolved to).

               |> Util.map_option (fun ((_, typ), range) ->
                                   FStar.TypeChecker.Err.format_info (snd env) symbol typ range) in

Feel free to close this issue and move these to the F* tracker: I think my work on the Emacs side is done :)

Thanks for your help with testing!

[cpitclaudel]

Here are the tests I was using, btw:

open FStar
open FStar.List
open FStar.List.Tot

(* Completion tests:
let _ = List...app // List.Tot.Base.append
let _ = Som // → Some
let _ = Pr.Som // → Prims.Some
let _ = unzi
let _ = Al.all_po // → All.all_post
let _ = List.To.Ba.unz // → List.Tot.Base.unzip
let _ = Tot.B.unzip // → List.Tot.Base.unzip
let _ = Base.unzip // → List.Tot.Base.unzip (why not Base.unzip?)
let _ = List.To // List.Tot.Base.append
let _ = Tot.unzip // → *fail*
let _ = Lis.BZZZ // → fail *)

[nikswamy]

Would be good to get some feedback from @tahina-pro on this.

The completions for the List module are particularly idiosyncractic, since they involve module inclusions.

Arguably, a client module shouldn't even see module implementation details like List.Tot.Base etc.

Also, this probably just a question of taste, but I find it weird that Al.all_po should complete to All.all_post , i.e., partial matches on the namespace feel strange to me.

[cpitclaudel]

Also, this probably just a question of taste, but I find it weird that Al.all_po should complete to All.all_post , i.e., partial matches on the namespace feel strange to me.

They typically make it faster to type full names: instead of having to complete each bit, you just type a few letters of each namespace and press .. This of it as a lightweight version of Visual Studio's intellisense inserting autocompleting up to . when you press . (IIRC in VS if you're trying to write List.Base.Tot.append it's enough to type Li.B.T.app RET — things work the same here, but they don't aggressively insert each chunk into the buffer). I agree that there is a fair bit of taste involved here :)

[nikswamy]

(IIRC in VS if you're trying to write List.Base.Tot.append it's enough to type Li.B.T.app RET

This is not the behavior of at least Visual Studio's F# mode. You have to write List. to start getting completions from the List namespace.

[nikswamy]

BTW, I'm noticing some amazing behavior where fstar-mode.el is suggesting completions for me without me even launching F* on that file. How is that working? Does company mode have some built-in ctags-like completion feature?

[jkzinzindohoue]

I believe company is aware of all open file in the emacs session. If I may complain about a behaviour: I used to use company before the completion addition and I no longer get completion when F* is busy, which happens a significant amount of my editing time. Is there anyway to work around that ? Otherwise it works beautifully :)

[s-zanella]

Same request as @jkzinzindohoue.

[cpitclaudel]

BTW, I'm noticing some amazing behavior where fstar-mode.el is suggesting completions for me without me even launching F* on that file. How is that working? Does company mode have some built-in ctags-like completion feature?

Company uses various sources, indeed :) That includes contents of your current buffer, and possibly other buffers (it uses dabbrev under the hood). If you have tags, it can also use them.

If I may complain about a behaviour: I used to use company before the completion addition and I no longer get completion when F* is busy, which happens a significant amount of my editing time. Is there anyway to work around that ? Otherwise it works beautifully :)

Same request as @jkzinzindohoue.

Done.

[cpitclaudel]

This is not the behavior of at least Visual Studio's F# mode. You have to write List. to start getting completions from the List namespace.

I could also be misremembering :) (And I never tried F# is VS)

[cpitclaudel]

I think we can track future completion issues in separate threads, when they arise :)