Spaces:
Sleeping
Sleeping
File size: 1,969 Bytes
5eea309 a31226e 5eea309 110315e a31226e 5eea309 a31226e 5eea309 a31226e 5eea309 a31226e 5eea309 a31226e 5eea309 a31226e |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 |
from fastapi import FastAPI, Request
from pytanque import Pytanque, PetanqueError
import subprocess, os, tempfile
import time
app = FastAPI()
PET_PORT = 8080
MATHCOMP_PATH = "/home/mathcomp/"
pet = None
pet_process = None
dict_mathcomp = {}
@app.on_event("startup")
def startup_event():
global pet, pet_process, dict_mathcomp
pet_process = subprocess.Popen(["pet-server", "--port", str(PET_PORT)])
time.sleep(1)
pet = Pytanque("127.0.0.1", PET_PORT)
pet.connect()
print("PET server started")
for root, _, files in os.walk(MATHCOMP_PATH):
for file in files:
if file.endswith(".v"):
abs_path = os.path.join(root, file)
rel_path = os.path.relpath(abs_path, MATHCOMP_PATH)
rel_path = rel_path[:-2].replace('/', '.')
with open(abs_path, 'r') as file:
content = file.read()
dict_mathcomp[rel_path] = {"path": abs_path, "content": content}
print(f"Indexed {len(dict_mathcomp)} .v files in MathComp")
@app.on_event("shutdown")
def shutdown_event():
if pet_process:
pet_process.terminate()
print("PET server stopped")
@app.get("/check")
async def check():
return {"status": "ok", "message": "Rocq backend running"}
@app.get("/name_sources")
async def sources():
return list(dict_mathcomp.keys())
@app.get("/all_sources")
async def all_sources(req: Request):
return dict_mathcomp
@app.post("/toc")
async def toc(req: Request):
data = await req.json()
source = data['source']
try:
toc = pet.toc(dict_mathcomp[source])
result = {}
for name, details in toc:
if len(details) == 1:
info = details[0]
if info['detail'] in ['Lemma', 'Theorem']:
result[name] = {"range": info['range'], "kind": info['detail']}
return result
except Exception as e:
return {"error": str(e)}
|