Verisyntax — brugermanual (prototype 0.1)

Lokal LLM-assistance

LLM-funktioner er valgfrie. Version 0.1 kan bede en lokal Ollama-model om et redigerbart kodeforslag:

<compiler>/verisyntax llm suggest-code request.txt --model glm-4.7-flash:latest

Kontekstvinduet er 64K som standard. Vælg 128K eksplicit, når opgaven og den lokale models kapacitet kræver det:

<compiler>/verisyntax llm suggest-code request.txt --model glm-4.7-flash:latest --context 128k

Den lokalt installerede qwen3:14b har et maksimalt kontekstvindue på 40.960 tokens. Den kan derfor ikke opfylde Verisyntax-kontrakten på 64K eller 128K og bliver afvist med en tydelig fejl i stedet for at blive kørt med en skjult lavere grænse. Desktopfeltets aktuelle standard er qwen3.6:35b-a3b: med suggest-code-v8-task-fidelity bestod den alle 10 compiler- og opgavekontroller i to gentagne kørsler uden reparationsrunde. Den afgrænsede suite dækker deterministisk logik, bevaring, boolsk og kontinuerlig Bayes-syntaks, sikker negation, ugyldig-kode-reparation, category/unit/period samt joins med to og tre sources. Modellen var også mest præcis af tre modeller på to artikel-passagetests. glm-4.7-flash:latest var hurtigst i den ældre en-opgaves kodeprøve og kan fortsat vælges. qwen3-coder:30b bestod den enkle artikel, men blev korrekt afvist på den svære, fordi et uddrag ikke matchede kilden ordret og i rækkefølge. Artikelpassager bruger fortsat segment-article-v1.

Den praktiske vurdering er, at qwen3.6:35b-a3b giver god hjælp til afgrænsede og reviewbare Verisyntax-udkast, inklusive de testede multi-source joins og typede konstruktioner. Syntaksreference, struktureret output, én begrænset reparationsrunde, task-fidelity-regler, C++-validering og bevaringskontrol gør arbejdsgangen væsentligt mere pålidelig end fri tekstfuldførelse. Ti syntetiske opgaver dokumenterer ikke robusthed på store projekter, tvetydige virkelige schemas, lang-kontekst-bevaring, semantisk fejlfinding eller domænekorrekthed. Brug den derfor som forslagshjælp, ikke som autonom udvikler, og læs altid hele udkastet før anvendelse.

<compiler>/verisyntax llm suggest-code <example-project> --model glm-4.7-flash:latest --context 64k

Kun en eksplicit loopback-adresse (127.0.0.1, localhost eller ::1) accepteres; der er ingen cloud-fallback. Kommandoen:

  1. kræver JSON efter et fast schema;
  2. validerer schemaet igen i C++;
  3. kører forslaget gennem Verisyntax-parser og semantisk kontrol;
  4. viser provider, model, promptversion, schemaversion, kontekstvindue samt input- og outputhash;
  5. skriver forslaget til skærmen som proposed code (not applied) og sætter review_required=true.

extraction_confidence er modellens sikkerhed på struktureringen, ikke sandsynligheden for at indholdet er sandt. Input og output registreres med SHA-256. Modeldigest gemmes sammen med det fulde llm_runs-auditrecord.

Claim-udtrækning kan køres over eksplicit valgte, allerede lagrede mentions:

<compiler>/verisyntax llm propose-claim model.vsx local \
  --mention MENTION_ID_1 \
  --mention MENTION_ID_2 \
  --model qwen3-coder:30b \
  --context 64k

C++ læser kun de angivne excerpts og deres synlige source/version-provenance fra SQLite/PostgreSQL. Source-tekst behandles som utroværdigt indhold, ikke instruktioner. Ollama-endpointet skal være loopback; der findes ingen cloud-fallback. Output må kun referere IDs fra den viste retrieval-bundle og valideres mod verisyntax.claim-proposal version 1. Modellen kan ikke selv gemme outputtet som claim eller fact.

Kørslen auditerer provider, modelnavn og installeret digest, prompt/schema-version, temperatur, seed, 64K/128K, input/outputhash, status og den præcise rækkefølge af mentions. Ugyldigt modeloutput markeres invalid; lokal transport/model-fejl markeres failed.

I IDE'en er lokal AI slået fra som standard. Sæt verisyntax.localLlm.enabled til true; kontrollér endpoint, model og 64k/128k. Suggest Claim With Local LLM viser de seneste lagrede mentions og sender kun dem, brugeren markerer efter en modal bekræftelse. Forslaget åbnes som redigerbar JSON og er stadig ikke gemt. Store Last Edited Local Claim Draft validerer den redigerede tekst og evidensen igen og opretter kun en proposed version. Godkendelse til fact er fortsat et separat trin.

Regelforslag bruger samme lokale og retrieval-synlige grænse. Modellen ser kun de valgte mentions samt navn og aritet for predicates i det aktuelt validerede program. Mentions er kontekst, ikke facts eller instruktioner; body-predicates uden for kataloget afvises af C++. CLI-kommandoen skriver kun redigerbar JSON og et audit-ID:

<compiler>/verisyntax llm propose-rule model.vsx local rule-request.txt \
  --mention MENTION_ID_1 --model qwen3-coder:30b --context 64k
<compiler>/verisyntax rules propose model.vsx local edited-rule.json \
  --origin-llm-run LLM_RUN_ID

I IDE'en svarer dette til Suggest Rule With Local LLM og derefter Store Last Edited Local Rule Draft. Lagring genvaliderer den aktuelt redigerede JSON, opretter kun en inaktiv proposed regelversion og bevarer forbindelsen til model, digest, audit-run og de synlige mentions. Approve or Reject Rule er fortsat et selvstændigt, hash-bundet menneskeligt trin.