Verisyntax — brugermanual (prototype 0.1)

Start her — Verisyntax forklaret for begyndere

Verisyntax er et deklarativt sprog. Det betyder, at du først og fremmest beskriver hvad dine data og regler betyder. Du skriver normalt ikke løkker, knapper eller rækkefølgen af små maskininstruktioner, som du ville gøre i C++ eller Python. C++-compileren kontrollerer beskrivelsen og udfører den på en kontrolleret måde.

En Verisyntax-fil kan indeholde fire forskellige slags arbejde:

En database fortæller, hvor tabellerne ligger.
En source giver en tabel et logisk navn og beskriver dens kolonner og typer.
Et dataset vælger, filtrerer eller kombinerer sources.
Facts, rules, ask og probabilistiske deklarationer udtrykker logik og usikkerhed.

Du behøver ikke bruge alle fire dele. Et lille familieprogram kan bestå af facts, en regel og en query. Et dataanalyseprogram kan nøjes med database, sources og datasets.

De vigtigste skriveregler

Sprogets nøgleord er engelske: eksempelvis database, source, dataset, select, where, if, and og ask.
Indrykning er en del af syntaksen. Brug præcis to mellemrum inde i en blok; brug ikke tabulator.
En deklarationsoverskrift som database local: slutter med kolon.
En almindelig fact som parent(person_a, person_b) slutter ikke med punktum.
Små begyndelsesbogstaver er konkrete navne eller værdier. Store begyndelsesbogstaver er variable: Who, X og Customer.
Tekst i data-deklarationer står i dobbelte anførselstegn, eksempelvis path "<data-storage>/shop.sqlite".
En kommentar begynder med #.

Din første kørsel i den selvstændige IDE

Åbn applikationen:

open "<desktop-release>/Verisyntax IDE.app"

Du kan også åbne Finder, gå til <desktop-release> under din brugermappe og dobbeltklikke Verisyntax IDE.app. Hvis macOS viser en sikkerhedsadvarsel for den lokalt signerede udviklingsapp, så højreklik appen, vælg Åbn, og bekræft én gang. Flytter du senere appen til mappen Programmer, skal terminalkommandoen i stedet pege på <applications>/Verisyntax IDE.app.

IDE'en åbner et lokalt demo-program. Prøv dette forløb:

Når appen starter, vises Start Center. Du behøver derfor ikke begynde med at skrive et script. Vælg den indgang, der svarer til det, du allerede har:

Blank model: åbner en helt tom, ikke-gemt untitled.vsx, så du kan skrive modellen fra bunden. Den sletter ingen gemt fil, projektmappe, importeret data eller database.
Local data file: vælg CSV, JSON, TXT eller XLSX. Ved Excel viser IDE'en workbookens regneark i en liste, så fanen ikke skal skrives manuelt. C++-runtime inspicerer filen read-only, viser fundne felter, foreslåede typer og optional-felter og laver derefter et redigerbart SQLite- eller PostgreSQL-program. Hvis en ID-lignende kolonne er udfyldt og unik i alle inspicerede rækker, viser guiden den som et begrundet primary-key-forslag. Forslaget er fravalgt som standard og føjes kun til .vsx-udkastet, hvis brugeren markerer det; originalfilen omskrives aldrig. Ingen rækker importeres i guiden. Det genererede udkast skifter venstresiden til datafilens mappe, og den første Save foreslår samme mappe. Hvis mappen endnu ikke har et konfigureret Verisyntax-projekt, registreres den gemte .vsx automatisk som analyseprojektets startprogram; et eksisterende projekt omkonfigureres aldrig lydløst. Tryk derefter Check, vælg den genererede source, og brug Import files… til preview og særskilt commit. Hvis Verisyntax' importmetadata mangler, forklarer appen hvorfor tabellerne kræves og beder om særskilt godkendelse til at oprette dem, før filvælgeren og importpreviewet fortsætter.
Existing database table: vælg en eksisterende SQLite-fil eller angiv navnet på en environment variable med PostgreSQL-forbindelsen. Tryk derefter Check, vælg databasen og Schema. Vælg en tabel/view i den read-only schema-dialog, kontrollér kolonner, nullability og primary key, og tryk Add reviewed source draft. Databasen ændres ikke af denne arbejdsgang.
Saved project folder: vælg en projektmappe. De seneste fem projektmapper kan åbnes igen direkte fra Start Center i en senere session. Database- og source-deklarationerne i .vsx-filerne er dermed den enkle vej tilbage til tabeller fra tidligere arbejde. En enkelt .vsx-fil åbnes via More tools… → Open file.
New article evidence project: vælg en tom mappe, og lad IDE'en oprette article_analysis.vsx, <article-storage>/ og data/. Startprogrammet bruger en lokal SQLite-fil og er lavet til gentagen import af almindelige, rå TXT-artikler. En lokal LLM kan bagefter foreslå de logikbærende passager; du behøver ikke dele artiklen op linje for linje. Eksisterende .vsx-filer overskrives aldrig.
Question for local AI: vælg en hurtig opgave og tilføj dit spørgsmål. Add project facts, code & schema to Request validerer alle registrerede .vsx-filer og føjer deres deklarationer samt alle aktive, databasegodkendte facts og regler til prompten. Hver databasepost medtager eksakt version, hash og godkendelsesproveniens. De andre projektfiler og biblioteker er read-only kontekst; modellen skal returnere ét komplet forslag til den aktuelt åbne fil. Domænetabellernes almindelige rækker hentes ikke. Læs altid hele Request-feltet, og kontrollér model, 64K/128K og lokal endpoint i bekræftelsen. Forslaget kontrolleres af C++-parseren og må kun anvendes, hvis alle eksisterende facts, regler og datadeklarationer er bevaret. Vælg derefter Apply preservation-safe draft; ændringen kan fortrydes og importerer, godkender eller kører intet.

Standardværktøjslinjen viser den normale kæde Start → Save → Check → Compile & build → Run samt Clear model. Compile & build kontrollerer, genererer C++ og linker den lokale executable i én arbejdsgang uden bekræftelsesdialoger; hvis et trin fejler, stopper kæden, og den eksakte fejl vises i en fejlboks og under Diagnostics. Clear kræver bekræftelse og tømmer den aktuelle editor samt nulstiller Diagnostics-fanen, fejltælleren og editorens fejlmarkører; editorændringen kan fortrydes. Den gemte .vsx-fil ændres først, hvis du bagefter trykker Save, og knappen sletter aldrig projektmapper, importerede data, databaser eller reviewhistorik. Tryk More tools… for at åbne ekstra funktioner som Open file, Format, Preview IR, metadata-initialisering, databaseaudit og resultatfil; tryk Fewer tools for at skjule dem igen. I venstre side kan Help: from start to result åbnes og lukkes. Panelerne Current data, Local AI, Claim review og Rule review er tilsvarende fold-ud-sektioner, så du kun ser den hjælp, du aktuelt bruger.

Preview IR betyder *Preview Intermediate Representation*. Det viser en maskinlæsbar JSON-version af det program, C++-compileren har forstået, mellem .vsx-koden og den genererede C++-kode. Det er nyttigt til avanceret kontrol af typer, sources, datasets, regler, queries og hashes. Funktionen kører ikke programmet og ændrer ingen data; begyndere kan normalt ignorere den.

Tryk Check. Fanen Diagnostics skal vise, at programmet er gyldigt.
Tryk Compile & build. IDE'en genererer C++ og linker automatisk; programmet køres ikke endnu.
Vælg Program queries i kørselsvælgeren.
Tryk Run, kontrollér executable-hashen, og godkend.
Når kørslen er færdig, åbner IDE'en automatisk en stor resultatdialog. Den hedder Run completed, når de numeriske diagnostics er acceptable, og Run completed with warnings, når eksempelvis R-hat eller ESS kræver kontrol. Her ser du svarene på programmets ask-queries. Lukker du dialogen, forbliver hele resultatet i fanen Results; knappen Open result view åbner præsentationen igen.

Demoen giver to resultatafsnit, fordi den indeholder både et logisk spørgsmål og en Bayes-model:

Kortet LOGIC QUERY viser grandparent(person_a, Who), svaret TRUE og løsningen Who = person_c. Under Proof står de to facts parent(person_a, person_b) og parent(person_b, person_c) efterfulgt af den afledte konklusion grandparent(person_a, person_c).
Kortet BAYESIAN POSTERIOR viser posterioren for p, efter at programmet har observeret 14 successer i 20 forsøg. Posterior mean: 0.6669 (66.7%) er modellens centrale estimat. 89% HDI: 0.5296 ... to 0.8265 ... betyder, at det tætteste interval, som indeholder 89 % af den beregnede posterior, går fra cirka 53,0 % til 82,6 %. Det er usikkerhed om parameteren under den valgte model og dens antagelser—ikke en garanti om næste forsøg.
Hvert hovedtal har Explain + / Close −. Her kan du åbne en kort forklaring af posterior mean, HDI, R-hat eller effective samples uden at åbne råoutputtet. Den særskilte sektion Explain sampling settings and acceptance rates forklarer chains, retained samples, seed, warmup-tilpasning og acceptance før og efter warmup.
R-hat tæt på 1 betyder, at de fire sampling chains stemmer godt overens. Effective sample size fortæller, hvor mange omtrent uafhængige samples den korrelerede MCMC-kørsel svarer til. Begge er diagnostik; de beviser ikke, at modellens antagelser er rigtige.
Technical details and raw output er lukket som standard. Her ligger samme resultat i maskinlæsbar form sammen med den fulde kørselsdokumentation; en begynder kan normalt lade sektionen være lukket.

Demoens database bruger path ":memory:". Det er en ny, midlertidig SQLite-database for hver proceskørsel. Vælger du datasettet catalog_names i stedet for Program queries, vil resultatet derfor normalt sige Rows returned: 0: queryen lykkedes, men den midlertidige database indeholder ingen brugertabeller. Brug en filsti som path "<data-storage>/demo.sqlite", hvis importerede tabeller skal kunne findes igen ved næste kørsel.

Brug Open Project…, hvis du vil arbejde med en hel mappe. Vælg projektets rodmappe; IDE'en finder .vsx-filer i rod og undermapper og viser dem i venstre side. Klik på en fil for at åbne den. Mapper som <version-control-metadata>, <managed-storage>, <virtual-environment>, <dependency-storage>, <build-output>, <native-build-output>, <distribution-output> og <application-release> ignoreres. Scanningen har dybde- og antalgrænser, og IDE'en afviser et projektfilvalg, som peger uden for den valgte rodmappe.

Kompilering og native build er samlet i én automatisk handling. Run er fortsat separat og kræver en synlig godkendelsesdialog. En ændring i koden ugyldiggør det gamle build, så du ikke ved en fejl kører en anden version end den, du lige har læst.

Praktisk øvelse: fra CSV-fil til resultat i IDE'en

Projektet indeholder en færdig øvelsesmappe:

<example-project>
├── customer_report.vsx
└── customers.csv

Kopiér gerne mappen til din egen projektmappe, så øvelsens SQLite-fil ikke blandes sammen med repositoryets eksempler. CSV-filen indeholder fire kunder fra Danmark og Sverige. Verisyntax-programmet ser sådan ud:

database local:
  engine sqlite
  path "customer_report.sqlite"

source customers:
  database local
  table "customers"
  column id: integer
  column name: text
  column country: text
  column active: boolean
  primary_key id
  provenance row

dataset danish_customers:
  from customers as customer
  select customer.id as id
  select customer.name as name
  where customer.country = "DK"

Gennemfør øvelsen trin for trin:

Åbn Verisyntax IDE, og tryk Open Project….
Vælg mappen practical_customer_report og åbn customer_report.vsx i projektlisten.
Tryk Check. Dokumentet skal være gyldigt, og menuerne Database… og Source… bliver udfyldt fra C++-compilerens IR.
Vælg local (sqlite) under Database…, tryk More tools… → Initialize metadata…, og godkend. Det opretter customer_report.sqlite og Verisyntax' provenance-tabeller i projektmappen.
Vælg customers · customers under Source…, og tryk Import files….
Vælg customers.csv. Skriv create, fordi tabellen ikke findes endnu.
Læs fanen Artifact: kontrollér filhash, mapping, fire datarækker og destinationstabellen. Godkend derefter Commit import.
Tryk Preview rows og godkend den read-only forespørgsel. Du skal kunne se alle fire importerede kunder.
Tryk Compile & build; begge trin kører automatisk.
Vælg danish_customers (sqlite) i kørselsmenuen, og tryk Run.
Resultatdialogens tabel skal vise Customer A, Customer C og Customer D. Customer B vises ikke, fordi hans country er SE. Luk dialogen eller vælg Open Results tab for at se den fulde kørselsdokumentation.

Kører du øvelsen igen med samme database, skal du ikke vælge create: brug append til nye rækker eller merge, hvis eksisterende rækker skal sammenlignes og opdateres efter primary_key id. merge viser en hashbundet plan og sletter aldrig rækker automatisk.

Øvelsen er automatisk testet af projektets C++/CLI-tests: testen kopierer filerne til en midlertidig mappe, initialiserer SQLite, importerer CSV-filen og kontrollerer det faktiske datasetresultat.

Som valgfri udvidelse kan du dokumentere en importeret celle som evidens og lade den lokale model foreslå et claim:

Find associationer på tværs af importerede rækker

Når en tabel er importeret, vælger du den tilhørende database og source under DATA og åbner CLAIM REVIEW. Tryk Find associations across rows. Den lokale C++-runtime gennemgår den seneste komplette, succesfulde importversion (højst 1.000 rækker), uden at kontakte Ollama og uden at oprette claims, facts eller regler.

Dialogen viser effektstørrelse, antal komplette rækker, metode, rå p-værdi, Benjamini-Hochberg-korrigeret q-værdi, et konkret mønstereksempel og datakvalitetsadvarsler. Kategoriske par bruger bias-korrigeret Cramér's V og Fisher exact ved et sparsomt 2×2-skema; numeriske par bruger Spearman-rangkorrelation; blandede par vises med eta-kvadreret, men anbefales ikke automatisk i denne version, fordi der endnu ikke beregnes en korrigerbar p-værdi for dem. Identifikatorlignende kolonner, konstanter, sjældne kategorier og næsten dublerede eller afledte felter bliver udelukket eller blokeret som anbefalinger.

Markér relevante kandidater og tryk Add selected to local Request. Det føjer kun source-hash, import-run, result-hash, mål og advarsler til det redigerbare Request-felt. Først Suggest code locally og den efterfølgende bekræftelse kontakter lokal Ollama. En association er et eksplorativt mønster i netop dette datasæt, ikke kausalitet, et godkendt fact eller row-level evidens; et egentligt claim kræver fortsat synlige mentions og separat review.

Tryk Configure reviewer, og gem et lokalt reviewer-ID og navn.
Vælg igen local (sqlite) og tryk Load imported cells under CLAIM REVIEW.
Vælg eksempelvis cellen med Customer A, og tryk Capture selected mention. Cellen er nu et uforanderligt mention med source-, record-, cell- og content-hash; den er endnu ikke et claim eller fact.
Brug Clear selected cell til at nulstille den aktuelle cellevælger. Brug Remove selected mention(s) eller Clear evidence list til at fjerne evidens fra det aktuelle claim-arbejde. Disse knapper sletter ikke importerede celler eller immutable mention-provenance fra databasen. Hvis evidensen ændres, ryddes et eksisterende claim-udkast, så det ikke kan godkendes mod en forældet evidensliste.
Markér mentionet, behold qwen3.6:35b-a3b og 64K, og tryk Suggest claim locally. Godkend kun kaldet, hvis lokal Ollama må læse det viste excerpt.
Læs og redigér claim-JSON i feltet. Tryk Store reviewed proposal. Hvis projektet endnu ikke har en reviewer-identitet, tilbyder appen nu den lokale engangsopsætning i stedet for at vise en teknisk fejl. Forslaget er stadig inaktivt.
Tryk til sidst Approve as fact eller Reject claim. Kun godkendelse af den viste eksakte hash opretter et aktivt fact. Dette ændrer ikke datasetresultatet; det tilføjer dokumenteret reviewhistorik i metadata-databasen.

Desktop-accepttesten udfører også dette flow uden modelkald med et deterministisk claim, og den særskilte levende test udfører hele kæden med standardmodellen og 64K.

Vil du bruge PostgreSQL i den samme øvelse, erstatter du databaseblokken med:

database warehouse:
  engine postgresql
  connection env "VERISYNTAX_DATABASE_URL"
  schema "public"

Skift derefter database local under source customers: til database warehouse, sæt miljøvariablen før appen åbnes, og vælg warehouse (postgresql) i IDE'en. Resten af import-, compile-, build- og Run-forløbet er det samme.

Situation 1: facts, en regel og et spørgsmål

Dette program kræver ingen database:

parent(person_a, person_b)
parent(person_b, person_c)

grandparent(X, Z)
  if parent(X, Y)
  and parent(Y, Z)

ask grandparent(person_a, Who)

Læs det sådan:

De første to linjer er facts: Person A er forælder til Customer B, og Customer B er forælder til Customer C.
grandparent(X, Z) er det resultat, reglen kan udlede.
Første betingelse finder en Y, som X er forælder til.
Anden betingelse kræver, at samme Y er forælder til Z.
ask spørger efter alle værdier af Who, der kan bevises.

Svaret binder Who til person_c. Hvis du i stedet spørger ask grandparent(person_c, Who), bliver svaret unknown; manglende viden behandles ikke automatisk som falsk.

Situation 2: læs en CSV-fil ind i SQLite

Opret først en fil people.csv:

id,name,country
1,Customer A,DK
2,Customer B,SE

Gem derefter dette som people.vsx i samme mappe:

database local:
  engine sqlite
  path "people.sqlite"

source people:
  database local
  table "people"
  column id: integer
  column name: text
  column country: text
  primary_key id
  provenance row

dataset danish_people:
  from people as person
  select person.id as id
  select person.name as name
  where person.country = "DK"

I IDE'en gør du følgende:

Åbn og gem people.vsx.
Vælg databasen local og tryk More tools… → Initialize metadata…. Godkend oprettelsen af Verisyntax' provenance-tabeller.
Vælg sourcen people og tryk Import files….
Vælg people.csv, vælg operationen create, og læs previewet.
Kontrollér især filhash, mapping, kolonnertyper og antal rækker. Godkend derefter importen.
Tryk Preview rows for at kontrollere destinationstabellen read-only.
Kompilér, byg, vælg datasettet danish_people, og tryk Run.

Resultatet indeholder Customer A, men ikke Customer B. Importen gemmer både de typede destinationsrækker og kæden tilbage til fil, kilderække og oprindelig celleværdi. create bruges første gang; append tilføjer nye rækker; merge sammenligner på den deklarerede primary_key og viser en separat plan før commit. Merge sletter aldrig rækker automatisk.

Situation 3: kombiner kunder og ordrer

Antag, at databasen har tabellerne customers og orders:

database shop:
  engine sqlite
  path "shop.sqlite"

source customers:
  database shop
  table "customers"
  column id: integer
  column name: text
  primary_key id
  provenance row

source orders:
  database shop
  table "orders"
  column id: integer
  column customer_id: integer
  column total: real
  column status: text
  primary_key id
  provenance row

dataset paid_orders_with_customer:
  from customers as customer
  inner join orders as order on customer.id = order.customer_id
  select order.id as order_id
  select customer.name as customer_name
  select order.total as total
  where order.status = "paid"

customer og order er aliases, som kun bruges inde i datasettet. inner join beholder kun ordrer med en matchende kunde. Brug left join, hvis alle rækker fra den første source skal med, også når den anden source mangler. Sources i samme dataset skal bruge samme databaseforbindelse; Verisyntax flytter ikke skjult data mellem SQLite og PostgreSQL.

Situation 4: brug PostgreSQL i stedet for SQLite

PostgreSQL-deklarationen indeholder navnet på en environment variable, aldrig adgangskoden:

database warehouse:
  engine postgresql
  connection env "VERISYNTAX_DATABASE_URL"
  schema "public"

Start IDE'en fra en terminal, der har forbindelsen i sit miljø:

export VERISYNTAX_DATABASE_URL='postgresql:///verisyntax'
open "<desktop-release>/Verisyntax IDE.app"

Hvis psql uden argumenter siger, at databasen med dit brugernavn ikke findes, betyder det kun, at PostgreSQL valgte det navn som standard. Opret eller vælg den ønskede database og brug dens URL, eksempelvis:

createdb verisyntax
export VERISYNTAX_DATABASE_URL='postgresql:///verisyntax'
psql "$VERISYNTAX_DATABASE_URL"

Vælg derefter warehouse i IDE'en og brug More tools… → Initialize metadata…. Den handling opretter/migrerer kun Verisyntax' metadata-schema; den opretter ikke selve PostgreSQL-databasen, brugere eller rettigheder.

Situation 5: modelér usikkerhed uden en LLM

rain ~ chance(0.30)
sprinkler ~ chance(0.20)

wet_grass:
  if rain and sprinkler: chance(0.99)
  if rain: chance(0.90)
  if sprinkler: chance(0.80)
  otherwise: chance(0.02)

observe wet_grass = true
ask rain

Her er 0.30 en modelantagelse om regn, mens observe er den observerede evidens. Verisyntax beregner posterioren i C++; den lokale LLM deltager ikke. Cases læses oppefra, og den første match bruges, så den mest specifikke case står først.

Situation 6: få lokal AI-hjælp uden automatisk at stole på den

I IDE'ens Local AI-felt kan du skrive eksempelvis:

Create a minimal Verisyntax program with two parent facts, one grandparent rule, and one ask query.

Vælg qwen3.6:35b-a3b og 64K, tryk Suggest code locally, og godkend kaldet til 127.0.0.1. Modelfeltet viser lokalt testede muligheder, men du kan også skrive navnet på en anden installeret Ollama-model. IDE'en bruger ingen cloud fallback. Modellen får den versionsstyrede syntaksreference verisyntax-syntax-v1.md, som indeholder C++-testede eksempler for alle implementerede sprogkonstruktioner. Modellen returnerer et struktureret forslag, som parseren kontrollerer. Ved en syntaksfejl kan IDE'en udføre én begrænset lokal reparationsrunde og validerer derefter igen. IDE'en kontrollerer modellens faktiske maksimale kontekstvindue, før den sender forespørgslen.

Forslaget indsættes ikke automatisk. Læs det i outputfanen og vælg først Apply preservation-safe draft, hvis det er relevant. Knappen er kun aktiv, når C++-valideringen har bevist, at forslaget er et komplet gyldigt program, som bevarer eksisterende facts, regler og datadeklarationer. Editorbufferen erstattes i én fortrydelig ændring; det gør ikke claims til facts og aktiverer ikke regler. extraction_confidence fortæller kun, hvor sikkert modellen mener, at den har struktureret teksten — ikke om indholdet er sandt.

Sådan læser du en fejlmeddelelse

En fejl som denne:

people.vsx:12:3: error: unknown source column 'person.countri'

betyder: fil people.vsx, linje 12, kolonne 3. Compileren kender ikke countri; kontrollér stavningen og source-deklarationen. Typiske begynderfejl er:

én eller fire mellemrum i stedet for to;
manglende kolon efter database, source eller dataset;
en alias-reference som people.id, selv om aliaset hedder person;
join af integer til text;
en required kolonne, hvor importfilen har en tom værdi;
en regelvariabel i head, som ingen positiv if/and-betingelse binder;
forsøg på import eller regelgodkendelse før metadata er initialiseret.

Ret fejlen og tryk Check igen. IDE'en kører aldrig et program med kendte compilerfejl.