Initial commit

Dockerfile

@@ -0,0 +1,23 @@
+# ===== Base Rocq + MathComp =====
+FROM mathcomp/mathcomp-dev:rocq-prover-9.0
+
+# ===== Install Coq-LSP + PET =====
+RUN opam update && \
+    opam install -y logs lwt coq-lsp
+
+# ===== Install Python + FastAPI =====
+RUN apt-get update && apt-get install -y python3 python3-pip git curl && \
+    pip install --no-cache-dir fastapi uvicorn requests
+
+# ===== Install pytanque from GitHub =====
+RUN git clone https://github.com/LLM4Rocq/pytanque.git /tmp/pytanque && \
+    pip install -e /tmp/pytanque && \
+    rm -rf /tmp/pytanque
+   
+# ===== Copy App =====
+WORKDIR /app
+COPY app.py /app
+
+EXPOSE 7861
+CMD ["uvicorn", "app:app", "--host", "0.0.0.0", "--port", "7861"]
+

app.py

@@ -0,0 +1,25 @@
+from fastapi import FastAPI, Request
+from pytanque import Pytanque, PetanqueError
+import subprocess, os, tempfile
+
+app = FastAPI()
+
+# Start PET server when container boots
+PET_PORT = 8080
+subprocess.Popen(["pet-server", "--port", str(PET_PORT)])
+pet = Pytanque("127.0.0.1", PET_PORT)
+pet.connect()
+
+@app.get("/")
+def health():
+    return {"status": "ok", "message": "Rocq backend running"}
+
+@app.post("/check")
+async def check_code(req: Request):
+    data = await req.json()
+    code = data.get("code", "")
+    try:
+        result = pet.eval(code)
+    except Exception as e:
+        result = f"Error: {e}"
+    return {"rocq_result": result}