MetaM example : Lean Server Crashed stack overflow

Stream: lean4

[Shreyas Srinivas]

I was typing out the example on page 20 of the Metaprogramming in Lean 4 pdf. It shows how assignment to and instantiation of metavariables works.

I got as far as the line :mvar₁.mvarId!.assign (.app mvar₁ mvar₂). Until the end of this line everything worked file. However, as soon as I finish typing the next line which just says printMVars, the lean server crashes and vscode reports

Lean server printed an error:

Stack overflow detected. Aborting.

[Shreyas Srinivas]

So for good measure, I added the lines assigning all three meta vars mvar1, mvar2, mvar3 and the assigns are not a problem.

[Shreyas Srinivas]

but as soon as printMVars is added, the crash happens.

[Shreyas Srinivas]

For reference here's printMVars :

...
let printMVars : MetaM Unit := do
    IO.println s!"meta 1 : {← instantiateMVars mvar1}"
    IO.println s!"meta 2 : {← instantiateMVars mvar2}"
    IO.println s!"meta 3 : {← instantiateMVars mvar3}"
...

[Max Nowak 🐉]

You are assigning an mvar to itself (mvar₁ := ... mvar₁ ...), I think that's not supposed to be like that?

[Shreyas Srinivas]

Max Nowak 🐺 said:

You are assigning an mvar to itself (mvar₁ := ... mvar₁ ...), I think that's not supposed to be like that?

thanks. That makes sense. The error was indeed caused by the assignment to mvar1