Initial commit

.gitignore

@@ -0,0 +1 @@
+.vscode

app.py

@@ -1,70 +1,102 @@
+import os
+import torch
 import gradio as gr
-from huggingface_hub import InferenceClient
+import spaces
+from threading import Thread
+from transformers import AutoTokenizer, AutoModelForCausalLM, FineGrainedFP8Config, TextIteratorStreamer
 
+# >>>> CHANGE THIS <<<<
+MODEL_ID = os.getenv("MODEL_ID", "theostos/LLM4Docq-annotator")
 
-def respond(
-    message,
-    history: list[dict[str, str]],
-    system_message,
-    max_tokens,
-    temperature,
-    top_p,
-    hf_token: gr.OAuthToken,
-):
-    """
-    For more information on `huggingface_hub` Inference API support, please check the docs: https://huggingface.co/docs/huggingface_hub/v0.22.2/en/guides/inference
-    """
-    client = InferenceClient(token=hf_token.token, model="openai/gpt-oss-20b")
+# Matches your training style: messages=[{"role":"user","content": template.format(term=..., dependencies=...)}]
+INSTRUCTION_TEMPLATE = (
+    "You are a Rocq code annotator. Given the Coq term and its dependencies, "
+    "produce helpful inline comments and explanations.\n\n"
+    "Term:\n{term}\n\nDependencies:\n{dependencies}\n"
+)
 
-    messages = [{"role": "system", "content": system_message}]
+HF_TOKEN = os.getenv("HF_TOKEN")
 
-    messages.extend(history)
+tokenizer = AutoTokenizer.from_pretrained(MODEL_ID, token=HF_TOKEN, use_fast=True)
+if tokenizer.pad_token_id is None and tokenizer.eos_token_id is not None:
+    tokenizer.pad_token_id = tokenizer.eos_token_id
 
-    messages.append({"role": "user", "content": message})
+quant_config = FineGrainedFP8Config()
 
-    response = ""
+_model = None
+def load_model():
+    global _model
+    if _model is None:
+        _model = AutoModelForCausalLM.from_pretrained(
+            MODEL_ID,
+            token=HF_TOKEN,
+            device_map="auto",
+            dtype="auto",                 # load base weights in their optimal dtype
+            quantization_config=quant_config,  # <-- FP8 quantization
+            trust_remote_code=True,
+        )
+    return _model
 
-    for message in client.chat_completion(
-        messages,
-        max_tokens=max_tokens,
-        stream=True,
-        temperature=temperature,
-        top_p=top_p,
-    ):
-        choices = message.choices
-        token = ""
-        if len(choices) and choices[0].delta.content:
-            token = choices[0].delta.content
+def build_messages(term: str, deps: str):
+    content = INSTRUCTION_TEMPLATE.format(term=term, dependencies=deps)
+    return [{"role": "user", "content": content}]
 
-        response += token
-        yield response
+# Estimate duration for ZeroGPU (default is 60s). Shorter = better queue priority.
+def _duration(term, deps, temperature, top_p, max_new_tokens, repetition_penalty):
+    # crude: ~2.5 tok/s + 30s headroom
+    return int(min(300, max(60, (int(max_new_tokens) / 2.5) + 30)))
 
+@spaces.GPU(duration=_duration)
+def generate(term, deps, temperature, top_p, max_new_tokens, repetition_penalty):
+    model = load_model()
+    device = "cuda" if torch.cuda.is_available() else "cpu"
 
-"""
-For information on how to customize the ChatInterface, peruse the gradio docs: https://www.gradio.app/docs/chatinterface
-"""
-chatbot = gr.ChatInterface(
-    respond,
-    type="messages",
-    additional_inputs=[
-        gr.Textbox(value="You are a friendly Chatbot.", label="System message"),
-        gr.Slider(minimum=1, maximum=2048, value=512, step=1, label="Max new tokens"),
-        gr.Slider(minimum=0.1, maximum=4.0, value=0.7, step=0.1, label="Temperature"),
-        gr.Slider(
-            minimum=0.1,
-            maximum=1.0,
-            value=0.95,
-            step=0.05,
-            label="Top-p (nucleus sampling)",
-        ),
-    ],
-)
+    messages = build_messages(term, deps)
+    inputs = tokenizer.apply_chat_template(
+        messages,
+        tokenize=True,
+        add_generation_prompt=True,
+        return_tensors="pt",
+    ).to(device)
+
+    streamer = TextIteratorStreamer(tokenizer, skip_prompt=True, skip_special_tokens=True)
+    gen_kwargs = dict(
+        inputs=inputs,
+        max_new_tokens=int(max_new_tokens),
+        temperature=float(temperature),
+        top_p=float(top_p),
+        do_sample=True,
+        streamer=streamer,
+        pad_token_id=tokenizer.pad_token_id,
+        eos_token_id=tokenizer.eos_token_id,
+    )
+
+    thread = Thread(target=model.generate, kwargs=gen_kwargs)
+    thread.start()
 
-with gr.Blocks() as demo:
-    with gr.Sidebar():
-        gr.LoginButton()
-    chatbot.render()
+    out = ""
+    for token in streamer:  # stream tokens to UI
+        out += token
+        yield f"```rocq\n{out}\n```"
 
+with gr.Blocks(title="Rocq Annotator (ZeroGPU)") as demo:
+    gr.Markdown("# Rocq annotator\nThe model will produce annotated Rocq code.")
+    with gr.Row():
+        term = gr.Textbox(label="Prefix", lines=100, placeholder="Paste the prefix to use")
+        deps = gr.Textbox(label="To annotate", lines=8, placeholder="The code to annotate")
+    with gr.Row():
+        temperature = gr.Slider(0.0, 1.5, value=0.7, step=0.05, label="Temperature")
+        top_p = gr.Slider(0.1, 1.0, value=0.9, step=0.05, label="top_p")
+        max_new = gr.Slider(256, 8192, value=4096, step=32, label="max_new_tokens")
+    out = gr.Markdown(label="Annotated Rocq")
+    btn = gr.Button("Annotate")
+    btn.click(
+        generate,
+        inputs=[term, deps, temperature, top_p, max_new],
+        outputs=out,
+        concurrency_limit=1,  # cooperate with ZeroGPU queues
+    )
+    demo.queue(max_size=20, default_concurrency_limit=1)
 
 if __name__ == "__main__":
     demo.launch()

requirements.txt

@@ -0,0 +1,5 @@
+torch==2.8.0
+transformers>=4.57.1
+accelerate>=1.10
+gradio>=4.44
+spaces>=0.42