Spaces:
Running
Running
include logo
Browse files- app.py +10 -2
- lean_finder_logo.png +0 -0
app.py
CHANGED
|
@@ -146,12 +146,20 @@ code{background:#f8f8f8;border:1px solid #eee;border-radius:4px;padding:2px 4px;
|
|
| 146 |
}
|
| 147 |
|
| 148 |
#vote_status{margin-top:0.5rem;text-align:center;} /* works for Markdown */
|
|
|
|
|
|
|
|
|
|
|
|
|
| 149 |
"""
|
| 150 |
|
| 151 |
|
| 152 |
with gr.Blocks(title="Lean Finder Retrieval", css=CUSTOM_CSS) as demo:
|
| 153 |
-
gr.
|
| 154 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 155 |
with gr.Row():
|
| 156 |
query_box = gr.Textbox(label="Query", lines=2, placeholder="Type your Lean query here …")
|
| 157 |
topk_slider = gr.Slider(label="Top-k", minimum=1, maximum=20, step=1, value=3)
|
|
|
|
| 146 |
}
|
| 147 |
|
| 148 |
#vote_status{margin-top:0.5rem;text-align:center;} /* works for Markdown */
|
| 149 |
+
|
| 150 |
+
#lf_header{justify-content:center;align-items:center;margin:1.2rem 0;}
|
| 151 |
+
#lf_header img{height:60px;border-radius:8px;}
|
| 152 |
+
#lf_header h1{margin:0 0 0 0.6rem;font-size:1.9rem;font-weight:700;}
|
| 153 |
"""
|
| 154 |
|
| 155 |
|
| 156 |
with gr.Blocks(title="Lean Finder Retrieval", css=CUSTOM_CSS) as demo:
|
| 157 |
+
with gr.Row(elem_id="lf_header"):
|
| 158 |
+
gr.Image("lean_finder_logo.png", show_label=False)
|
| 159 |
+
gr.HTML("<h1>Lean Finder</h1>")
|
| 160 |
+
|
| 161 |
+
gr.Markdown("Choose **Normal** for standard retrieval from Lean Finder or **Arena** to compare with LeanSearch and vote.")
|
| 162 |
+
|
| 163 |
with gr.Row():
|
| 164 |
query_box = gr.Textbox(label="Query", lines=2, placeholder="Type your Lean query here …")
|
| 165 |
topk_slider = gr.Slider(label="Top-k", minimum=1, maximum=20, step=1, value=3)
|
lean_finder_logo.png
ADDED
|