Update app.py

app.py

@@ -12,7 +12,7 @@ LEAN4_DEFAULT_HEADER = (
     "open BigOperators Real Nat Topology Rat\n"
 )
 
-title = """# 🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉
+title = """🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉
 You can build with this endpoint using🔮Goedel-Prover-SFT📉 available here : [Goedel-LM/Goedel-Prover-SFT](https://huggingface.co/Goedel-LM/Goedel-Prover-SFT)."""
 
 def format_prompt(formal_statement, informal_prefix=""):
@@ -31,7 +31,8 @@ def extract_code(response):
         # Find all content between ```lean4 and ``` tags
         matches = re.findall(r'```lean4(.*?)```', response, re.DOTALL)
         if not matches:
-            return "None"
+            # If no matches found in code blocks, return the full response
+            return response.strip()
         
         # Get the last complete response including the model output
         full_content = matches[-1].strip()
@@ -40,28 +41,49 @@ def extract_code(response):
         lines = full_content.split('\n')
         cleaned_lines = []
         seen_headers = set()
+        header_done = False
         
         for line in lines:
             # Skip empty lines at the start
             if not cleaned_lines and not line.strip():
                 continue
-            # Skip duplicate headers and "Complete the following..." text
-            if any(header in line for header in ["import Mathlib", "import Aesop", "set_option", "Complete the following"]):
-                if line in seen_headers:
-                    continue
-                seen_headers.add(line)
-            # Skip duplicate goal statements
+                
+            # Process headers only once
+            if not header_done and any(header in line for header in ["import Mathlib", "import Aesop", "set_option", "open BigOperators"]):
+                if line not in seen_headers:
+                    seen_headers.add(line)
+                    cleaned_lines.append(line)
+                continue
+            
+            # Mark header section as complete after processing imports and settings
+            if not header_done and cleaned_lines:
+                header_done = True
+                cleaned_lines.append("")  # Add a blank line after headers
+            
+            # Include the line if it's not a duplicate goal statement
             if "Goal:" in line and line in cleaned_lines:
                 continue
-            cleaned_lines.append(line)
+            if "Complete the following" not in line:
+                cleaned_lines.append(line)
         
         # Remove any trailing "Complete the following..." text
         while cleaned_lines and "Complete the following" in cleaned_lines[-1]:
             cleaned_lines.pop()
             
+        # Ensure the model's output is included
+        if "===========================" in full_content:
+            output_start = full_content.find("============================")
+            if output_start != -1:
+                output_text = full_content[output_start:].strip()
+                if ":= by" in output_text:
+                    proof_part = output_text[output_text.find(":= by"):]
+                    cleaned_lines.append(proof_part)
+        
         return '\n'.join(cleaned_lines)
-    except:
-        return "None"
+    except Exception as e:
+        print(f"Error in extract_code: {str(e)}")
+        return "Error processing code"
+        
 
 # Example problems
 unimath1 = """Goal:
@@ -145,7 +167,7 @@ def solve_math_problem(question, informal_prefix, max_tokens):
 
 def main():
     iface = gr.Interface(        
-        title="# 🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉",
+        title="🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉",
         description="""You can build with this endpoint using🔮Goedel-Prover-SFT📉 available here : [Goedel-LM/Goedel-Prover-SFT](https://huggingface.co/Goedel-LM/Goedel-Prover-SFT). We're using 🤖[introspector/unimath](https://huggingface.co/datasets/introspector/unimath) for cool examples, check it out below ! The demo is still a work in progress and we're looking forward to build downstream tasks that showcase outstanding mathematical reasoning. Have any ideas ? join us below !
 You can also use 🔮Goedel Prover📉 by cloning this space. Simply click here: <a style="display:inline-block" href="https://huggingface.co/spaces/Tonic/Math?duplicate=true"><img src="https://img.shields.io/badge/-Duplicate%20Space-blue?labelColor=white&style=flat&logo=data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAAXNSR0IArs4c6QAAAP5JREFUOE+lk7FqAkEURY+ltunEgFXS2sZGIbXfEPdLlnxJyDdYB62sbbUKpLbVNhyYFzbrrA74YJlh9r079973psed0cvUD4A+4HoCjsA85X0Dfn/RBLBgBDxnQPfAEJgBY+A9gALA4tcbamSzS4xq4FOQAJgCDwV2CPKV8tZAJcAjMMkUe1vX+U+SMhfAJEHasQIWmXNN3abzDwHUrgcRGmYcgKe0bxrblHEB4E/pndMazNpSZGcsZdBlYJcEL9Afo75molJyM2FxmPgmgPqlWNLGfwZGG6UiyEvLzHYDmoPkDDiNm9JR9uboiONcBXrpY1qmgs21x1QwyZcpvxt9NS09PlsPAAAAAElFTkSuQmCC&logoWidth=14" alt="Duplicate Space"></a></h3> 
 Join us : 🌟TeamTonic🌟 is always making cool demos! Join our active builder's 🛠️community 👻 [Join us on Discord](https://discord.gg/GWpVpekp) On 🤗Huggingface: [TeamTonic](https://huggingface.co/TeamTonic) & [MultiTransformer](https://huggingface.co/MultiTransformer) Math with [introspector](https://huggingface.co/introspector) On 🌐Github: [Tonic-AI](https://github.com/tonic-ai) & contribute to🌟 [SciTonic](https://github.com/Tonic-AI/scitonic)🤗Big thanks to Yuvi Sharma and all the folks at huggingface for the community grant 🤗