Bugs for metavariable '?[anonymous]' when setting "allTactics" as true

[xinhjBrant]

Hi, I encountered an exception while trying to extract all tactic applications in Mathlib:

PANIC at List.head! Init.Data.List.BasicAux:32:12: empty list
backtrace:
[././.lake/packages/REPL/.lake/build/bin/repl](lean_panic_fn+0x9e)[0x556114129a8e]
[././.lake/packages/REPL/.lake/build/bin/repl](l_REPL_ProofSnapshot_create___lambda__2+0xf5)[0x556110f52b15]
[././.lake/packages/REPL/.lake/build/bin/repl](lean_apply_5+0x3e9)[0x556114137da9]
[././.lake/packages/REPL/.lake/build/bin/repl](l_Lean_Elab_ContextInfo_runMetaM___rarg+0x3d3)[0x556111363ed3]
[././.lake/packages/REPL/.lake/build/bin/repl](l_List_mapM_loop___at_REPL_runCommand___spec__6+0x216)[0x556110f14576]
[././.lake/packages/REPL/.lake/build/bin/repl](l_REPL_runCommand___lambda__2+0x68c)[0x556110f171cc]
[././.lake/packages/REPL/.lake/build/bin/repl](l_REPL_runCommand___lambda__3+0x26d)[0x556110f17d7d]
[././.lake/packages/REPL/.lake/build/bin/repl](l_repl_loop___lambda__1+0x1f1)[0x556110f1b111]
[././.lake/packages/REPL/.lake/build/bin/repl](l_repl+0x1a)[0x556110f1d6da]
[././.lake/packages/REPL/.lake/build/bin/repl](+0xbe8773)[0x556110f1e773]
[/lib/x86_64-linux-gnu/libc.so.6](x86_64-linux-gnu/libc.so.6)(+0x2724a)[0x7ff83fb6924a]
[/lib/x86_64-linux-gnu/libc.so.6](x86_64-linux-gnu/libc.so.6)(__libc_start_main+0x85)[0x7ff83fb69305]
[././.lake/packages/REPL/.lake/build/bin/repl](_start+0x2e)[0x556110f024ee]
uncaught exception: unknown metavariable '?[anonymous]'

The error occurs in the following Mathlib files:

MathlibExtras/Rewrites.lean
Mathlib/Init/Data/Nat/Lemmas.lean
Mathlib/Tactic/Widget/CommDiag.lean
Mathlib/CategoryTheory/Products/Basic.lean
Mathlib/CategoryTheory/Comma/Over.lean
Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
Mathlib/Algebra/FreeAlgebra.lean
Mathlib/Algebra/Ring/Defs.lean
Mathlib/Data/Sym/Sym2.lean
Mathlib/Data/Real/Basic.lean
Mathlib/Data/Ordmap/Ordset.lean
Mathlib/NumberTheory/ClassNumber/Finite.lean
Mathlib/Computability/TMToPartrec.lean
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Environment details:

• Lean version: leanprover/lean4:v4.6.0-rc1
• REPL commit: 2ab7948163863ee222891653ac98941fe4f20e87
• Mathlib commit: 64528268b3c2cf578639bc479828882a9ecd3a82

[peter-peng-w]

Same issue here when using Lean 4.7.0, any suggestions?

[xinhjBrant]

Same issue here when using Lean 4.7.0, any suggestions?

I solved this in my branch.