chore: update stage0

This PR promotes the `repeat`, `while`, and `repeat ... until` parsers
from `syntax` declarations in `Init.While` to `@[builtin_doElem_parser]`
definitions in `Lean.Parser.Do`, alongside the other do-element parsers.
The `while` variants and `repeat ... until` get `@[builtin_macro]`
expansions; `repeat` itself gets a `@[builtin_doElem_elab]` so a
follow-up can extend it with an option-driven choice between `Loop.mk`
and a well-founded `Repeat.mk`.

The new builtin parsers are registered at `low` priority so that the
bootstrapping `syntax` declarations in `Init.While` (still needed for
stage0 compatibility) take precedence during the transition. After the
next stage0 update, the `Init.While` syntax and macros can be removed.

src/Lean/Compiler/LCNF/EmitC.lean

@@ -207,7 +207,7 @@ def emitLns [EmitToString α] (as : List α) : EmitM Unit :=
   emitLn "}"
   return ret
 
-def toHexDigit (c : Nat) : String :=
+def toDigit (c : Nat) : String :=
   String.singleton c.digitChar
 
 def quoteString (s : String) : String :=
@@ -221,7 +221,11 @@ def quoteString (s : String) : String :=
       else if c == '\"' then "\\\""
       else if c == '?' then "\\?" -- avoid trigraphs
       else if c.toNat <= 31 then
-        "\\x" ++ toHexDigit (c.toNat / 16) ++ toHexDigit (c.toNat % 16)
+        -- Use octal escapes instead of hex escapes because C hex escapes are
+        -- greedy: "\x01abc" would be parsed as the single escape \x01abc rather
+        -- than \x01 followed by "abc".  Octal escapes consume at most 3 digits.
+        let n := c.toNat
+        "\\" ++ toDigit (n / 64) ++ toDigit ((n / 8) % 8) ++ toDigit (n % 8)
       -- TODO(Leo): we should use `\unnnn` for escaping unicode characters.
       else String.singleton c)
     q;

src/Lean/Elab/Do/InferControlInfo.lean

@@ -129,6 +129,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return thenInfo.alternative info
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
+  -- For/Repeat
   | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
@@ -136,6 +137,13 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
       continues := false,
       breaks := false
     }
+  | `(doRepeat| repeat $bodySeq) =>
+    let info ← ofSeq bodySeq
+    return { info with
+      numRegularExits := if info.breaks then 1 else 0,
+      continues := false,
+      breaks := false
+    }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>
     let mut info ← ofSeq trySeq

stage0/src/stdlib_flags.h

@@ -1,6 +1,5 @@
 #include "util/options.h"
 
-// bump
 namespace lean {
 options get_default_options() {
     options opts;