chore: add ControlInfo handler for doRepeat

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,5 +1,6 @@
 #include "util/options.h"
 
+// bump for ControlInfo handler
 namespace lean {
 options get_default_options() {
     options opts;

tests/bench/build/run_bench.sh

@@ -18,6 +18,17 @@ make -C "$BUILD_ROOT" -j"$(nproc)" "$STAGE_NEXT-configure"
 
 
 
+echo
+echo ">"
+echo "> Warming up $STAGE_NEXT..."
+echo ">"
+
+make -C "$BUILD_NEXT" -j"$(nproc)"
+find "$BUILD_NEXT/lib" -name "*.olean" -delete
+rm -f measurements.jsonl
+
+
+
 echo
 echo ">"
 echo "> Building $STAGE_NEXT..."
@@ -27,7 +38,7 @@ LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
 WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
   lakeprof record -- \
   "$TEST_DIR/measure.py" -t build -d -a -- \
-  make -C "$BUILD_NEXT" -j"$(nproc)" make_stdlib LAKE_EXTRA_ARGS="+Init:olean +Std:olean +Lean:olean +Lake:olean +LakeMain:olean +LeanIR:olean +Leanc:olean +LeanChecker:olean"
+  make -C "$BUILD_NEXT" -j"$(nproc)"