chore: update stage0

stage0/src/Lean/Parser/Basic.lean

@@ -1420,8 +1420,11 @@ fun c s =>
 @[inline] def eoi : Parser :=
 { fn := eoiFn }
 
-@[inline] def many1Indent (p : Parser) (errorMsg : String) : Parser :=
-withPosition $ many1 (checkColGe errorMsg >> p)
+@[inline] def many1Indent (p : Parser) : Parser :=
+withPosition $ many1 (checkColGe "irrelevant" >> p)
+
+@[inline] def manyIndent (p : Parser) : Parser :=
+withPosition $ many (checkColGe "irrelevant" >> p)
 
 open Std (RBMap RBMap.empty)
 

stage0/src/Lean/Parser/Do.lean

@@ -21,25 +21,7 @@ namespace Term
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 
-def doSeqIndent :=
-withPosition $ many1 $
-  checkColGe "do-elements must be indented"
-  /-
-    We considered using `withPosition doElemParser` here instead of just `doElemParser` to make sure
-    the applications must be indented with respect to the current do-element.
-    Example:
-    ```
-    def foo : IO Nat := do
-    IO.println "hello";
-       List.forM xs
-     (fun x => IO.println x)
-    ```
-    The argument `(fun x => IO.println x)` is considered part of the application since it is
-    indented with respect to the first action.
-  -/
-  >> doElemParser
-  >> optional "; "
-
+def doSeqIndent    := many1Indent $ doElemParser >> optional "; "
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 

stage0/src/Lean/Parser/Tactic.lean

@@ -25,11 +25,11 @@ fun c s =>
 
 def ident' : Parser := ident <|> underscore
 
-@[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> many (termParser maxPrec)
-@[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> many ident'
-@[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1 ident
-@[builtinTacticParser] def «clear»      := parser! nonReservedSymbol "clear " >> many1 ident
-@[builtinTacticParser] def «subst»      := parser! nonReservedSymbol "subst " >> many1 ident
+@[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> manyIndent (termParser maxPrec)
+@[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> manyIndent ident'
+@[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1Indent ident
+@[builtinTacticParser] def «clear»      := parser! nonReservedSymbol "clear " >> many1Indent ident
+@[builtinTacticParser] def «subst»      := parser! nonReservedSymbol "subst " >> many1Indent ident
 @[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
 @[builtinTacticParser] def «apply»      := parser! nonReservedSymbol "apply " >> termParser
 @[builtinTacticParser] def «exact»      := parser! nonReservedSymbol "exact " >> termParser

stage0/src/Lean/Parser/Term.lean

@@ -22,8 +22,7 @@ categoryParser `tactic rbp
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
-parser! withPosition $
-  sepBy1 tacticParser (try ("; " >>  checkColGe "tatic must be indented"))
+parser! many1Indent $ tacticParser >> optional "; "
 def tacticSeqBracketed : Parser :=
 parser! "{" >> sepBy tacticParser "; " true >> "}"
 def tacticSeq :=

stage0/stdlib/Lean/Elab/Binders.c

@@ -14688,7 +14688,7 @@ lean_object* _init_l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("seq");
+x_1 = lean_mk_string("seq1");
 return x_1;
 }
 }

stage0/stdlib/Lean/Elab/BuiltinNotation.c

@@ -229,7 +229,6 @@ lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__7;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandHave(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__1;
 lean_object* l___regBuiltin_Lean_Elab_Term_elabPanic(lean_object*);
-extern lean_object* l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__6;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandGT___closed__3;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandLE(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_expandBEq___closed__1;
@@ -253,6 +252,7 @@ lean_object* l_Lean_Elab_Term_elabAnonymousCtor(lean_object*, lean_object*, lean
 lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandIff___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_expandseq___closed__4;
 lean_object* l_Lean_Elab_Term_elabNativeRefl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandEmptyC___closed__3;
 lean_object* l_Lean_Elab_Term_expandShow___closed__7;
@@ -9402,9 +9402,17 @@ return x_3;
 lean_object* _init_l_Lean_Elab_Term_expandseq___closed__3() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_mk_string("seq");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_expandseq___closed__4() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_Term_expandseq___closed__2;
-x_2 = l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__6;
+x_2 = l_Lean_Elab_Term_expandseq___closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -9413,7 +9421,7 @@ lean_object* l_Lean_Elab_Term_expandseq(lean_object* x_1, lean_object* x_2, lean
 _start:
 {
 lean_object* x_4; lean_object* x_5; 
-x_4 = l_Lean_Elab_Term_expandseq___closed__3;
+x_4 = l_Lean_Elab_Term_expandseq___closed__4;
 x_5 = l_Lean_Elab_Term_expandInfixOp(x_4, x_1, x_2, x_3);
 return x_5;
 }
@@ -9433,7 +9441,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_mkAppStx___closed__6;
-x_2 = l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__6;
+x_2 = l_Lean_Elab_Term_expandseq___closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -12457,6 +12465,8 @@ l_Lean_Elab_Term_expandseq___closed__2 = _init_l_Lean_Elab_Term_expandseq___clos
 lean_mark_persistent(l_Lean_Elab_Term_expandseq___closed__2);
 l_Lean_Elab_Term_expandseq___closed__3 = _init_l_Lean_Elab_Term_expandseq___closed__3();
 lean_mark_persistent(l_Lean_Elab_Term_expandseq___closed__3);
+l_Lean_Elab_Term_expandseq___closed__4 = _init_l_Lean_Elab_Term_expandseq___closed__4();
+lean_mark_persistent(l_Lean_Elab_Term_expandseq___closed__4);
 l___regBuiltin_Lean_Elab_Term_expandseq___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandseq___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_expandseq___closed__1);
 l___regBuiltin_Lean_Elab_Term_expandseq___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_expandseq___closed__2();

stage0/stdlib/Lean/Elab/Tactic/Basic.c

@@ -286,7 +286,6 @@ lean_object* l_Lean_Meta_revert(lean_object*, lean_object*, uint8_t, lean_object
 lean_object* l_Lean_Elab_Tactic_evalChoice___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_liftMetaMAtMain___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern size_t l_Std_PersistentHashMap_insertAux___main___rarg___closed__2;
-lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2;
 lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalParen___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalSeq1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -319,7 +318,6 @@ lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Elab_Tactic_evalTactic___main__
 lean_object* l_Lean_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_Lean_Ref;
 lean_object* l_Lean_Elab_Tactic_evalFailIfSuccess___closed__2;
-lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3;
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalTactic___main___spec__8___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__1;
 lean_object* l_List_findM_x3f___main___at___private_Lean_Elab_Tactic_Basic_6__findTag_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -7757,24 +7755,6 @@ lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("seq1");
-return x_1;
-}
-}
-lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
-x_2 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3() {
-_start:
-{
-lean_object* x_1; 
 x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalSeq1___boxed), 10, 0);
 return x_1;
 }
@@ -7784,8 +7764,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
-x_3 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2;
-x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3;
+x_3 = l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__7;
+x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -15156,10 +15136,6 @@ l_Lean_Elab_Tactic_focus___rarg___closed__1 = _init_l_Lean_Elab_Tactic_focus___r
 lean_mark_persistent(l_Lean_Elab_Tactic_focus___rarg___closed__1);
 l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1);
-l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2);
-l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3);
 res = l___regBuiltin_Lean_Elab_Tactic_evalSeq1(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);

stage0/stdlib/Lean/Parser/Command.c

@@ -803,7 +803,6 @@ lean_object* l_Lean_Parser_Command_commentBody_parenthesizer___rarg(lean_object*
 lean_object* l___regBuiltin_Lean_Parser_Command_mutual_parenthesizer(lean_object*);
 lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__15;
 lean_object* l_Lean_Parser_Command_exit_parenthesizer___closed__1;
-extern lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__6;
 lean_object* l_Lean_Parser_Command_example_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Command_classInductive___closed__5;
 lean_object* l_Lean_Parser_Command_open___closed__2;
@@ -1878,6 +1877,7 @@ lean_object* l_Lean_Parser_Command_init__quot___elambda__1___closed__6;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_mutual(lean_object*);
 lean_object* l_Lean_Parser_Command_openSimple___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_openOnly___closed__1;
+extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Command_openRenamingItem___closed__1;
 lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_optDeclSig_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -42142,7 +42142,7 @@ lean_object* _init_l_Lean_Parser_Command_attribute_parenthesizer___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_structInst_parenthesizer___closed__6;
+x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__2;
 x_2 = l_Lean_Parser_Command_attribute_parenthesizer___closed__4;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
 lean_closure_set(x_3, 0, x_1);

stage0/stdlib/Lean/Parser/Module.c

@@ -118,7 +118,6 @@ lean_object* l_Lean_Parser_Module_header___elambda__1___closed__2;
 lean_object* lean_array_fget(lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_testModuleParser___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__6;
 lean_object* l_Lean_Parser_parseModuleAux___main___closed__2;
 lean_object* l_Lean_Parser_Module_header___closed__2;
 lean_object* l_Lean_Parser_Module_import___elambda__1___closed__8;
@@ -238,6 +237,7 @@ lean_object* l_Lean_Parser_Module_module_parenthesizer___closed__3;
 lean_object* l_IO_FS_Handle_readToEndAux___main___at_IO_Process_output___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_header_formatter___closed__3;
 lean_object* l_Lean_Parser_Module_prelude___elambda__1(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Module_import___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Module_header_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
@@ -2457,7 +2457,7 @@ lean_object* _init_l_Lean_Parser_Module_import_parenthesizer___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_structInst_parenthesizer___closed__6;
+x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__2;
 x_2 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
 lean_closure_set(x_3, 0, x_1);