Spaces:
Runtime error
Runtime error
Update app.py
Browse files
app.py
CHANGED
@@ -10,7 +10,7 @@ model_name = "internlm/internlm2-math-plus-7b"
|
|
10 |
HF_TOKEN = os.environ.get("HF_TOKEN")
|
11 |
#login(HF_TOKEN)
|
12 |
|
13 |
-
generator = pipeline('text-generation', model=model_name, token=HF_TOKEN)
|
14 |
|
15 |
# Function for generating Lean 4 code
|
16 |
def generate_lean4_code(prompt):
|
|
|
10 |
HF_TOKEN = os.environ.get("HF_TOKEN")
|
11 |
#login(HF_TOKEN)
|
12 |
|
13 |
+
generator = pipeline('text-generation', model=model_name, trust_remote_code=True, token=HF_TOKEN)
|
14 |
|
15 |
# Function for generating Lean 4 code
|
16 |
def generate_lean4_code(prompt):
|