Upload folder using huggingface_hub

app.py

@@ -81,8 +81,12 @@ def ensure_mathlib_import(code: str) -> str:
     return f"import Mathlib\n\n{code.lstrip()}"
 
 
-def split_stream(text: str) -> tuple[str, str]:
+def split_stream(text: str, thinking: bool = True) -> tuple[str, str]:
     """Split a partial generation into (reasoning, answer-so-far)."""
+    if not thinking:
+        # `enable_thinking=False` puts the empty think block in the *prompt*,
+        # so the generation is the answer with no `</think>` marker.
+        return "", text
     close = list(re.finditer(r"</think>", text, flags=re.I))
     if close:
         reasoning = text[: close[-1].start()]
@@ -199,13 +203,14 @@ def formalize(
         now = time.perf_counter()
         if now - last_push > 0.25:
             last_push = now
-            reasoning, answer = split_stream(full)
-            yield partial_lean(answer), reasoning or "Thinking…", used_seed
+            reasoning, answer = split_stream(full, thinking)
+            placeholder = "Thinking…" if thinking else "(thinking disabled)"
+            yield partial_lean(answer), reasoning or placeholder, used_seed
     thread.join()
 
     elapsed = time.perf_counter() - start
     n_tokens = len(tokenizer(full, add_special_tokens=False).input_ids)
-    reasoning, _ = split_stream(full)
+    reasoning, _ = split_stream(full, thinking)
     code = ensure_mathlib_import(extract_lean_code_from_inference(full))
     if not code.strip():
         code = (