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:

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. Ingen rækker importeres i guiden. Gem programmet, tryk Check, vælg den genererede source, og brug Import data… til preview og særskilt commit.
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 TXT-import med én meningsfuld tekstpassage pr. linje. Eksisterende .vsx-filer overskrives aldrig.
Question for local AI: vælg en hurtig opgave og tilføj dit spørgsmål. Use current program and data schema føjer den synlige .vsx-tekst og en compiler-valideret katalogoversigt til prompten, så modellen kender kolonner og eksisterende deklarationer; database-tabellernes rækker hentes ikke. Læs altid hele Request-feltet, og kontrollér model, 64K/128K og lokal endpoint i bekræftelsen. Modellen skal returnere ét komplet program. Forslaget kontrolleres af C++-parseren og erstatter først editoren, når du vælger Replace editor with reviewed draft. Ændringen kan fortrydes og importerer eller kører intet.

Standardværktøjslinjen viser kun den normale kæde Start → Save → Check → Compile C++ → Build native → Run. 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 C++ og godkend dokumenthashen. Dette laver C++-kildekode, men kører ikke programmet.
Tryk Build native og godkend. Dette linker en lokal eksekverbar fil.
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 Run completed som en stor resultatdialog. 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.
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, build og kørsel er bevidst tre adskilte trin. Hvert trin bruger en synlig godkendelsesdialog inde i IDE-vinduet. 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 data….
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 C++, godkend, tryk Build native, og godkend igen.
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:

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.
Markér mentionet, behold glm-4.7-flash:latest 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. 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 data….
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 glm-4.7-flash:latest 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 Replace editor with reviewed draft, hvis det er relevant. Forslaget er et komplet program, så knappen erstatter editorbufferen i én fortrydelig ændring i stedet for at indsætte et fragment midt i eksisterende kode. 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.