Taskfile.yaml

version: "3"

vars:
  CGO_FLAGS: 'CGO_LDFLAGS="-L/opt/homebrew/opt/icu4c@78/lib" CGO_CPPFLAGS="-I/opt/homebrew/opt/icu4c@78/include" CGO_CFLAGS="-I/opt/homebrew/opt/icu4c@78/include"'
  GO_ENV: "GONOSUMDB=github.com/nustiueudinastea/*"
  DOCKER_IMAGE: doltswarmdemo
  NR_INSTANCES: '{{.NR_INSTANCES | default "5"}}'
  TIMEOUT: '{{.TIMEOUT | default "20m"}}'
  # Set KEEP=1 to leave containers running after tests for log inspection
  KEEP_CONTAINERS: '{{if eq .KEEP "1"}}KEEP_DOCKER_CONTAINERS=1{{end}}'

tasks:
  build:
    desc: Build the ddolt binary (integration test demo CLI)
    dir: integration
    cmds:
      - "{{.GO_ENV}} {{.CGO_FLAGS}} go build -o ddolt ."

  integration:
    desc: Build Docker image and run all integration tests (Docker, one container per peer)
    summary: |
      Build Docker image and run integration tests.

      Options:
        KEEP=1    Leave containers running after tests (for log inspection)
        TIMEOUT   Test timeout (default: 20m)
        NR_INSTANCES  Number of peer instances (default: 5)

      Examples:
        task integration              # Normal run
        task integration KEEP=1       # Keep containers after test
    interactive: true
    cmds:
      - ./integration/docker/build-docker.sh
      - task: integration:quick

  integration:quick:
    desc: Run integration tests without rebuilding Docker image (faster iteration)
    summary: |
      Run integration tests without rebuilding the Docker image.
      Use this when only test code changed, not the application code.

      Options:
        KEEP=1    Leave containers running after tests (for log inspection)
        TIMEOUT   Test timeout (default: 20m)
        NR_INSTANCES  Number of peer instances (default: 5)

      Examples:
        task integration:quick              # Quick run without rebuild
        task integration:quick KEEP=1       # Keep containers after test
    dir: integration
    interactive: true
    cmds:
      - |
        set -euo pipefail
        BIN=$(mktemp -t doltswarm-integration.test-XXXXXX)
        {{.GO_ENV}} {{.CGO_FLAGS}} go test -c -o "$BIN"
        {{.GO_ENV}} {{.CGO_FLAGS}} {{.KEEP_CONTAINERS}} NR_INSTANCES={{.NR_INSTANCES}} "$BIN" -test.v -test.timeout {{.TIMEOUT}}
        rm -f "$BIN"

  docker:build:
    desc: Build the Docker image for integration tests
    cmds:
      - ./integration/docker/build-docker.sh

  docker:shell:
    desc: Open a shell in the Docker container
    cmds:
      - docker run --rm -it {{.DOCKER_IMAGE}} /bin/bash

  docker:clean:
    desc: Clean up Docker test containers, networks, and initialized images
    summary: |
      Remove all test containers, the test network, and initialized images.
      Use this after running tests with KEEP=1 to clean up.

      Example:
        task integration KEEP=1   # Run tests, keep containers
        docker logs ddolt-test-1  # Inspect logs
        task docker:clean         # Clean up when done
    cmds:
      - docker ps -a --filter "label=doltswarmdemo-test" -q | xargs -r docker rm -f || true
      - docker network rm doltswarmdemo-test || true
      - docker images --filter "reference=doltswarmdemo-initialized*" -q | xargs -r docker rmi -f || true

  docker:logs:
    desc: Show logs from all test containers (use CONTAINER=name for specific one)
    summary: |
      View logs from test containers.

      Options:
        CONTAINER   Specific container name (e.g., ddolt-test-1)
        TAIL        Number of lines to show (default: 100)
        GREP        Pattern to filter logs

      Examples:
        task docker:logs                           # All containers, last 100 lines
        task docker:logs CONTAINER=ddolt-test-1   # Specific container
        task docker:logs GREP="reorder|retry"     # Filter by pattern
        task docker:logs TAIL=500                 # More lines
    vars:
      TAIL: '{{.TAIL | default "100"}}'
    cmds:
      - |
        {{if .CONTAINER}}
          {{if .GREP}}
            docker logs --tail {{.TAIL}} {{.CONTAINER}} 2>&1 | grep -E "{{.GREP}}" || true
          {{else}}
            docker logs --tail {{.TAIL}} {{.CONTAINER}} 2>&1
          {{end}}
        {{else}}
          for c in $(docker ps -a --filter "label=doltswarmdemo-test" --format "{{`{{.Names}}`}}"); do
            echo "=== $c ==="
            {{if .GREP}}
              docker logs --tail {{.TAIL}} "$c" 2>&1 | grep -E "{{.GREP}}" || true
            {{else}}
              docker logs --tail {{.TAIL}} "$c" 2>&1
            {{end}}
            echo ""
          done
        {{end}}

  docker:ps:
    desc: List running test containers
    cmds:
      - docker ps -a --filter "label=doltswarmdemo-test" --format "table {{`{{.Names}}`}}\t{{`{{.Status}}`}}\t{{`{{.Ports}}`}}"

  clean:
    desc: Clean up test artifacts and processes
    cmds:
      - pkill -9 -f ddolt || true
      - rm -rf integration/temp/tst* || true
      - rm -f integration/ddolt || true

  clean:logs:
    desc: Clean up integration test logs
    summary: |
      Remove all saved container logs from integration/logs directory.
      These logs are automatically saved when integration tests complete.

      Example:
        task clean:logs   # Remove all test logs
    cmds:
      - rm -rf integration/logs/*
      - echo "Cleaned integration/logs/"

  kill:
    desc: Kill all running ddolt processes
    cmds:
      - pkill -9 -f ddolt || true

  quint:run:
    desc: Run Quint simulator on the verification spec (random sampling)
    summary: |
      Run the Quint simulator to randomly sample traces and check invariants.
      Fast, no Java required. Does not prove correctness but can find bugs.

      Options:
        SAMPLES     Number of random traces (default: 10000)
        STEPS       Max steps per trace; overrides annotated per-invariant defaults
        VERBOSITY   Passed to quint --verbosity for richer trace output
        INVARIANT   Specific invariant to check (default: all inv_* checks)

      Examples:
        task quint:run                                                       # Full suite using per-invariant default steps
        task quint:run STEPS=30                                              # Override annotated defaults for every invariant
        task quint:run VERBOSITY=3 > /tmp/tests.log 2>&1                     # Capture more detailed output
        task quint:run INVARIANT=inv_fullmesh_heal_bounded_converges         # Single invariant using its annotated step budget
        task quint:run INVARIANT=inv_fullmesh_heal_bounded_converges SAMPLES=50000 STEPS=30
    dir: specs
    vars:
      SAMPLES: '{{.SAMPLES | default "10000"}}'
      STEPS_ARG: "{{if .STEPS}} --steps={{.STEPS}}{{end}}"
      VERBOSITY_ARG: "{{if .VERBOSITY}} --verbosity={{.VERBOSITY}}{{end}}"
      INVARIANT_ARG: "{{if .INVARIANT}} --invariant={{.INVARIANT}}{{end}}"
    cmds:
      - python3 tooling/quint_invariants.py run --spec doltswarm_verify.qnt --samples={{.SAMPLES}}{{.STEPS_ARG}}{{.VERBOSITY_ARG}}{{.INVARIANT_ARG}}

  quint:benchmark:
    desc: Benchmark Quint invariants and regenerate annotated step budgets
    summary: |
      Benchmark every inv_* check, estimate runtime at a chosen suite sample
      count, regenerate specs/invariant-benchmarks.md, and rewrite the
      @default_steps annotations in doltswarm_verify.qnt.

      Options:
        BENCH_SAMPLES   Number of benchmark traces per invariant (default: 1000)
        BENCH_STEPS     Max steps for the benchmark pass (default: 20)
        DEFAULT_SAMPLES Suite sample count used for estimates (default: 10000)
        TARGET_SECONDS  Target engine time budget per invariant (default: 5)

      Example:
        task quint:benchmark
    dir: specs
    vars:
      BENCH_SAMPLES: '{{.BENCH_SAMPLES | default "1000"}}'
      BENCH_STEPS: '{{.BENCH_STEPS | default "20"}}'
      DEFAULT_SAMPLES: '{{.DEFAULT_SAMPLES | default "10000"}}'
      TARGET_SECONDS: '{{.TARGET_SECONDS | default "5"}}'
    cmds:
      - |
        python3 tooling/quint_invariants.py benchmark --spec doltswarm_verify.qnt \
        --benchmark-samples={{.BENCH_SAMPLES}} --benchmark-steps={{.BENCH_STEPS}} \
        --default-samples={{.DEFAULT_SAMPLES}} --target-seconds={{.TARGET_SECONDS}} \
        --output-markdown=invariant-benchmarks.md --write-annotations

  quint:verify:
    desc: Formally verify Quint invariants via Apalache (bounded model checking)
    summary: |
      Run quint verify (Apalache model checker) on invariants. This proves
      correctness up to the given step bound, unlike quint:run which only
      does random sampling.

      Requires Java (Apalache is downloaded automatically by quint).

      Options:
        STEPS       Max steps for bounded model checking (default: 2)
        INVARIANT   Specific invariant to check (default: all inv_* checks)
        JVM_MEMORY  Max JVM heap size (default: 16g)

      Examples:
        task quint:verify INVARIANT=inv_self_in_active_peers
        task quint:verify INVARIANT=inv_self_in_active_peers STEPS=3 JVM_MEMORY=40g
    dir: specs
    vars:
      STEPS: '{{.STEPS | default "2"}}'
      JVM_MEMORY: '{{.JVM_MEMORY | default "16g"}}'
      INVARIANT_ARG: "{{if .INVARIANT}} --invariant={{.INVARIANT}}{{end}}"
    cmds:
      - JVM_ARGS="-Xmx{{.JVM_MEMORY}}" quint verify doltswarm_verify.qnt --max-steps={{.STEPS}}{{.INVARIANT_ARG}}

  quint:docker:build:
    desc: Build the quint-runner Docker image locally (current platform only)
    dir: specs
    cmds:
      - docker buildx build -f tooling/Dockerfile.quint -t nustiueudinastea/quint-runner:latest --load .

  quint:docker:build-and-push:
    desc: Build and push the quint-runner Docker image (amd64 + arm64)
    dir: specs
    cmds:
      - docker buildx build --platform linux/amd64,linux/arm64 -f tooling/Dockerfile.quint -t nustiueudinastea/quint-runner:latest --push .

  quint:cloud:
    desc: Run Quint invariants in parallel on cloud VMs (Scaleway, Hetzner, or UpCloud)
    summary: |
      Provision cloud VMs, pull the quint Docker image, and distribute
      invariant checks across VMs using all available CPUs.

      Scaleway (default): uses ~/.config/scw/config.yaml, deploys to "testing" project
      Hetzner:            requires HCLOUD_TOKEN env var
      UpCloud:            requires UPCLOUD_TOKEN (or UPCLOUD_USERNAME + UPCLOUD_PASSWORD)

      pip install paramiko scaleway   # or: pip install paramiko hcloud / upcloud-api

      Options:
        VMS         Number of VMs to run in parallel (required)
        PROVIDER    Cloud provider: scaleway (default), hetzner, or upcloud
        MODE        Quint mode: run (default) or verify (Apalache model checking)
        SAMPLES     Number of random traces per invariant (default: 10000, run mode only)
        STEPS       Override max steps for all invariants
        VM_TYPE     VM type (default per provider)
        INVARIANT   Run only this specific invariant
        KEEP_VMS    Set to 1 to keep VMs alive after run
        JVM_MEMORY  Max JVM heap for verify mode (default: 8g)

      Examples:
        task quint:cloud VMS=3
        task quint:cloud VMS=2 PROVIDER=hetzner SAMPLES=50000
        task quint:cloud VMS=4 VM_TYPE=POP2-HC-16C-32G SAMPLES=10000
        task quint:cloud VMS=1 KEEP_VMS=1 SAMPLES=1000
        task quint:cloud VMS=3 MODE=verify STEPS=2 JVM_MEMORY=10g
    dir: specs
    vars:
      VMS: '{{.VMS | default ""}}'
      SAMPLES: '{{.SAMPLES | default "10000"}}'
      PROVIDER: '{{.PROVIDER | default "scaleway"}}'
      MODE: '{{.MODE | default "run"}}'
      JVM_MEMORY: '{{.JVM_MEMORY | default "8g"}}'
      PROVIDER_ARG: "--provider={{.PROVIDER}}"
      MODE_ARG: "--mode={{.MODE}}"
      JVM_MEMORY_ARG: "--jvm-memory={{.JVM_MEMORY}}"
      VM_TYPE_ARG: "{{if .VM_TYPE}} --vm-type={{.VM_TYPE}}{{end}}"
      STEPS_ARG: "{{if .STEPS}} --steps={{.STEPS}}{{end}}"
      INVARIANT_ARG: "{{if .INVARIANT}} --invariant={{.INVARIANT}}{{end}}"
      KEEP_ARG: '{{if eq .KEEP_VMS "1"}} --keep-vms{{end}}'
    preconditions:
      - sh: '[ -n "{{.VMS}}" ]'
        msg: "VMS parameter is required. Example: task quint:cloud VMS=3"
    cmds:
      - python3 tooling/quint_cloud_runner.py --vms={{.VMS}} {{.PROVIDER_ARG}} {{.MODE_ARG}} {{.JVM_MEMORY_ARG}}{{.VM_TYPE_ARG}} --samples={{.SAMPLES}}{{.STEPS_ARG}}{{.INVARIANT_ARG}}{{.KEEP_ARG}}

  default:
    desc: Show available tasks
    cmds:
      - task --list