From f06007733e74a859b4d20665404e49eaa80454a6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 11:44:30 +1000 Subject: [PATCH] fix: use the String API that survives v4.35.0-rc3 `String.trim` and `String.dropRight` are removed in v4.35.0-rc3, so `Core/Generate.lean` no longer elaborates there, which in turn breaks any downstream project that builds this package at that toolchain. Move the four sites to `trimAscii` and `dropEnd`. Both return a `String.Slice`, so each call gains the `.toString` that line 1848 of the same file was already using for `trimAsciiEnd`. The replacements have existed since well before v4.33.0 -- the old names were merely deprecated until rc3 removed them -- so this needs no toolchain change here: `lake build` is clean on this package's own v4.33.0 and on v4.35.0-rc3. Co-Authored-By: Claude Opus 5 --- LeanEvalGenerator/Core/Generate.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean index 9013df1..4c2022c 100644 --- a/LeanEvalGenerator/Core/Generate.lean +++ b/LeanEvalGenerator/Core/Generate.lean @@ -67,7 +67,7 @@ def RootRequire.ofSpec (spec : DependencySpec) : RootRequire := { name := spec.name, git := some spec.git, rev := some spec.rev } private def nonEmptyTrimmed? (value? : Option String) : Option String := - value?.bind fun v => let v := v.trim; if v.isEmpty then none else some v + value?.bind fun v => let v := v.trimAscii.toString; if v.isEmpty then none else some v /-- The `[[require]]` to emit for a selected root require, or an explanation of why a standalone workspace cannot reproduce it. -/ @@ -1851,8 +1851,8 @@ def injectSolutionHoleModifiers (signature basename : String) : Option String := if trimmed == noncomputableKw then "" else if trimmed.endsWith noncomputableKw && - (trimmed.dropRight noncomputableKw.length).back.isWhitespace then - trimmed.dropRight noncomputableKw.length + (trimmed.dropEnd noncomputableKw.length).toString.back.isWhitespace then + (trimmed.dropEnd noncomputableKw.length).toString else prefixText let trimmedPrefix := prefixText.trimAsciiEnd.toString @@ -2919,7 +2919,7 @@ def buildHolesMetadata (root : System.FilePath) (entry : EvalProblemMetadata) let startOff ← src.offsetForLineColumn e.startLine e.startColumn let endOff ← src.offsetForLineColumn e.endLine e.endColumn let bodyRaw := Source.slice src startOff endOff - let body := (stripProblemMarkers bodyRaw).trim + let body := (stripProblemMarkers bodyRaw).trimAscii.toString holes := holes.push <| ojObj #[ ("name", ojStr e.declarationName), ("basename", ojStr (lastComponentStr e.declarationName)),