Zulip Chat Archive

Stream: general

Topic: Instance cache in the infoview


Yaël Dillies (Jul 31 2022 at 09:57):

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 (Jul 31 2022 at 09:58):

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 (Jul 31 2022 at 10:41):

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 (Jul 31 2022 at 11:11):

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

Eric Wieser (Jul 31 2022 at 11:14):

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 (Jul 31 2022 at 11:25):

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 (Jul 31 2022 at 12:16):

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 (Jul 31 2022 at 13:21):

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

Yaël Dillies (Jul 31 2022 at 13:25):

Does that mean haveI resets the instance cache?

Yaël Dillies (Jul 31 2022 at 13:42):

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

Yaël Dillies (Jul 31 2022 at 13:44):

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 (Jul 31 2022 at 13:46):

You can override from user code, even outside mathlib.

Patrick Massot (Jul 31 2022 at 13:48):

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 (Jul 31 2022 at 13:49):

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

Patrick Massot (Jul 31 2022 at 13:51):

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 (Aug 08 2022 at 12:59):

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 (Aug 08 2022 at 13:03):

Italics, maybe? image.png

Eric Wieser (Aug 08 2022 at 13:04):

I'd maybe go for a more muted color

Eric Wieser (Aug 08 2022 at 13:04):

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

Yaël Dillies (Aug 08 2022 at 13:04):

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

Eric Wieser (Aug 08 2022 at 13:04):

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

Yaël Dillies (Aug 08 2022 at 13:05):

Ah! Yes exactly.

Yaël Dillies (Aug 08 2022 at 13:06):

Muted colors. image.png

Eric Wieser (Aug 08 2022 at 13:06):

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

Eric Wieser (Aug 08 2022 at 13:07):

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 (Aug 08 2022 at 13:08):

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

Yaël Dillies (Aug 08 2022 at 13:08):

Like this? Uploading image.png…

Eric Wieser (Aug 08 2022 at 13:09):

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

Eric Wieser (Aug 08 2022 at 13:10):

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 (Aug 08 2022 at 13:11):

Underlines sound like a good idea

Eric Wieser (Aug 08 2022 at 13:11):

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

Eric Rodriguez (Aug 08 2022 at 13:44):

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

Yaël Dillies (Aug 08 2022 at 18:12):

/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 (Aug 08 2022 at 18:13):

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

Eric Wieser (Aug 08 2022 at 18:19):

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

Yaël Dillies (Aug 08 2022 at 18:32):

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

Eric Wieser (Aug 08 2022 at 18:36):

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

Eric Wieser (Aug 08 2022 at 18:36):

(I would hope the answer is just the latter)

Yaël Dillies (Aug 08 2022 at 18:37):

Just the latter.

Yaël Dillies (Aug 08 2022 at 19:17):

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 (Aug 08 2022 at 19:18):

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

Yaël Dillies (Aug 08 2022 at 19:19):

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

Mario Carneiro (Aug 08 2022 at 19:20):

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

Yaël Dillies (Aug 08 2022 at 19:21):

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

Mario Carneiro (Aug 08 2022 at 19:22):

when you say unfreeze_local_instances

Mario Carneiro (Aug 08 2022 at 19:22):

the tactic frozen_local_instances returns the list of frozen local instances

Yaël Dillies (Aug 08 2022 at 19:25):

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

Eric Wieser (Aug 08 2022 at 19:32):

@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 (Aug 08 2022 at 19:33):

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 (Aug 08 2022 at 19:35):

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 (Aug 08 2022 at 19:39):

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 (Aug 08 2022 at 19:40):

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 (Aug 08 2022 at 19:42):

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 (Aug 08 2022 at 19:52):

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 (Aug 08 2022 at 19:53):

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

Mario Carneiro (Aug 08 2022 at 19:53):

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

Gabriel Ebner (Aug 08 2022 at 21:01):

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 (Aug 08 2022 at 21:02):

@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 (Aug 08 2022 at 21:24):

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 (Aug 09 2022 at 07:59):

Mario's dream:
Before unfreezing
Within an unfreezingI

Eric Wieser (Aug 09 2022 at 10:53):

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

Eric Wieser (Aug 09 2022 at 10:54):

Should we use a symbol instead / as well?

Anne Baanen (Aug 09 2022 at 11:21):

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

Yaël Dillies (Aug 09 2022 at 11:24):

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 (Aug 09 2022 at 13:26):

#15959

Yaël Dillies (Aug 24 2022 at 19:14):

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


Last updated: Dec 20 2023 at 11:08 UTC