InfoView completely blank

Stream: general

[Moritz R]

Since updating to v4.28-rc1, every few seconds in my project the infoview goes blank on me. Reopening it works, but it fails soon again.
image.png

[Moritz R]

Holdup, i have some custom css in the Lean4 Infoview: Style setting, maybe that broke. Let me test that

[Moritz R]

It is not the css

[Moritz R]

:(

[Marc Huisinga]

Does the developer console contain any errors? 'Developer: Toggle Developer Tools'

[Moritz R]

No new messages from the point where it went grey

[Moritz R]

These are the messages i get (which i think are probably unrelated) before. Then i waited ~40seconds and the infoview went gray without any new messages
image.png

[Marc Huisinga]

Can you confirm that the issue does not occur now if you go back to a commit of your project before v4.28.0-rc1?

[Moritz R]

i will downgrade my version again and update you

[Moritz R]

I was using 4.27.0 before

[Moritz R]

i wanted to upgrade to something, since 4.27 broke the autocomplete suggestions with modules(always completing to
Meta. ......... .Tactic.assumption instead of assumption)

[Moritz R]

Which got fixed at some point

[Moritz R]

Oh heck no

[Moritz R]

Its still happening

[Moritz R]

i also remember that i had no issues yesterday before sleep, when i was already on 4.28-rc1

[Marc Huisinga]

Did you update VS Code recently by any chance? :-)

[Moritz R]

so its probably not the lean version

[Moritz R]

Not actively at least

[Moritz R]

image.png
Whatever this menu is, it shows that my system at least didn't do an update this night

[Moritz R]

image.png
And this suggests, im on a 1 week old vscode?

[Marc Huisinga]

What's your Lean VS Code extension version? Also, does the issue still occur if you disable all non-Lean extensions and fully restart VS Code?

[Moritz R]

image.png
It's 1 month? old

[Moritz R]

And yes, disabling all the extensions (except "Even Better TOML" which the Lean 4 extension seems to depend on) still produces the gray screen (after a restart of vscode)

[Moritz R]

hmm maybe it has to do with trace messages

[Moritz R]

i was debugging a looping simp_all and had

set_option trace.Meta.Tactic.simp.unify true
set_option diagnostics true

active.
Now that i have commented them out, it has not yet gone gray yet

[Moritz R]

Aha!
I need the looping simp_all call and tracing enabled. Then it happens

[Moritz R]

I will try to reduce

[Moritz R]

image.png

[Moritz R]

Any suggestions on how to create such a high succeeded count with a loop in simp?

[Moritz R]

My reduced examples always stop at max : 167, because they stop via max recursion depth, not via timeout at whnf

[Moritz R]

Enabling more traces also helps it go faster gray in my application:

set_option trace.Meta.Tactic.simp.unify true
set_option trace.Meta.Tactic.simp.rewrite true
set_option diagnostics true

[Moritz R]

I think one just needs to generate an absurd amount of failed to unify or other messages

[Moritz R]

I could recreate it

[Moritz R]

@Marc Huisinga

[Moritz R]

set_option maxRecDepth 20000
set_option trace.Meta.Tactic.simp.unify true
set_option trace.Meta.Tactic.simp.rewrite true
set_option diagnostics true

opaque bar : Nat → Type
opaque foo : Nat → Type

@[simp]
axiom bar_eq_foo : bar x = foo x

@[simp]
axiom foo_eq_bar : foo x = bar x






@[simp 100000]
axiom foo_eq_bar2 : foo (x + 1) = bar x

@[simp 100000]
axiom foo_eq_bar3 : foo (x + 2) = bar x

@[simp 100000]
axiom foo_eq_bar4 : foo (x + 3) = bar x

@[simp 100000]
axiom foo_eq_bar5 : foo (x + 4) = bar x





@[simp 100000]
axiom bar_eq_foo2 : bar (x + 1) = foo x

@[simp 100000]
axiom bar_eq_foo3 : bar (x + 2) = foo x

@[simp 100000]
axiom bar_eq_foo4 : bar (x + 3) = foo x

@[simp 100000]
axiom bar_eq_foo5 : bar (x + 4) = foo x

example : foo 5 = foo 7 := by
  simp_all  -- Loops: foo 5 → bar 5 → foo 5 → ...

[Moritz R]

I know im setting recursion depth and diagnostics threshold unreasonably high, but it creates the gray screen error i was getting in my project where i didn't touch any of these settings

[Moritz R]

It doesn't recreate on Lean 4 Web tough

[Moritz R]

So it might have to do with machine specs

[Moritz R]

Can you recreate on your machine?

[Moritz R]

You need to put the cursor after the simp_all and wait a bit (<= 3 minutes for me i think)

[Moritz R]

Edit: The diagnostics threshold doesn't need to be changed, i deleted that line

[Moritz R]

The idea of the example is to create a huge amount of messages, by having the rewrite loop of
bar x -> foo x -> bar x -> foo x ...
so that set_option trace.Meta.Tactic.simp.rewrite true will generate a message for each rewrite.
In between we generate even more messages by having some high priority simp lemmas, that will fail the unification (and set_option trace.Meta.Tactic.simp.unify true will generate a message from this)

[Moritz R]

If it doesn't reproduce for you, try adding even more unification-fail-lemmas in each step.