From 1bf4f88ef080d43b21073bef93f210b5672c6e49 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Tue, 10 Nov 2026 20:32:25 +0000 Subject: [PATCH 1/3] Add Lean 4.36.0 support to tactic parser with backward compatibility Lean reworked the String type around UTF-8 slices (landing by v4.35) and removed the whole-String spellings String.trim, trimLeft, trimRight, dropRightWhile, takeRightWhile, and dropRight, which the TacticParser source uses. Add existence-gated shims in Compat.lean that reintroduce each spelling only when the corresponding String.* constant is absent from the environment, so toolchains that still provide the core definition use it unchanged while newer ones get the shim. Shims use only primitives stable across the supported range (String.toList, String.push, Char.isWhitespace, List ops). Also widen the version regex in tactic_parser.py to accept release-candidate suffixes (e.g. 4.36.0-rc2), and import Compat into Base64.lean so the shims are in scope there. Verified: full build on 4.27.0, 4.30.0, 4.35.0, and 4.36.0-rc2; end-to-end data extraction clean on batteries (4.36.0-rc2) and miniF2F (4.27.0). Co-Authored-By: Claude Opus 4.8 (1M context) --- src/itp_interface/lean/tactic_parser.py | 4 +- .../tactic_parser/TacticParser/Base64.lean | 1 + .../tactic_parser/TacticParser/Compat.lean | 80 +++++++++++++++++++ 3 files changed, 83 insertions(+), 2 deletions(-) diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index a9c2162..0307351 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/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. " + diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Base64.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Base64.lean index 786c87f..a9b2f6f 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Base64.lean +++ b/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 diff --git a/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean b/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean index f78c6d0..a2e08ea 100644 --- a/src/itp_interface/lean/tactic_parser/TacticParser/Compat.lean +++ b/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. -- From e33de6d084e813a44f773dc3763cc24304e41fdf Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Wed, 11 Nov 2026 09:38:40 +0000 Subject: [PATCH 2/3] chore: update test repos and Mathlib project toward Lean 4.36.0-rc2 - batteries: bump to v4.36.0-rc2 - cslib: bump to v4.36.0-rc2 - Mathlib (repl-mathlib-tests): repin mathlib require and lean-toolchain to v4.36.0-rc2 and regenerate lake-manifest.json - miniF2F-lean4: point submodule at amit9oct fork on Lean 4.27.0 - clever: bump to latest version Co-Authored-By: Claude Opus 4.8 (1M context) --- .gitmodules | 2 +- src/data/test/Mathlib/lake-manifest.json | 30 ++++++++++++------------ src/data/test/Mathlib/lakefile.lean | 2 +- src/data/test/Mathlib/lean-toolchain | 2 +- src/data/test/batteries | 2 +- src/data/test/clever | 2 +- src/data/test/cslib | 2 +- src/data/test/miniF2F-lean4 | 2 +- 8 files changed, 22 insertions(+), 22 deletions(-) diff --git a/.gitmodules b/.gitmodules index d7a125b..f2cce8b 100644 --- a/.gitmodules +++ b/.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 diff --git a/src/data/test/Mathlib/lake-manifest.json b/src/data/test/Mathlib/lake-manifest.json index ed9c558..a40d984 100644 --- a/src/data/test/Mathlib/lake-manifest.json +++ b/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»", diff --git a/src/data/test/Mathlib/lakefile.lean b/src/data/test/Mathlib/lakefile.lean index d22cb4c..53f6c59 100644 --- a/src/data/test/Mathlib/lakefile.lean +++ b/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 diff --git a/src/data/test/Mathlib/lean-toolchain b/src/data/test/Mathlib/lean-toolchain index af9e5d3..0fc4336 100644 --- a/src/data/test/Mathlib/lean-toolchain +++ b/src/data/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0 +leanprover/lean4:v4.36.0-rc2 diff --git a/src/data/test/batteries b/src/data/test/batteries index 32dc18c..d4c39b2 160000 --- a/src/data/test/batteries +++ b/src/data/test/batteries @@ -1 +1 @@ -Subproject commit 32dc18cde3684679f3c003de608743b57498c56f +Subproject commit d4c39b228d4a06f3b00748c2c445a7b9f056a6e3 diff --git a/src/data/test/clever b/src/data/test/clever index 7d0e80f..8348039 160000 --- a/src/data/test/clever +++ b/src/data/test/clever @@ -1 +1 @@ -Subproject commit 7d0e80f5b35383126148267c8bfbbd6fe8ff2309 +Subproject commit 8348039a7ff7730a126d761e71d0439735eeb3e2 diff --git a/src/data/test/cslib b/src/data/test/cslib index c7944a9..8a8ad74 160000 --- a/src/data/test/cslib +++ b/src/data/test/cslib @@ -1 +1 @@ -Subproject commit c7944a9fb44c3298f1a960a5e574ab23a6ab8ed5 +Subproject commit 8a8ad7489cdccb007ad7279bfb9d03bbda2229ad diff --git a/src/data/test/miniF2F-lean4 b/src/data/test/miniF2F-lean4 index 5746b7d..7d60222 160000 --- a/src/data/test/miniF2F-lean4 +++ b/src/data/test/miniF2F-lean4 @@ -1 +1 @@ -Subproject commit 5746b7d6c47855ce1294bed87329618ff7f1bc31 +Subproject commit 7d60222d9961c5cfd13bad59bba964154cbb6a1e From 40ecf2376d44931c5fd257583e52342701a44d86 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Wed, 11 Nov 2026 09:39:47 +0000 Subject: [PATCH 3/3] Bump version to 1.13.0 in pyproject.toml Co-Authored-By: Claude Opus 4.8 (1M context) --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 2fd91f2..1525f9b 100644 --- a/pyproject.toml +++ b/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" }, ]