Spaces:
Running
on
Zero
Running
on
Zero
fix typo
Browse files
app.py
CHANGED
@@ -199,6 +199,11 @@ def main():
|
|
199 |
informal = gr.Textbox(value=additional_info_prompt, label="Optional informal prefix")
|
200 |
max_tokens = gr.Slider(minimum=150, maximum=4096, value=2500, label="Max Tokens")
|
201 |
submit = gr.Button("Send")
|
|
|
|
|
|
|
|
|
|
|
202 |
with gr.Column():
|
203 |
chat = gr.Chatbot(label="Chat History")
|
204 |
with gr.Accordion("Complete Output", open=False):
|
@@ -206,11 +211,6 @@ def main():
|
|
206 |
code_out = gr.Code(label="Extracted Lean4 Code", language="python")
|
207 |
state = gr.State([])
|
208 |
submit.click(chat_handler, [user_input, informal, max_tokens, state], [chat, json_out, code_out, state])
|
209 |
-
gr.Examples(
|
210 |
-
examples=examples,
|
211 |
-
inputs=["user_input", "informal", "max_tokens"],
|
212 |
-
label="Example Problems"
|
213 |
-
)
|
214 |
gr.Markdown(citation)
|
215 |
demo.launch()
|
216 |
|
|
|
199 |
informal = gr.Textbox(value=additional_info_prompt, label="Optional informal prefix")
|
200 |
max_tokens = gr.Slider(minimum=150, maximum=4096, value=2500, label="Max Tokens")
|
201 |
submit = gr.Button("Send")
|
202 |
+
gr.Examples(
|
203 |
+
examples=examples,
|
204 |
+
inputs=[user_input, informal, max_tokens],
|
205 |
+
label="Example Problems"
|
206 |
+
)
|
207 |
with gr.Column():
|
208 |
chat = gr.Chatbot(label="Chat History")
|
209 |
with gr.Accordion("Complete Output", open=False):
|
|
|
211 |
code_out = gr.Code(label="Extracted Lean4 Code", language="python")
|
212 |
state = gr.State([])
|
213 |
submit.click(chat_handler, [user_input, informal, max_tokens, state], [chat, json_out, code_out, state])
|
|
|
|
|
|
|
|
|
|
|
214 |
gr.Markdown(citation)
|
215 |
demo.launch()
|
216 |
|