Instance cache in the infoview

Stream: general

[Yaël Dillies]

Has the infoview access to the instance cache? If so, could we make this information available by coloring the name of an instance variable differently from a non-instance one? This would bring us closer to our mental model that "The infoview is all you need to see".

[Yaël Dillies]

Here's a (somewhat artificial) example where one can't tell whether a variable is in the instance cache or not:

import algebra.hom.equiv

variables {G H : Type*} [group G] [monoid H]

example (f : G ≃* H) : true :=
begin
  have my_instance : group H := { inv := sorry, mul_left_inv := sorry, ..‹monoid H› },
/-
G: Type u_1
H: Type u_2
_inst_1: group G
_inst_2: monoid H
f: G ≃* H
my_instance: group H
⊢ true-/
end

example (f : G ≃* H) : true :=
begin
  haveI my_instance : group H := { inv := sorry, mul_left_inv := sorry, ..‹monoid H› },
/-
G: Type u_1
H: Type u_2
_inst_1: group G
_inst_2: monoid H
f: G ≃* H
my_instance: group H
⊢ true-/
end

[Damiano Testa]

I do not know the answer to your question, but for your examples, G, f are unnecessary, right? Could you just have a type and prove with sorry that it is inhabited or is there something else that I am overlooking?

[Yaël Dillies]

The example was "Transfer the group structure on G to a group structure on H using f" :grinning:

[Eric Wieser]

I think the answer is "the infoview is implemented via widgets in leanprover-community/lean, so in theory it has access to everything"

[Damiano Testa]

Yaël, I guessed as much, I was simply making a Meaningless Working Example:

example {α} : true :=
begin
  have my_non_instance : inhabited α := sorry,
  haveI my_instance : inhabited α := sorry,
/-
α: Sort ?
my_non_instance my_instance: inhabited α
⊢ true -/
  trivial,
end

:face_palm:

[Damiano Testa]

There is a tactic frozen_local_instances: using trace frozen_local_instances, reveals that it interprets my_non_instance as a non-instance in isolation, but as an instance when my_instance is around.

example {α : Type*} : true :=
begin
--  have my_non_instance : inhabited α := sorry,   -- comment/uncomment this and the next line in all configurations and look at the trace!
  haveI my_instance : inhabited α := sorry,
  trace frozen_local_instances,
  trivial,
end

[Eric Wieser]

I think that might be a quirk in haveI; nice find!

[Yaël Dillies]

Does that mean haveI resets the instance cache?

[Yaël Dillies]

If I were to implement my above suggestion, is there a way for me to try out the modified infoview easily?

[Yaël Dillies]

Actually, the widgets are defined in core Lean, right? so I can literally write a test file that imports them and I will see the modified there?

[Patrick Massot]

You can override from user code, even outside mathlib.

[Patrick Massot]

See https://github.com/PatrickMassot/MDD154/blob/master/src/lib/interactive_expr.lean which is imported at https://github.com/PatrickMassot/MDD154/blob/master/src/lib/tactiques.lean

[Patrick Massot]

The last three lines of the first file do the magic of overriding the version of that file that is in mathlib.

[Patrick Massot]

You can compare with the mathlib version. The main changes should be the parenthesis option (this was before Kyle put an option in core Lean) and pretty printing bounded quantifiers (using code from #5440)

[Yaël Dillies]

A first try, with... salmon instances! Anne also offered pinkstances.

open tagged_format tactic
open widget widget.html widget.attr widget.interactive_expression

namespace inst_widget

/-- Component that displays the main (first) goal. -/
meta def tactic_view_goal {γ} (local_c : tc local_collection γ) (target_c : tc expr γ) : tc filter_type γ :=
tc.stateless $ λ ft, do
  is ← tactic.frozen_local_instances,
  let is' : list expr := option.cases_on is [] id,
  g@(expr.mvar u_n pp_n y) ← main_goal,
  t ← get_tag g,
  let case_tag : list (html γ) :=
    match interactive.case_tag.parse t with
    | some t :=
      [h "li" [key "_case"] $ [h "span" [cn "goal-case b"] ["case"]] ++
        (t.case_names.bind $ λ n, [" ", n])]
    | none := []
    end,
  lcs ← local_context,
  lcs ← list.mfilter (filter_local ft) lcs,
  lcs ← to_local_collection [] lcs,
  -- Display the local variables; grouping together locals of the same type.
  lchs ← lcs.mmap (λ lc, do
    lh ← local_c lc,
    ns ← lc.locals.mmap (λ n, do
      let var_color : attr γ := if n ∈ is'
      then attr.style [("color", "#ff0073")]  -- "goal-hyp-inst"
      else attr.style [("color", "#ffcc00")], -- "goal-hyp"
        pure $ h "span" [cn "goal-hyp b pr2", var_color] [html.of_name $ expr.local_pp_name n]),
    pure $ h "li" [key lc.key] (ns ++ [": ", h "span" [cn "goal-hyp-type"] [lh]])),
  t_comp ← target_c g,
  pure $ h "ul" [key g.hash, className "list pl0 font-code"] $ case_tag ++ lchs ++ [
    h "li" [key u_n] [
      h "span" [cn "goal-vdash b"] ["⊢ "],
      t_comp
  ]]

/-- Component that displays all goals, together with the `$n goals` message. -/
meta def tactic_view_component {γ} (local_c : tc local_collection γ) (target_c : tc expr γ) : tc unit γ :=
tc.mk_simple
  (tactic_view_action γ)
  (filter_type)
  (λ _, pure $ filter_type.none)
  (λ ⟨⟩ ft a, match a with
              | (tactic_view_action.out a) := pure (ft, some a)
              | (tactic_view_action.filter ft) := pure (ft, none)
              end)
  (λ ⟨⟩ ft, do
    gs ← get_goals,
    hs ← gs.mmap (λ g, do set_goals [g], flip tc.to_html ft $ tactic_view_goal local_c target_c),
    set_goals gs,
    let goal_message :=
      if gs.length = 0 then
        "goals accomplished"
      else if gs.length = 1 then
        "1 goal"
      else
        to_string gs.length ++ " goals",
    let goal_message : html γ := h "strong" [cn "goal-goals"] [goal_message],
    let goals : html γ := h "ul" [className "list pl0"]
        $ list.map_with_index (λ i x,
          h "li" [className $ "lh-copy mt2", key i] [x])
        $ (goal_message :: hs),
    pure [
      h "div" [className "fr"] [html.of_component ft $ component.map_action tactic_view_action.filter filter_component],
      html.map_action tactic_view_action.out goals
    ])

meta def tactic_render : tc unit empty :=
component.ignore_action $ tactic_view_component show_local_collection_component show_type_component

meta def tactic_state_widget : component tactic_state empty :=
tc.to_component tactic_render

end inst_widget

attribute [vm_override inst_widget.tactic_state_widget] widget.tactic_state_widget

example : true :=
begin
  haveI an_instance : has_add ℕ := sorry,
  have not_instance : has_add ℕ := sorry,
  have another_not_instance : has_mul ℕ := sorry,
  have yet_another : has_add ℕ := sorry,
  trivial,
end

image.png

[Yaël Dillies]

Italics, maybe? image.png

[Eric Wieser]

I'd maybe go for a more muted color

[Eric Wieser]

Since you shouldn't have to know the name of things in the instance cache anyway

[Yaël Dillies]

Note, the colors are surprisingly strong on the first one for a reason that escapes me.

[Eric Wieser]

My guess would be that they're the dark mode colors being used in white mode

[Yaël Dillies]

Ah! Yes exactly.

[Yaël Dillies]

Muted colors. image.png

[Eric Wieser]

Possibly coloring things that aren't in the instance cache but are @[class] would be a good idea too / instead

[Eric Wieser]

Eric Wieser said:

I'd maybe go for a more muted color

I meant make the ones in the cache be more muted than the ones not in the cache

[Yaël Dillies]

Rob suggested this as well. It's a choice to make.

[Yaël Dillies]

Like this? Uploading image.png…

[Eric Wieser]

(Zulip's behavior of allowing you to send the loading text is wonderful, isn't it...)

[Eric Wieser]

Another good option might just be a red dotted / squiggly line underneath the non-instance cache ones, with a title="not in the instance cache" attribute

[Anne Baanen]

Underlines sound like a good idea

[Eric Wieser]

Or maybe not red since it's not an error, but some kind of underline, probably not in yellow

[Eric Rodriguez]

I'd definitely suggest highlighting what's not in the cache instead of what is

[Yaël Dillies]

/poll What should we separate visually?
Instances vs non instances
Typeclass assumptions that are not instances vs the rest
Instances vs typeclass assumptions that are not instances vs the rest
Typeclass assumptions from the rest

[Yaël Dillies]

/poll How should we separate it?
Different color
Italic
Bold
Underline

[Eric Wieser]

By "instances" you mean "in the instance cache" or "of a type tagged with @[class]"?

[Yaël Dillies]

In the instance cache. as opposed to "typeclass assumptions".

[Eric Wieser]

Are you considering either of [n : nat] and {s : setoid X} a typeclass assumption?

[Eric Wieser]

(I would hope the answer is just the latter)

[Yaël Dillies]

Just the latter.

[Yaël Dillies]

Regarding the first poll, it might be possible to make variable names clickable or hoverable in order to show a bubble of the form "This is a class but not an instance" or something along those lines...

[Mario Carneiro]

is "frozen local instance" being distinguished here? (i.e. something that would make revert fail)

[Yaël Dillies]

If you explain me what it is, I would be happy to try! My code above only knows about the instance cache.

[Mario Carneiro]

the frozen local instances generally coincide with the ones in the cache

[Yaël Dillies]

Okay, that was my mental model. What are the exceptions?

[Mario Carneiro]

when you say unfreeze_local_instances

[Mario Carneiro]

the tactic frozen_local_instances returns the list of frozen local instances

[Yaël Dillies]

This is not supposed to be used by the end user, right?

[Eric Wieser]

@Yaël Dillies, can you make a draft PR of this against lean to make it clear which bits of your code are copy-pasted to make vm_override work, and which bits are changed? My impression is that we want this in lean core eventually, and that vm_override is just a neat tool for protyping

[Yaël Dillies]

Yes absolutely! The twist is that to avoid harcoding the style I will need to first get a PR merged to vscode-lean to add the missing style attributes to the CSS file, unless you see another way out.

[Eric Wieser]

I think for the purpose of a draft PR that can be dealt with later (either by assuming the PR exists, or by inlining the styles for now)

[Mario Carneiro]

Yaël Dillies said:

This is not supposed to be used by the end user, right?

No, but it is user-visible and I assumed that's why you want to color these things in the first place

[Mario Carneiro]

I assume you are trying to make it possible for the user to predict in advance that a typeclass in the context won't be used or something like that

[Mario Carneiro]

There are basically two user-facing issues that would be relevant here: (1) a typeclass in the context is not going to be used because it was added after the cache was frozen, (2) a typeclass in the context cannot be reverted or rewritten because it is frozen

[Mario Carneiro]

Here's a suggested scheme:

• If the instance cache is not frozen, all instances are reddish
• If the instance cache is frozen, frozen instances are bluish and unfrozen instances are italic

[Mario Carneiro]

so bluish means you can't revert it and italic means you forgot a haveI

[Mario Carneiro]

reddish means you are in the middle of a unfreezingI, this should be rare

[Gabriel Ebner]

I would only color "unavailable" type classes instances in red (= local instances are frozen & the instance is not part of the frozen ones), because that's when you need to take action.

[Gabriel Ebner]

@Yaël Dillies You need to do the changes in mathlib: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive_expr.lean Feel free to sync that file to core though if you want.

[Eric Wieser]

I think showing somehow that the cache is frozen/unfrozen is good too, otherwise there's no observable effect of unfreezing the instance cache

[Yaël Dillies]

Mario's dream:
Before unfreezing
Within an unfreezingI

[Eric Wieser]

One other thought: it's quite common to paste goals into Zulip /discord where the colors are lost

[Eric Wieser]

Should we use a symbol instead / as well?

[Anne Baanen]

Also symbols might be useful for people who are colourblind...

[Yaël Dillies]

Agreed! I paid attention to the colors scheme, because I am myself colorblind. But I am only one flavor of colorblind so it would be good to get other people's opinions.

[Yaël Dillies]

#15959

[Yaël Dillies]

This is still not merged, if people want to suggest ways to show the instance cache in the infoview on #15959.