chore: update stage0

stage0/src/Init/Lean/Elab/Tactic/Basic.lean

@@ -136,19 +136,24 @@ adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ct
 
 partial def evalTactic : Syntax → TacticM Unit
 | stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
-  | Syntax.node k args => do
+  | Syntax.node k args =>
+    if k == nullKind then
+      -- list of tactics separated by `;` => evaluate in order
+      -- Syntax quotations can return multiple ones
+      stx.forSepArgsM evalTactic
+    else do
     trace `Elab.step stx $ fun _ => stx;
-    s ← get;
-    let table := (tacticElabAttribute.ext.getState s.env).table;
-    let k := stx.getKind;
-    match table.find? k with
-    | some elabFns => evalTacticUsing s stx elabFns
-      | none         => do
-        scp ← getCurrMacroScope;
-        env ← getEnv;
-        match expandMacro env stx scp with
-        | some stx' => withMacroExpansion stx $ evalTactic stx'
-        | none      => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
+      s ← get;
+      let table := (tacticElabAttribute.ext.getState s.env).table;
+      let k := stx.getKind;
+      match table.find? k with
+      | some elabFns => evalTacticUsing s stx elabFns
+        | none         => do
+          scp ← getCurrMacroScope;
+          env ← getEnv;
+          match expandMacro env stx scp with
+          | some stx' => withMacroExpansion stx $ evalTactic stx'
+          | none      => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
   | _ => throwError stx "unexpected command"
 
 @[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TacticM α) : TacticM α :=

stage0/src/Init/Lean/Parser/Parser.lean

@@ -441,7 +441,8 @@ fun a c s =>
 { info := p.info,
   fn   := many1Fn p.fn unboxSingleton }
 
-@[specialize] private partial def sepByFnAux {k : ParserKind} (p : ParserFn k) (sep : ParserFn k) (allowTrailingSep : Bool) (iniSz : Nat) : Bool → ParserFn k
+@[specialize] private partial def sepByFnAux {k : ParserKind} (p : ParserFn k) (sep : ParserFn k) (allowTrailingSep : Bool)
+    (iniSz : Nat) (unboxSingleton : Bool)  : Bool → ParserFn k
 | pOpt, a, c, s =>
   let sz  := s.stackSize;
   let pos := s.pos;
@@ -449,7 +450,10 @@ fun a c s =>
   if s.hasError then
     if pOpt then
       let s := s.restore sz pos;
-      s.mkNode nullKind iniSz
+      if s.stackSize - iniSz == 2 && unboxSingleton then
+        s.popSyntax
+      else
+        s.mkNode nullKind iniSz
     else
       -- append `Syntax.missing` to make clear that List is incomplete
       let s := s.pushSyntax Syntax.missing;
@@ -460,19 +464,22 @@ fun a c s =>
     let s   := sep a c s;
     if s.hasError then
       let s := s.restore sz pos;
-      s.mkNode nullKind iniSz
+      if s.stackSize - iniSz == 1 && unboxSingleton then
+        s
+      else
+        s.mkNode nullKind iniSz
     else
       sepByFnAux allowTrailingSep a c s
 
 @[specialize] def sepByFn {k : ParserKind} (allowTrailingSep : Bool) (p : ParserFn k) (sep : ParserFn k) : ParserFn k
 | a, c, s =>
   let iniSz := s.stackSize;
-  sepByFnAux p sep allowTrailingSep iniSz true a c s
+  sepByFnAux p sep allowTrailingSep iniSz false true a c s
 
-@[specialize] def sepBy1Fn {k : ParserKind} (allowTrailingSep : Bool) (p : ParserFn k) (sep : ParserFn k) : ParserFn k
+@[specialize] def sepBy1Fn {k : ParserKind} (allowTrailingSep : Bool) (p : ParserFn k) (sep : ParserFn k) (unboxSingleton : Bool) : ParserFn k
 | a, c, s =>
   let iniSz := s.stackSize;
-  sepByFnAux p sep allowTrailingSep iniSz false a c s
+  sepByFnAux p sep allowTrailingSep iniSz unboxSingleton false a c s
 
 @[noinline] def sepByInfo (p sep : ParserInfo) : ParserInfo :=
 { collectTokens := p.collectTokens ∘ sep.collectTokens,
@@ -487,9 +494,9 @@ fun a c s =>
 { info := sepByInfo p.info sep.info,
   fn   := sepByFn allowTrailingSep p.fn sep.fn }
 
-@[inline] def sepBy1 {k : ParserKind} (p sep : Parser k) (allowTrailingSep : Bool := false) : Parser k :=
+@[inline] def sepBy1 {k : ParserKind} (p sep : Parser k) (allowTrailingSep : Bool := false) (unboxSingleton := false) : Parser k :=
 { info := sepBy1Info p.info sep.info,
-  fn   := sepBy1Fn allowTrailingSep p.fn sep.fn }
+  fn   := sepBy1Fn allowTrailingSep p.fn sep.fn unboxSingleton }
 
 @[specialize] partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : BasicParserFn
 | c, s =>

stage0/src/Init/Lean/Parser/Tactic.lean

@@ -49,7 +49,8 @@ end Tactic
 namespace Term
 
 @[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
-@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> tacticParser >> ")"
+-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
+@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
 
 end Term