Spaces:
Sleeping
Sleeping
Commit History
-
Remove Lean+Mathlib warmup step from Dockerfile
p4r5kpftnp-cmd +1: Claude Sonnet 4.6The warmup triggered a full Mathlib download which exceeded HF Spaces build limits. Mathlib will now be cached lazily on the first user request instead of at build time. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>23a1c60 -
Fix Dockerfile: collapse multi-line python -c into single line
p4r5kpftnp-cmd +1: Claude Sonnet 4.6Docker was parsing the newlines in the heredoc-style python command as separate Dockerfile instructions, causing 'unknown instruction: import'. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>dbbf243
-
Add Hugging Face Spaces deployment with Groq API
p4r5kpftnp-cmd +1: Claude Sonnet 4.6- Replace Ollama/local LLM with Groq API (langchain-groq + groq SDK) - Default model changed to llama-3.3-70b-versatile across all LLM clients - Add Gradio web UI (app.py) as the HF Spaces entry point - Add Dockerfile with Ubuntu 22.04 + Lean 4 via elan, Mathlib pre-warmed - Update requirements.txt: remove ollama/langchain-ollama, add groq/langchain-groq/gradio Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>c2ebdf5