From f33126fa10ad885d234746f8dc114fd033744a78 Mon Sep 17 00:00:00 2001
From: David Chanin <chanindav@gmail.com>
Date: Tue, 31 Mar 2026 15:27:06 +0100
Subject: [PATCH] Fix comment stripping crash on /- inside string literals

The crawler has been failing since March 27 because mathlib4 added
scripts/find_command_range.lean which contains /- inside a string
literal (e.g. `s.startsWith "/-"`). The comment stripper was treating
this as a block comment start, then failing to find the closing -/.

Add _find_outside_strings() helper that skips string literals when
searching for comment delimiters at the top level. Inside block
comments, strings are not special per Lean's grammar, so the existing
behavior is preserved there.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 crawler/crawler/parser/strip_lean_comments.py | 44 ++++++++++++++++---
 .../tests/parser/test_strip_lean_comments.py  | 31 +++++++++++++
 2 files changed, 69 insertions(+), 6 deletions(-)

diff --git a/crawler/crawler/parser/strip_lean_comments.py b/crawler/crawler/parser/strip_lean_comments.py
index c7be5d3..fc16459 100644
--- a/crawler/crawler/parser/strip_lean_comments.py
+++ b/crawler/crawler/parser/strip_lean_comments.py
@@ -12,6 +12,32 @@ def strip_lean_comments(lean_contents: str) -> str:
 LINE_DELIM = "--"
 
 
+def _find_outside_strings(txt: str, target: str) -> int:
+    """Find the first occurrence of target not inside a string literal.
+
+    Returns -1 if not found.
+    """
+    i = 0
+    n = len(txt)
+    target_len = len(target)
+    while i <= n - target_len:
+        if txt[i] == '"':
+            i += 1
+            while i < n:
+                if txt[i] == "\\" and i + 1 < n:
+                    i += 2
+                elif txt[i] == '"':
+                    i += 1
+                    break
+                else:
+                    i += 1
+            continue
+        if txt[i : i + target_len] == target:
+            return i
+        i += 1
+    return -1
+
+
 def has_nested_comment(txt_in_block: str) -> bool:
     if DELIM_L not in txt_in_block:
         return False
@@ -27,11 +53,17 @@ def has_nested_comment(txt_in_block: str) -> bool:
 def strip_single_comment_block(txt: str, strip_line_comments: bool = True) -> str:
     "Strips first nest of block comments"
     out = ""
-    next_line_comment_index = (
-        txt.index(LINE_DELIM) if LINE_DELIM in txt and strip_line_comments else None
-    )
-    if DELIM_L in txt:
-        block_start_index = txt.index(DELIM_L)
+    next_line_comment_index: int | None = None
+    if strip_line_comments:
+        # At top level: skip delimiters inside string literals
+        raw_line_idx = _find_outside_strings(txt, LINE_DELIM)
+        next_line_comment_index = raw_line_idx if raw_line_idx >= 0 else None
+        block_start_index = _find_outside_strings(txt, DELIM_L)
+    else:
+        # Inside a block comment: strings are not special
+        block_start_index = txt.index(DELIM_L) if DELIM_L in txt else -1
+
+    if block_start_index >= 0:
         # if we see a line comment before the start of the next block comment, remove it first
         # otherwise stuff like "-- this is /- irrelevant" will break the system
         if (
@@ -63,6 +95,6 @@ def strip_nested_block_comment(txt: str) -> str:
     "Strips nests of block comments"
     stripped_txt = txt
 
-    while DELIM_L in stripped_txt:
+    while _find_outside_strings(stripped_txt, DELIM_L) >= 0:
         stripped_txt = strip_single_comment_block(stripped_txt, True)
     return stripped_txt
diff --git a/crawler/tests/parser/test_strip_lean_comments.py b/crawler/tests/parser/test_strip_lean_comments.py
index 1da61af..cd94d46 100644
--- a/crawler/tests/parser/test_strip_lean_comments.py
+++ b/crawler/tests/parser/test_strip_lean_comments.py
@@ -143,3 +143,34 @@ def test_strip_lean_comments_handles_block_chars_in_line_comments() -> None:
 just some more code
     """.strip()
     assert strip_lean_comments(input) == expected
+
+
+def test_strip_lean_comments_ignores_delimiters_in_string_literals() -> None:
+    input = """
+def foo : IO Unit := do
+  if s.startsWith "/-" then
+    IO.println "found block comment start"
+  IO.println s!"delim is /-"
+    """.strip()
+    expected = """
+def foo : IO Unit := do
+  if s.startsWith "/-" then
+    IO.println "found block comment start"
+  IO.println s!"delim is /-"
+    """.strip()
+    assert strip_lean_comments(input) == expected
+
+
+def test_strip_lean_comments_handles_string_and_real_comment_together() -> None:
+    input = """
+/-- A doc comment -/
+def foo := "this has /- in it"
+/- real block comment -/
+def bar := 42
+    """.strip()
+    result = strip_lean_comments(input)
+    assert '"this has /- in it"' in result
+    assert "def foo" in result
+    assert "def bar := 42" in result
+    assert "A doc comment" not in result
+    assert "real block comment" not in result