Spaces:
Running
Running
File size: 962 Bytes
16fb4fc | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 | #!/usr/bin/env python3
import os
import sys
# Add src to Python path
sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
from lean_verifier import LeanEnvironment
def main():
print("Setting up Lean Environment and pre-caching Mathlib...")
print("This might take a while if Mathlib has not been built yet.")
# Initialize the Lean environment with Mathlib
lean_env = LeanEnvironment(use_mathlib=True)
print("\nEnvironment initialized successfully!")
# Run a simple test
print("\nRunning a quick verification test...")
test_code = """
import Mathlib
example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 :=
sorry
"""
result = lean_env.verify_proof(test_code)
print(f"Test Result: {result['status']}")
if result['status'] != 'success':
print(f"Errors: {result['errors']}")
print(f"Goals: {result['goals']}")
if __name__ == "__main__":
main()
|