Huajian Xin

[BUG]: `LowLevelZeroOptimizer` gets stuck in `all_reduce` when executing `check_overflow`

1

### 🐛 Describe the bug I'm having a problem running the code of the ColossalChat: the [`strategy.optimizer_step`](https://github.com/hpcaitech/ColossalAI/blob/main/applications/Chat/coati/trainer/sft.py#L67) gets stuck, and specifically, it's stuck in the execution of [`torch.all_reduce`](https://github.com/hpcaitech/ColossalAI/blob/main/colossalai/amp/naive_amp/mixed_precision_mixin/fp16.py#L62). I'm running...

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

2

Hi, I encountered an exception while trying to extract all tactic applications in Mathlib: ```bash 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]...