From 82932ec86a865b7c9468e39472d36b346f422995 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 22 Aug 2025 19:04:04 +0200
Subject: [PATCH] feat: add stop position to parser (#10057)

This PR adds a stop position field to parser input contexts, allowing
the parser to be instructed to stop parsing prior to the end of a file.

This is step 1, prior to a stage0 update, to make run-time data
structures sufficiently compatible to avoid segfaults. After the update,
the actual code to stop parsing can be merged.
---
 src/Init/Data/String/Basic.lean | 5 +++++
 src/Lean/Parser/Types.lean      | 6 +++++-
 stage0/src/stdlib_flags.h       | 3 +++
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index ffa6b94e08..fba3d347ec 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -2084,6 +2084,11 @@ theorem le_iff {i₁ i₂ : Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteI
 
 @[simp] theorem mk_le_mk {i₁ i₂ : Nat} : Pos.mk i₁ ≤ Pos.mk i₂ ↔ i₁ ≤ i₂ := .rfl
 
+@[simp] theorem le_refl {p : Pos} : p ≤ p := mk_le_mk.mpr (Nat.le_refl _)
+
+@[simp] theorem le_trans {p1 p2 p3 : Pos} : p1 ≤ p2 → p2 ≤ p3 → p1 ≤ p3 := fun h1 h2 =>
+  mk_le_mk.mpr <| Nat.le_trans (mk_le_mk.mp h1) (mk_le_mk.mp h2)
+
 theorem lt_iff {i₁ i₂ : Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx := .rfl
 
 @[simp] theorem mk_lt_mk {i₁ i₂ : Nat} : Pos.mk i₁ < Pos.mk i₂ ↔ i₁ < i₂ := .rfl
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index b6a9de5c98..8199307353 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -51,7 +51,11 @@ structure InputContext where
   input    : String
   fileName : String
   fileMap  : FileMap
-  deriving Inhabited
+  endPos   : String.Pos := input.endPos
+  endPos_valid : endPos ≤ input.endPos := by simp
+
+instance : Inhabited InputContext where
+  default := ⟨"", default, default, "".endPos, String.Pos.mk_le_mk.mpr (Nat.le_refl _)⟩
 
 /-- Input context derived from elaboration of previous commands. -/
 structure ParserModuleContext where
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..f76d71f579 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,8 @@
 #include "util/options.h"
 
+
+/* Dear CI, please update stage0 */
+
 namespace lean {
 options get_default_options() {
     options opts;