From d20d9910165736bd11fe1d5546d14cded08a947f Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Tue, 6 May 2025 20:48:44 +0000 Subject: [PATCH 1/3] Fixed theorem name match regex. --- src/itp_interface/tools/lean4_sync_executor.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/itp_interface/tools/lean4_sync_executor.py b/src/itp_interface/tools/lean4_sync_executor.py index 9d8311f..83134ef 100644 --- a/src/itp_interface/tools/lean4_sync_executor.py +++ b/src/itp_interface/tools/lean4_sync_executor.py @@ -30,8 +30,8 @@ class Lean4SyncExecutor: # We ONLY support proofs which are written in tactic mode i.e. with := syntax theorem_endings = r"(:=|(\|[\S|\s]*=>))" theorem_end_regex = r"(theorem|lemma|example)([\s|\S]*?)(:=|=>)" - theorem_regex = r"((((theorem|lemma)[\s]+([\S]*))|example)([\S|\s]*?)(:=|=>)[\s]*?)[\s]+" - theorem_name_regex = r"(((theorem|lemma)[\s]+([\S]*))|example)" + theorem_regex = r"((((theorem|lemma)[\s]+([^ :]*))|example)([\S|\s]*?)(:=|=>)[\s]*?)[\s]+" + theorem_name_regex = r"(((theorem|lemma)[\s]+([^ :]*))|example)" remove_proof_regex = r"([\s|\S]*(:=|\|))[\s|\S]*?" proof_context_separator = "⊢" proof_context_regex = r"((\d+) goals)*([\s|\S]*?)\n\n" From ddbe633b83ed239fe493953648a3aa486122ad33 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Tue, 6 May 2025 20:53:07 +0000 Subject: [PATCH 2/3] Updated `itp-interface-version` --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 0833849..e07dd2f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.1.10" +version = "1.1.11" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] From 7a8ada041873f357fc3a595296e83d5b2db589a1 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Tue, 6 May 2025 21:31:19 +0000 Subject: [PATCH 3/3] Fixed non-space character error in itp-interface. --- src/itp_interface/tools/lean4_sync_executor.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/itp_interface/tools/lean4_sync_executor.py b/src/itp_interface/tools/lean4_sync_executor.py index 83134ef..f3e7ae2 100644 --- a/src/itp_interface/tools/lean4_sync_executor.py +++ b/src/itp_interface/tools/lean4_sync_executor.py @@ -30,8 +30,8 @@ class Lean4SyncExecutor: # We ONLY support proofs which are written in tactic mode i.e. with := syntax theorem_endings = r"(:=|(\|[\S|\s]*=>))" theorem_end_regex = r"(theorem|lemma|example)([\s|\S]*?)(:=|=>)" - theorem_regex = r"((((theorem|lemma)[\s]+([^ :]*))|example)([\S|\s]*?)(:=|=>)[\s]*?)[\s]+" - theorem_name_regex = r"(((theorem|lemma)[\s]+([^ :]*))|example)" + theorem_regex = r"((((theorem|lemma)[\s]+([^\s:]*))|example)([\S|\s]*?)(:=|=>)[\s]*?)[\s]+" + theorem_name_regex = r"(((theorem|lemma)[\s]+([^\s:]*))|example)" remove_proof_regex = r"([\s|\S]*(:=|\|))[\s|\S]*?" proof_context_separator = "⊢" proof_context_regex = r"((\d+) goals)*([\s|\S]*?)\n\n"