auto completion doesn't use prefix

avigad commented 9 years ago

If I start a new file and type

import standard

open nat

theorem test (x y z : ℕ) : x = x := eq.re

I get a list of completions such as false.rec, relation.is_equivalence.rec, ... but not eq.refl.

If I continue and type the "f", the first suggestion is eq.refl, but I also get suggestions like iff.refl and false.rec.

Is this the intended behavior?

leodemoura commented 9 years ago

Could you get the latest changes, and try again? I get the following list of completions:

leodemoura commented 9 years ago

Lean uses "fuzzy" matching. "false.rec" is in the list because it contains the substring "e.re" which matches "eq.re" modulo 1 error. Lean uses the following fuzzy matching procedure http://en.wikipedia.org/wiki/Bitap_algorithm

avigad commented 9 years ago

Curiously, I don't get exactly the same list, but it is reasonable.

screenshot

leodemoura commented 9 years ago

@avigad The behavior you are getting does not look reasonable. Could you double check you have the latest version? I explicitly added code to display "prefix" exact matches before other matches, and sort matches by the number of errors. "false.rec" is not an prefix match, nor it has 0 errors. "eq.refl" must occur first.

avigad commented 9 years ago

I fetched and rebuilt just before testing again (commit ba35ca5, I think).

But come to think of it, when I exit, I still get "Active processes exist; kill them and exit anyway?". Didn't Soonho correct that? Is there something I need to do to recompile lean-mode? How can I tell which version I am using?

leodemoura commented 9 years ago

To use the latest lean-mode we need to restart emacs. @soonhokong Any additional remarks?

soonhokong commented 9 years ago

@avigad, @leodemoura: the previous way of killing lean-process before emacs exit had some problems. I just push a fix 5c89e70a23c05c7470a88ea5e5d949e34c638a30.

avigad commented 9 years ago

The plot thickens. Over the weekend I was using my computer at home (a laptop). I just tried fetched, rebuilt, and tried it on my office computer. The choices are closer to the ones that Leo gets but still not perfect; in particular, decidable_eq.rec comes first.

test

I would be glad to send additional information if you let me know what might be helpful.

In case it is relevant, the test.lean file I am editing is not in the lean folder, it is in a separate folder.

avigad commented 9 years ago

In case it is helpful, here is lean-server.

Sent Message: VISIT /home/avigad/projects/lean_work/test.lean Sent Message: INFO 1 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away:Sent Message: INFO 1 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 1 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: FINDP 1 standard Received Message: -- BEGINFINDP NAY -- ENDFINDP

The following pre-message will be thrown away: Sent Message: REPLACE 1 import standard Sent Message: INFO 1 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 1 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 1 Received Message: -- BEGININFO -- ENDINFO

The following pre-message will be thrown away: Sent Message: INSERT 2

Sent Message: REPLACE 1 import standard Sent Message: REPLACE 2 open nat Sent Message: INFO 2 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 2 Received Message: -- BEGININFO STALE NAY -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 2 Received Message: -- BEGININFO -- ENDINFO

The following pre-message will be thrown away: Sent Message: INSERT 3

Sent Message: REPLACE 2 open nat Sent Message: INSERT 4

Sent Message: REPLACE 3

Sent Message: FINDP 4 theo Received Message: -- BEGINFINDP tactic.and_then|tactic → tactic → tactic -- ENDFINDP

The following pre-message will be thrown away: Sent Message: REPLACE 4 theo Sent Message: INSERT 5

Sent Message: REPLACE 4 theo Sent Message: REPLACE 4 theor Sent Message: REMOVE 4 Sent Message: REPLACE 4 theor Sent Message: REPLACE 4 theorem tst (x y z : ℕ) : x Sent Message: INFO 4 Received Message: -- BEGININFO STALE NAY -- ENDINFO

Sent Message: REPLACE 4 theorem tst (x y z : ℕ) : x = y := Sent Message: INSERT 5

Sent Message: REPLACE 4 theorem tst (x y z : ℕ) : x = y := The following pre-message will be thrown away: Sent Message: INFO 5 Received Message: -- BEGININFO STALE -- ENDINFO

The following pre-message will be thrown away: Sent Message: FINDP 5 eq.re Received Message: -- BEGINFINDP decidable_eq.rec|(Π (a : Π (x y : ?A), decidable (eq x y)), ?C (decidable_eq.intro a)) → (Π (n : decidable_eq ?A), ?C n) eq.rec_id|∀ (H : eq ?a ?a) (b : ?B ?a), eq (eq.rec b H) b eq.rec_on_id|∀ (H : eq ?a ?a) (b : ?B ?a), eq (eq.rec_on H b) b eq.refl|∀ (a : ?A), eq a a eq.rec_on_compose|∀ (H1 : eq ?a ?b) (H2 : eq ?b ?c) (u : ?P ?a), eq (eq.rec_on H2 (eq.rec_on H1 u)) (eq.rec_on (eq.trans H1 H2) u) eq.rec_on|eq ?a1 ?a2 → ?B ?a1 → ?B ?a2 eq.rec|?C ?a → (Π {a : ?A}, eq ?a a → ?C a) false.rec|∀ (C : Prop), false → C relation.is_equivalence.rec|(relation.is_reflexive ?R → relation.is_symmetric ?R → relation.is_transitive ?R → ?C) → relation.is_equivalence ?R → ?C relation.congruence.rec|((Π (x y : ?T1), ?R1 x y → ?R2 (?f x) (?f y)) → ?C) → relation.congruence ?R1 ?R2 ?f → ?C subtype.rec|(Π (x : ?A) (a : ?P x), ?C (subtype.tag x a)) → (Π (n : subtype ?P), ?C n) decidable.rec|(Π (a : ?p), ?C (decidable.inl a)) → (Π (a : not ?p), ?C (decidable.inr a)) → (Π (n : decidable ?p), ?C n) relation.congruence2.rec|((Π (x1 y1 : ?T1) (x2 y2 : ?T2), ?R1 x1 y1 → ?R2 x2 y2 → ?R3 (?f x1 x2) (?f y1 y2)) → ?C) → relation.congruence2 ?R1 ?R2 ?R3 ?f → ?C relation.is_reflexive.rec|(relation.reflexive ?R → ?C) → relation.is_reflexive ?R → ?C relation.is_transitive.rec|(relation.transitive ?R → ?C) → relation.is_transitive ?R → ?C inhabited.rec|(Π (a : ?A), ?C (inhabited.mk a)) → (Π (n : inhabited ?A), ?C n) decidable.rec_on|decidable ?p → (?p → ?C) → (not ?p → ?C) → ?C list.append_eq_reverse_cons|eq (list.append ?x ?l) (list.reverse (list.cons ?x (list.reverse ?l))) false.rec_type|Π (A : Type), false → A relation.mp_like.rec|((?a → ?b) → ?C) → relation.mp_like ?H → ?C

Received Message: true.rec|?C → true → ?C -- ENDFINDP

The following pre-message will be thrown away: Sent Message: REPLACE 5 eq.re Sent Message: INSERT 6

Sent Message: REPLACE 5 eq.re Sent Message: INFO 5 Received Message: -- BEGININFO STALE -- ENDINFO

The following pre-message will be thrown away: Sent Message: INFO 5 Received Message: -- BEGININFO STALE -- ENDINFO

The following pre-message will be thrown away:

leodemoura commented 9 years ago

@avigad I managed to reproduce the behavior you described. I submitted a fix.

Thanks!

leanprover / lean3

auto completion doesn't use prefix #147