Suggestions about suggestion ordering

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode

GNU General Public License v3.0

354 stars 29 forks source link

Suggestions about suggestion ordering #44

Open JasonGross opened 8 years ago

JasonGross commented 8 years ago

[x] reflexivity should come before refine <term>
[x] constructor should come before constructor num
[ ] discriminate (with no arguments, possibly all the variants) should come before discrR (which doesn't even seem to exist?)
[x] Goal Prop should not suggest Proposition # : #._Proof._#_Qed.
[x] Goal Set should not suggest Search @{term_pattern}
[x] Goal Type should not suggest Typeclasses eauto :=.

Feel free to edit this and ~~crossout~~ any that are fixed.

cpitclaudel commented 8 years ago

Did you update recently? I've should have fixed the first two ones a few days ago.

cpitclaudel commented 8 years ago

Regarding the last three ones, the best I can do is probably mark Set, Prop, and Type reserved (so they'll behave just like with or fun. Is that what you had in mind?

cpitclaudel commented 8 years ago

I've marked Prop, Set, and Type as reserved. Feel free to add more things to that list, and I'll see what I can do :)

JasonGross commented 8 years ago

Thanks!

JasonGross commented 1 year ago

There seems to be a regression on reflexivity vs refine (and I just updated)

I propose that suggestions should be ordered by unigram statistics. Here's the ordered list of tactics (aka single tokens starting with a lowercase letter), and of vernaculars (like tactics but starting with an uppercase letter). Counts are for occurrences across all devs on Coq's CI as of a year or so ago.

It might be worth fine-tuning the orderings according to frequency of occurrence in the current file being edited, too?

cpitclaudel commented 1 year ago

That list is great. Problem is we will lose the links to the docs if we use it plain, but maybe we can merge the two data sources? I'm out for the next two weeks :/

JasonGross commented 1 year ago

Yeah, this list is meant to be just for ordering, and definitely should be merged with the other data source. My search criterion was "single words starting with a lowercase", so you don't even want to use this list without filtering for "real" tactics, otherwise you'll pick up, e.g., all the custom tactics from every project even if they don't exist in the file the suggestions are happening in.