Open xinhjBrant opened 1 month ago
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:
leanprover/lean4:v4.6.0-rc1
2ab7948163863ee222891653ac98941fe4f20e87
64528268b3c2cf578639bc479828882a9ecd3a82
Hi, I encountered an exception while trying to extract all tactic applications in Mathlib:
The error occurs in the following Mathlib files:
Environment details:
leanprover/lean4:v4.6.0-rc1
2ab7948163863ee222891653ac98941fe4f20e87
64528268b3c2cf578639bc479828882a9ecd3a82