Chores: Updating repos and Lean version support

.gitmodules

@@ -27,7 +27,7 @@
 	ignore = dirty
 [submodule "src/data/test/miniF2F-lean4"]
 	path = src/data/test/miniF2F-lean4
-	url = https://github.com/yangky11/miniF2F-lean4
+	url = https://github.com/amit9oct/miniF2F-lean4.git
 [submodule "src/data/test/PutnamBench"]
 	path = src/data/test/PutnamBench
 	url = https://github.com/trishullab/PutnamBench.git

pyproject.toml

@@ -5,7 +5,7 @@ requires = [
 build-backend = "hatchling.build"
 [project]
 name = "itp_interface"
-version = "1.12.0"
+version = "1.13.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]

src/data/test/Mathlib/lake-manifest.json

@@ -1,21 +1,21 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,37 +45,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "b0256621cb88178e9ad932a53633077b3029e621",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.36.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«repl-mathlib-tests»",

src/data/test/Mathlib/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.36.0-rc2"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where

src/data/test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.30.0
+leanprover/lean4:v4.36.0-rc2

src/itp_interface/lean/tactic_parser.py

@@ -312,8 +312,8 @@ def toolchain_version_and_env_version(version_dir: str|None=None) -> tuple[str,
 
 def change_toolchain_version(lean_version_needed: str, toolchain_file: str, toolchain_content: str):
     # Replace the version in the toolchain file
-    # The version should be like 4.x.y
-    pattern = r'^4\.\d+\.\d+$'
+    # The version should be like 4.x.y, optionally with a release-candidate suffix like 4.x.y-rcN
+    pattern = r'^4\.\d+\.\d+(-rc\d+)?$'
     if not re.match(pattern, lean_version_needed):
         raise RuntimeError(f"Tactic parser built with Lean version {toolchain_content}, but version {lean_version_needed} is required." +
         "Don't know how to build Lean which is not of the form 4.x.y. " +

src/itp_interface/lean/tactic_parser/TacticParser/Base64.lean

@@ -1,6 +1,7 @@
 /-
 Base64 decoder for receiving Lean code from Python.
 -/
+import TacticParser.Compat
 
 namespace TacticParser.Base64
 

src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean

@@ -47,6 +47,86 @@ def elabCompatPreV427 : CommandElab := fun stx => do
     for c in cmds do
       elabCommand c
 
+-- ---------------------------------------------------------------------------
+-- Removed-`String`-method shims.
+--
+-- The Lean 4 `String` type was reworked around UTF-8 slices (landing by v4.35)
+-- and the whole-`String` spellings `String.trim`, `String.trimLeft`,
+-- `String.trimRight`, `String.dropRightWhile`, `String.takeRightWhile`, and
+-- `String.dropRight` were removed. The `TacticParser` source still uses those
+-- spellings (`s.trim`, `line.trimLeft`, `s.dropRightWhile p`, …).
+--
+-- Rather than gate on a version number (fragile — the exact removal release is
+-- easy to get wrong, and different methods could in principle go at different
+-- times), each shim below is elaborated only when the corresponding `String.*`
+-- constant is ABSENT from the current environment. On toolchains that still
+-- provide the core definition the shim is skipped and the core version is used;
+-- on toolchains where it has been removed the shim supplies it. The shims use
+-- only primitives stable across the documented range (`String.toList`,
+-- `String.push`, `Char.isWhitespace`, and `List` operations), so every call
+-- site compiles unchanged on all supported toolchains.
+-- ---------------------------------------------------------------------------
+
+/-- Elaborate the brace-delimited body iff `name✝` is absent from the current
+    environment. The single leading identifier is the fully-qualified constant to
+    probe; the body is brace-delimited so its `command*` does not swallow the
+    declarations that follow. -/
+syntax (name := compatIfMissing) "compat_if_missing " ident "{" command* "}" : command
+
+@[command_elab compatIfMissing]
+def elabCompatIfMissing : CommandElab := fun stx => do
+  let name := stx[1].getId
+  unless (← getEnv).contains name do
+    for c in stx[3].getArgs do
+      elabCommand c
+
+/-- Build a `String` from characters without `String.mk` (deprecated on recent
+    toolchains) or `String.ofList` (absent on older ones). Always defined; only
+    used by the shims below. -/
+private def String.itpOfChars (cs : List Char) : String :=
+  cs.foldl (fun s c => s.push c) ""
+
+/- Shim for a removed `String.trimLeft`: drop leading whitespace. -/
+compat_if_missing String.trimLeft {
+  def String.trimLeft (s : String) : String :=
+    String.itpOfChars (s.toList.dropWhile Char.isWhitespace)
+}
+
+/- Shim for a removed `String.trimRight`: drop trailing whitespace. -/
+compat_if_missing String.trimRight {
+  def String.trimRight (s : String) : String :=
+    String.itpOfChars (s.toList.reverse.dropWhile Char.isWhitespace).reverse
+}
+
+/- Shim for a removed `String.trim`: drop leading and trailing whitespace.
+    Uses `trimLeft`/`trimRight`, which resolve to the core or shimmed version. -/
+compat_if_missing String.trim {
+  def String.trim (s : String) : String :=
+    s.trimLeft.trimRight
+}
+
+/- Shim for a removed `String.dropRightWhile`: drop the trailing run of
+    characters satisfying `p`, returning the remaining prefix. -/
+compat_if_missing String.dropRightWhile {
+  def String.dropRightWhile (s : String) (p : Char → Bool) : String :=
+    String.itpOfChars (s.toList.reverse.dropWhile p).reverse
+}
+
+/- Shim for a removed `String.takeRightWhile`: take the trailing run of
+    characters satisfying `p`, in original order. -/
+compat_if_missing String.takeRightWhile {
+  def String.takeRightWhile (s : String) (p : Char → Bool) : String :=
+    String.itpOfChars (s.toList.reverse.takeWhile p).reverse
+}
+
+/- Shim for a removed `String.dropRight`: drop the last `n` characters.
+    Nat subtraction saturates at 0, so `n ≥ length` yields the empty string. -/
+compat_if_missing String.dropRight {
+  def String.dropRight (s : String) (n : Nat) : String :=
+    let cs := s.toList
+    String.itpOfChars (cs.take (cs.length - n))
+}
+
 -- ---------------------------------------------------------------------------
 -- Pre-v4.27 shims.
 --