From dc01e79388c84756edea2da57b431e66e71ae4e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Dec 2020 21:26:15 -0800
Subject: [PATCH] chore: update stage0

---
 stage0/src/Init/Notation.lean    | 11 ++++----
 stage0/src/Lean/Elab/Syntax.lean |  4 +--
 stage0/stdlib/Lean/Elab/Syntax.c | 45 ++++++++++++++++----------------
 3 files changed, 31 insertions(+), 29 deletions(-)

diff --git a/stage0/src/Init/Notation.lean b/stage0/src/Init/Notation.lean
index 1f429e997d..8672014928 100644
--- a/stage0/src/Init/Notation.lean
+++ b/stage0/src/Init/Notation.lean
@@ -195,15 +195,16 @@ syntax[changeWith] "change " term " with " term (location)? : tactic
 syntax rwRule    := ("←" <|> "<-")? term
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
+-- TODO: fix 100000 priorities
 syntax[rewrite] "rewrite " rwRule (location)? : tactic
-syntax[rewriteSeq, 1] "rewrite " rwRuleSeq (location)? : tactic
+syntax[rewriteSeq, 100000] "rewrite " rwRuleSeq (location)? : tactic
 syntax[erewrite] "erewrite " rwRule (location)? : tactic
-syntax[erewriteSeq, 1] "erewrite " rwRuleSeq (location)? : tactic
+syntax[erewriteSeq, 100000] "erewrite " rwRuleSeq (location)? : tactic
 
 syntax[rw] "rw " rwRule (location)? : tactic
-syntax[rwSeq, 1] "rw " rwRuleSeq (location)? : tactic
+syntax[rwSeq, 100000] "rw " rwRuleSeq (location)? : tactic
 syntax[erw] "erw " rwRule (location)? : tactic
-syntax[erwSeq, 1] "erw " rwRuleSeq (location)? : tactic
+syntax[erwSeq, 100000] "erw " rwRuleSeq (location)? : tactic
 
 private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
   `(tactic| $tac; try (withReducible rfl))
@@ -248,7 +249,7 @@ syntax[introMatch] "intro " matchAlts : tactic
 syntax[existsIntro] "exists " term : tactic
 
 /- We use a priority > 0, to avoid ambiguity with the builtin `have` notation -/
-macro[1] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro[100000] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
 
 syntax "repeat " tacticSeq : tactic
 macro_rules
diff --git a/stage0/src/Lean/Elab/Syntax.lean b/stage0/src/Lean/Elab/Syntax.lean
index 7934db9217..7e027d20ed 100644
--- a/stage0/src/Lean/Elab/Syntax.lean
+++ b/stage0/src/Lean/Elab/Syntax.lean
@@ -231,12 +231,12 @@ where
 
 private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Option Name × Nat) := do
   if stx.isNone then
-    pure (none, 0)
+    pure (none, evalPrio! default)
   else
     let arg := stx[1]
     if arg.getKind == `Lean.Parser.Command.parserKind then
       let k := arg[0].getId
-      pure (k, 0)
+      pure (k, evalPrio! default)
     else if arg.getKind == `Lean.Parser.Command.parserPrio then
       let prio ← liftMacroM <| evalPrio arg[0]
       pure (none, prio)
diff --git a/stage0/stdlib/Lean/Elab/Syntax.c b/stage0/stdlib/Lean/Elab/Syntax.c
index 93b2793ed5..0582a676ac 100644
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
@@ -443,7 +443,7 @@ lean_object* l_List_filterMap___at_Lean_Elab_Term_toParserDescrAux___spec__10(le
 lean_object* l_Lean_Elab_Term_toParserDescrAux_match__5___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_String_capitalize(lean_object*);
 lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacro_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_object*);
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_object*);
 lean_object* l_Lean_Elab_Command_elabSyntax_match__2___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMixfix___lambda__1___closed__4;
 extern lean_object* l_stx___x3c_x7c_x3e_____closed__6;
@@ -1043,7 +1043,7 @@ lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___bo
 lean_object* l___private_Init_Meta_0__Array_mapSepElemsMAux___at_Lean_Elab_Command_elabMacroRulesAux___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___spec__1___closed__8;
 extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__4;
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1;
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1;
 lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__4;
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_checkLeftRec___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMacro___closed__2;
@@ -13432,7 +13432,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = lean_unsigned_to_nat(0u);
+x_2 = lean_unsigned_to_nat(1000u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -13937,7 +13937,7 @@ return x_160;
 }
 else
 {
-lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; 
+lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; 
 lean_dec(x_9);
 lean_dec(x_3);
 x_161 = lean_unsigned_to_nat(0u);
@@ -13947,24 +13947,25 @@ x_163 = l_Lean_Syntax_getId(x_162);
 lean_dec(x_162);
 x_164 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_164, 0, x_163);
-x_165 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_165, 0, x_164);
-lean_ctor_set(x_165, 1, x_161);
+x_165 = lean_unsigned_to_nat(1000u);
 x_166 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_166, 0, x_165);
-lean_ctor_set(x_166, 1, x_5);
-return x_166;
+lean_ctor_set(x_166, 0, x_164);
+lean_ctor_set(x_166, 1, x_165);
+x_167 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_167, 0, x_166);
+lean_ctor_set(x_167, 1, x_5);
+return x_167;
 }
 }
 else
 {
-lean_object* x_167; lean_object* x_168; 
+lean_object* x_168; lean_object* x_169; 
 lean_dec(x_3);
-x_167 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__4;
-x_168 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_168, 0, x_167);
-lean_ctor_set(x_168, 1, x_5);
-return x_168;
+x_168 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__4;
+x_169 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_169, 0, x_168);
+lean_ctor_set(x_169, 1, x_5);
+return x_169;
 }
 }
 }
@@ -35042,7 +35043,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -35052,11 +35053,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
@@ -40142,9 +40143,9 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabMacro___closed__1);
 res = l___regBuiltin_Lean_Elab_Command_elabMacro(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1);
-res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_io_mk_world());
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1);
+res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_Elab_Command_withExpectedType___closed__1 = _init_l_Lean_Elab_Command_withExpectedType___closed__1();