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

@@ -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

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

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;